Automated transformations from UML behavior models to contracts

In model driven architecture （MDA）, system requirements are first captured by UML （unified mod- eling language） use cases with sequence diagrams to describe their intended use and implemented by classes of objected-oriented languages in the subsequent design stages. It is important that the dynamic behavior specified by the sequence diagrams is in full compliance with the implementation classes. This paper proposes an auto- matic approach and tool support for generating class contracts, which define a precondition and a postcondition for each operation of the class. The former serves as a guard to ensure invocations of the operations respect the semantics introduced by the sequence diagrams, and the latter places the system in a legal state to facilitate the succeeding operation calls. The contracts can be easily mapped to code of an object-oriented language such as Java. Thus, the approach helps to bridge the gap between the requirements and design stages of system development process. We use our model transformation tool to first generate a UML protocol state machine from the sequence diagrams, and then derive the contracts for a controller class. The transformations take into account the concurrency and critical constructs of the respective UML diagrams.     

Automated formal verification of visual modeling languages by model checking

Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level.     

Recognition of dynamic visual images based on group transformations

A new dynamic image recognition method for image sequences based on two-level recognition of individual states and a set of states as a whole is considered in the paper. Integrated and invariant estimations of internal automorphisms are suggested. The modified collective decision-making method for dynamic image recognition uses four types of pseudodistances, in order to obtain a measure of similarity of input dynamic images with dynamic reference images depending on representation of dynamic features, as sets of numerical parameters, sets of vectors, or sets of functions. The experimental data on dynamic image recognition based on various measures of similarity of the sample with the reference pattern, which take into account isomorphic and permissible homomorphic transformations of visual projections, are presented.     

Formalised EMFTVM bytecode language for sound verification of model transformations

Model-driven engineering is an effective approach for addressing the full life cycle of software development. Model transformation is widely acknowledged as one of its central ingredients. With the increasing complexity of model transformations, it is urgent to develop verification tools that prevent incorrect transformations from generating faulty models. However, the development of sound verification tools is a non-trivial task, due to unimplementable or erroneous execution semantics encoded for the target model transformation language. In this work, we develop a formalisation for the EMFTVM bytecode language by using the Boogie intermediate verification language. It ensures the model transformation language has an implementable execution semantics by reliably prototyping the implementation of the model transformation language. It also ensures the absence of erroneous execution semantics encoded for the target model transformation language by using a translation validation approach.     

A visual token-based formalization of BPMN 2.0 based on in-place transformations

ContextThe Business Process Model and Notation (BPMN) standard informally defines a precise execution semantics. It defines how process instances should be updated in a model during execution. Existing formalizations of the standard are incomplete and rely on mappings to other languages.ObjectiveThis paper provides a BPMN 2.0 semantics formalization that is more complete and intuitive than existing formalizations.MethodThe formalization consists of in-place graph transformation rules that are documented visually using BPMN syntax. In-place transformations update models directly and do not require mappings to other languages. We have used a mature tool and test-suite to develop a reference implementation of all rules.ResultsOur formalization is a promising complement to the standard, in particular because all rules have been extensively verified and because conceptual validation is facilitated (the informal semantics also describes in-place updates).ConclusionSince our formalization has already revealed problems with the standard and since the BPMN is still evolving, the maintainers of the standard can benefit from our results. Moreover, tool vendors can use our formalization and reference implementation for verifying conformance to the standard.     

基于UPPAAL的AADL模型可调度性验证

针对体系结构分析设计语言(AADL)模型的可调度性验证问题,提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法,并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性。相比其他方法而言,基于形式化理论的本方法的验证结果更加精确。     

Slicing ATL model transformations for scalable deductive verification and fault localization

Model-driven engineering (MDE) is increasingly accepted in industry as an effective approach for managing the full life cycle of software development. In MDE, software models are manipulated, evolved and translated by model transformations (MT), up to code generation. Automatic deductive verification techniques have been proposed to guarantee that transformations satisfy correctness requirements (encoded as transformation contracts). However, to be transferable to industry, these techniques need to be scalable and provide the user with easily accessible feedback. In MT-specific languages like ATL, we are able to infer static trace information (i.e., mappings among types of generated elements and rules that potentially generate these types). In this paper, we show that this information can be used to decompose the MT contract and, for each sub-contract, slice the MT to the only rules that may be responsible for fulfilling it. Based on this contribution, we design a fault localization approach for MT, and a technique to significantly enhance scalability when verifying large MTs against a large number of contracts. We implement both these algorithms as extensions of the VeriATL verification system, and we show by experimentation that they increase its industry readiness.     

Automated verification of refinement laws

Demonic refinement algebras are variants of Kleene algebras. Introduced by von Wright as a light-weight variant of the refinement calculus, their intended semantics are positively disjunctive predicate transformers, and their calculus is entirely within first-order equational logic. So, for the first time, off-the-shelf automated theorem proving (ATP) becomes available for refinement proofs. We used ATP to verify a toolkit of basic refinement laws. Based on this toolkit, we then verified two classical complex refinement laws for action systems by ATP: a data refinement law and Back’s atomicity refinement law. We also present a refinement law for infinite loops that has been discovered through automated analysis. Our proof experiments not only demonstrate that refinement can effectively be automated, they also compare eleven different ATP systems and suggest that program verification with variants of Kleene algebras yields interesting theorem proving benchmarks. Finally, we apply hypothesis learning techniques that seem indispensable for automating more complex proofs.     

基于马尔可夫模型的多agent自适应在线验证

用于领域中业务关键型的自适应系统(self-adaptive system,SAS)需要遵从严格的质量要求,在多agent自适应系统运行过程中需要根据动态环境与需求实现自适应调整。针对上述问题,提出了一种基于马尔可夫的多agent自适应在线验证方法。首先将多agent系统中环境影响因素转换为概率形式,然后将系统形式化为马尔可夫模型,最后通过模型检查的方式进行在线验证,使系统通过验证结果对自身进行调控。通过现实的智能无人停车场案例进行了实验,论述了方法的使用流程以及验证效果。实验结果表明,该方法适用于具有多agent的自适应系统,并能够在系统出现故障情况下及时进行调控,相比原始系统的稳定性有了较大的改善。     

Interactive specification and verification of behavioral adaptation contracts

ContextAdaptation is a crucial issue when building new applications by reusing existing software services which were not initially designed to interoperate with each other. Adaptation contracts describe composition constraints and adaptation requirements among these services. The writing of this specification by a designer is a difficult and error-prone task, especially when interaction protocols are considered in service interfaces.ObjectiveIn this article, we propose a tool-based, interactive approach to support the contract design process.MethodOur approach includes: (i) a graphical notation to define port bindings, and an interface compatibility measure to compare protocols and suggest some port connections to the designer, (ii) compositional and hierarchical techniques to facilitate the specification of adaptation contracts by building them incrementally, (iii) validation and verification techniques to check that the contract will make the involved services work correctly and as expected by the designer.ResultsOur results show a reduction both in the amount of effort that the designer has to put into building the contract, as well as in the number of errors present in the final result (noticeably higher in the case of manual specification).ConclusionWe conclude that it is important to provide integrated tool support for the specification and verification of adaptation contracts, since their incorrect specification induces erroneous executions of the system. To the best of our knowledge, such tool support has not been provided by any other approach so far, and hence we consider the techniques described in this paper as an important contribution to the area of behavioral software adaptation.     

Automated verification of security pattern compositions

Software security becomes a critically important issue for software development when more and more malicious attacks explore the security holes in software systems. To avoid security problems, a large software system design may reuse good security solutions by applying security patterns. Security patterns document expert solutions to common security problems and capture best practices on secure software design and development. Although each security pattern describes a good design guideline, the compositions of these security patterns may be inconsistent and encounter problems and flaws. Therefore, the compositions of security patterns may be even insecure. In this paper, we present an approach to automated verification of the compositions of security patterns by model checking. We formally define the behavioral aspect of security patterns in CCS through their sequence diagrams. We also prove the faithfulness of the transformation from a sequence diagram to its CCS representation. In this way, the properties of the security patterns can be checked by a model checker when they are composed. Composition errors and problems can be discovered early in the design stage. We also use two case studies to illustrate our approach and show its capability to detect composition errors.     

异或视觉密码方案目标优化研究*

通过建立群结构的视觉密码目标优化模型,设计了一种基于异或的(k, n)门限方案。该方案将基础矩阵构造问题转换为共享份中出现黑白像素概率的求解问题,通过概率矩阵对加密规则进行选择得到共享份。实验结果表明,该方案在像素不扩展的同时,使相对差大幅改善。     

基于视觉感知模型的行人再识别

行人再识别是多摄像机协同监控系统中需要解决的关键问题之一。针对行人再识别问题的影响因素,根据人类视觉系统对行人进行识别的过程,提出一种基于视觉感知模型的行人再识别方法。该方法根据行人的局部对称性将行人分为头部、躯干和腿部,分别以行人的躯干和腿部的垂直对称轴为中心建立基于感知均匀颜色空间CIELAB的局部加权空间直方图,结合贝叶斯框架下基于局部统计特征的显著区域检测方法描述行人外观特征。两种特征分别采用不同的距离测度计算相似度,并通过自适应选取权值的方法进行线性融合。基于VIPeR数据库的实验比较和分析验证了该方法的行人再识别性能。     

基于模型检测的微服务组合平台QoS验证

针对当前缺少对微服务组合平台的服务质量（QoS）指标进行分析验证的问题，提出一种基于模型检测的形式化验证方法，对影响微服务平台性能的因素进行分析评估。首先，将微服务组合的服务资源配置过程划分为服务请求、资源配置和服务执行3个阶段，并分别由服务请求队列、服务请求配置器和提供服务资源的虚拟机等模块实现；其次，将各个模块的实现过程建模为带标记Markov回报模型（LMRM），借助类似于进程代数的同步概念获得微服务组合过程的全局模型；接着，用连续随机回报逻辑公式刻画期望的QoS指标；最后，将形式模型与逻辑公式作为模型检测工具PRISM的输入以获得验证结果。实验结果表明，LMRM可较好地用于微服务组合平台的建模和QoS验证分析。     

基于模型检测的微服务组合平台QoS验证

针对当前缺少对微服务组合平台的服务质量（QoS）指标进行分析验证的问题,提出一种基于模型检测的形式化验证方法,对影响微服务平台性能的因素进行分析评估。首先,将微服务组合的服务资源配置过程划分为服务请求、资源配置和服务执行3个阶段,并分别由服务请求队列、服务请求配置器和提供服务资源的虚拟机等模块实现;其次,将各个模块的实现过程建模为带标记Markov回报模型（LMRM）,借助类似于进程代数的同步概念获得微服务组合过程的全局模型;接着,用连续随机回报逻辑公式刻画期望的QoS指标;最后,将形式模型与逻辑公式作为模型检测工具PRISM的输入以获得验证结果。实验结果表明,LMRM可较好地用于微服务组合平台的建模和QoS验证分析。     

Formal verification of multitasking applications based on timed automata model

The aim of this paper is to show, how a multitasking application running under a real-time operating system compliant with an OSEK/VDX standard can be modeled by timed automata. The application under consideration consists of several non-preemptive tasks and interrupt service routines that can be synchronized by events. A model checking tool is used to verify time and logical properties of the proposed model. Use of this methodology is demonstrated on an automated gearbox case study and the result of the worst-case response time verification is compared with the classical method based on the time-demand analysis. It is shown that the model-checking approach provides less pessimistic results due to a more detailed model and exhaustive state-space exploration.

Automated assumption generation for compositional verification

We describe a method for computing a minimum-state automaton to act as an intermediate assertion in assume-guarantee reasoning, using a sampling approach and a Boolean satisfiability solver. For a set of synthetic benchmarks intended to mimic common situations in hardware verification, this is shown to be significantly more effective than earlier approximate methods based on Angluin’s L* algorithm. For many of these benchmarks, this method also outperforms BDD-based model checking and interpolation-based model checking. We also demonstrate how domain knowledge can be incorporated into our algorithm to improve its performance.     

A survey of database design transformations based on the Entity-Relationship model

At present, the Entity-Relationship (ER) model is the most important paradigm for conceptual database design. Since the model was introduced in the mid-seventies, a large body of literature has been published on transforming conceptual ER schemas or diagrams into logical data models. The purpose of this paper is to survey this literature. A first focus is on transformation approaches from the ER model to traditional data models, i.e. to the relational, the network, or the hierarchical model; this is then complemented by a discussion of more recent transformations to object-oriented models. A second focus is on considering the process of reverse engineering, i.e. transformations from a logical model back into the ER model; finally, an overview of direct transformations between various logical data models is presented.