An integrated semantics for reasoning about SysML design models using refinement

SysML is a variant of UML for systems design. Several formalisations of SysML (and UML) are available. Our work is distinctive in two ways: a semantics for refinement and for a representative collection of elements from the UML4SysML profile (blocks, state machines, activities, and interactions) used in combination. We provide a means to analyse and refine design models specified using SysML. This facilitates the discovery of problems earlier in the system development lifecycle, reducing time, and costs of production. Here, we describe our semantics, which is defined using a state-rich process algebra and implemented in a tool for automatic generation of formal models. We also show how the semantics can be used for refinement-based analysis and development. Our case study is a leadership-election protocol, a critical component of an industrial application. Our major contribution is a framework for reasoning using refinement about systems specified by collections of SysML diagrams.     

FDR Explorer

We describe: (1) the internal structures of FDR, the refinement model checker for Hoare’s Communicating Sequential Processes (CSP); and (2) an application-programming interface (API) that allows users to interact more closely with FDR and to have finer-grain control over its behaviour and data structures. This API makes it possible to create optimised CSP code to perform refinement checks that are more space or time efficient, enabling the analysis of more complex and data-intensive specifications. The API can be used either by those constructing CSP models or by tools that automatically generate CSP code. We present examples of using our tool, including handling advanced FDR features such as transparent functions, which compress state spaces before checking. We also show how to transform FDR’s graph format into a graph notation such as JGraph, enabling visualisation of labelled transition systems of CSP specifications.     

Formalisations and applications of BPMN

We present two formalisations of the Business Process Modelling Notation (BPMN). In particular, we introduce a semantic model for BPMN in the process algebra CSP; we then study an augmentation of this model in which we introduce relative timing information, allowing one to specify timing constraints on concurrent activities. By exploiting CSP refinement, we are able to show some relationships between the timed and the untimed models. We then describe a novel empirical studies’ model, and the transformation to BPMN, allowing one to apply our formal semantics for analysing different kinds of workflows. To provide a better facility for describing behaviour specification about a BPMN diagram, we also present a pattern-based approach using which a workflow designer could specify properties which could otherwise be difficult to express. Our approach is specifically designed to allow behavioural properties of BPMN diagrams to be mechanically verified via automatic model checking as provided by the FDR tool. We use two examples to illustrate our approach.     

Concurrency and Refinement in the Unified Modeling Language

This paper shows how a formal notion of refinement may be defined for models, and model components, expressed in the Unified Modeling Language (UML). A formal, behavioural semantics is given to combinations of class, object, and state diagrams, using the notation of Communicating Sequential Processes (CSP); this semantics is adequate for the analysis of concurrent, communicating behaviour, and induces a notion of refinement for UML based upon existing notions of traces and failures refinement for CSP.     

A formal verification framework for SysML activity diagrams

SysML activity diagrams are OMG/INCOSE standard diagrams used for modeling and specifying probabilistic systems. They support systems composition by call behavior and send/receive artifacts. For verification, the existing approaches dedicated to these diagrams are limited to a restricted set of artifacts. In this paper, we propose a formal verification framework for these diagrams that supports the most important artifacts. It is based on mapping a composition of SysML activity diagrams to the input language of the probabilistic symbolic model checker called “PRISM”. To prove the soundness of our mapping approach, we capture the underlying semantics of both the SysML activity diagrams and their generated PRISM code. We found that the probabilistic equivalence relation between both semantics preserve the satisfaction of the system requirements. Finally, we demonstrate the effectiveness of our approach by presenting real case studies.     

Unifying classes and processes

Previously, we presented Circus, an integration of Z, CSP, and Morgan’s refinement calculus, with a semantics based on the unifying theories of programming. Circus provides a basis for development of state-rich concurrent systems; it has a formal semantics, a refinement theory, and a development strategy. The design of Circus is our solution to combining data and behavioural specifications. Here, we further explore this issue in the context of object-oriented features. Concretely, we present an object-oriented extension of Circus called OhCircus. We present its syntax, describe its semantics, explain the formalisation of method calls, and discuss our approach to refinement.     

Property specifications for workflow modelling

Previously we provided two formal behavioural semantics for the Business Process Modelling Notation (BPMN) in the process algebra CSP. By exploiting CSP’s refinement orderings, developers may formally compare their BPMN models. However, BPMN is not a specification language, and it is difficult and sometimes impossible to use it to construct behavioural properties against which other BPMN models may be verified. This paper considers a pattern-based approach to expressing behavioural properties. We describe a property specification language PL for capturing a generalisation of Dwyer et al.’s Property Specification Patterns, and present a translation from PL into a bounded, positive fragment of linear temporal logic, which can then be automatically translated into CSP for simple refinement checking. We present a detailed example studying the behavioural properties of an airline ticket reservation business process. Using the same example we also describe some recent results on expressing behavioural compatibility within our semantic models. These results lead to a compositional approach for ensuring deadlock freedom of interacting business processes.     

Using formal methods with SysML in aerospace design and engineering

Maintaining design consistency is a critical issue for macro-level aerospace development. The inability to maintain design consistency is a major contributor to cost and schedule overruns. By embedding The Systems Modeling Language (SysML) within a formal logic, formal methods can be used to maintain consistency as a design evolves. SysML, provided with a formal semantics, enables engineers to employ reasoning in the course of a typical model-based development process. Engineers can make use of formal methods within the context of current engineering practice and tools without needing to have special formal methods training. As component subsystems are introduced to refine a design, their assumptions are checked against current assumptions. If new assumptions do not introduce inconsistency, they are added to the model assumptions. If the assumptions render the design inconsistent, they are detected which minimizes potential rework. SysML has a demonstrated capability for top-to-bottom design refinement for large-scale aerospace systems. SysML does not have a formal logic-based semantics. The logical formalism within which SysML is embedded matches the informal semantic of SysML closely. The approach to integrating formal methods with SysML is illustrated with a typical macro-level aerospace design task. The design process produces a design solution which provably satisfies the top level requirements. The example provides evidence that coupling formal methods with SysML can realistically be applied to solve aerospace development problems. The approach results from a number of detailed design trades employing a model-based system development process which used SysML as the model integration framework.     

Concurrency and Refinement in the Unified Modeling Language

This paper defines a formal semantics for a subset of the Unified Modeling Language (UML). It shows how suitable combinations of class, object, state, and sequence diagrams can be associated with patterns of interaction, expressed in the event notation of Communicating Sequential Processes (CSP). The diagram semantics is then extended to give a meaning to complete models – suitable combinations of diagrams – and thus a concurrency semantics for object models written in UML. This model semantics is in turn used to define a theory of refinement, based upon existing notions of data and process refinement.     

基于不干扰理论的隔离语义描述及隔离策略的自动化验证方法研究

隔离有助于阻止信息泄露或被篡改、错误或失败被传递等.利用不干扰理论给出了隔离的精确语义,以利于分析和制定系统的隔离策略;利用通信顺序进程CSP来定义上述隔离语义,并给出一个系统满足给定隔离策略的判定断言,以利于借助形式化验证工具FDR2来实现系统内隔离策略的自动化验证.以基于虚拟机的文件服务监控器为例,展示了如何利用CSP来建模一个系统及其隔离策略以及如何利用FDR2来验证该系统模型满足给定的隔离策略.     

Automatically Detecting and Visualising Errors in UML Diagrams

UML has become the de facto standard for object-oriented modelling. Currently, UML comprises several different notations with no formal semantics attached to the individual diagrams or their integration, thus preventing rigorous analysis of the diagrams. Previously, we developed a formalisation framework that attaches formal semantics to a subset of UML diagrams used to model embedded systems. This paper describes automated structural and behavioural analyses applicable to UML diagrams using our formalisation framework. In addition to intra- and inter-diagram consistency checks, we discuss how simulation and model checking can be used in tandem for behavioural analysis of the UML diagrams. Our tools also visually interpret the analysis results in terms of the original UML diagrams, thereby facilitating their correction and refinement. We illustrate these capabilities through the modelling and analysis of UML diagrams for an automotive industrial case study. Correspondence and offprint requests to: Dr B. Cheng, Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, 3115 Engineering Building, East Lansing, MI 48824, USA. Tel.: +1 517 355 8344; Fax: +1 517 432 1061; Email: chengb@cse.msu.edu     

一种从Object—Z到CSP规格说明的转化方法

面向对象形式规格说明语言Object-Z与进程代数CSP相结合是当今的一个热点,它既可以表示复杂的模块化数据与算法,又可以表示系统的行为,但求精与验证对它们结合后的规格说明需要分别进行处理。本文提出了一个方法,把Object-Z规格说明转化为CSP规格说明,可以方便地处理结合后的规格说明,因此求精与推理对结合后的规格说明可以按CSP规则与方法一致来进行处理。此外,转化后的Object-Z规格说明可以按照CSP方法进行模型检查。     

基于Spin的SysML活动图验证框架

系统建模语言（systems modeling language,SysML）缺乏精确的形式化分析和验证手段,造成模型存在死锁、活锁等诸多问题,可以通过形式化验证方法来提高模型的正确性。然而,受制于传统的形式化方法需要复杂的公式推理,并且不易理解等方面局限性,大多数验证仅限专家使用并且很耗时。为了克服SysML模型中存在的问题,提出了一种针对SysML多层次活动图的分析验证框架。它可以根据已构建的模型,将多层次活动图分解转换为Spin的输入模型,并对相关子图进行重组和验证。实验表明,该方法可以有效识别多层次活动图,并准确实施转换,为模型验证的演化提供支持。     

The behavioural semantics of Event-B refinement

Event-B provides a flexible framework for stepwise system development via refinement. The framework supports steps for (a) refining events (one-by-one), (b) splitting events (one-by-many), and (c) introducing new events. In each of the steps events can be indicated as convergent (to be made internal) or anticipated (treatment deferred to a later refinement step). All such steps are accompanied with precise proof obligations. However, no behavioural semantics has been provided to validate the proof obligations, and no formal justification has previously been given for the application of these rules in a refinement chain. Behavioural semantics expresses a clear relationship between the first and last machines in a refinement chain. The framework we present provides a coherent justification for Abrial’s approach to refinement in Event-B, and its generalisation to interface extension: adding events to the interface. In this paper, we give a behavioural semantics for Event-B refinement, with a treatment for the first time of splitting events and of anticipated events, adding to the well-understood treatment of convergent events. To this end, we define a CSP semantics for Event-B and show how the different forms of Event-B refinement can be captured as CSP refinement. It turns out that the appropriate CSP refinement relationship is influenced by the particular Event-B development strategy taken. We present two such strategies, one allowing, the other disallowing interface extensions.     

Quantitative and qualitative analysis of SysML activity diagrams

Model-driven engineering refers to a range of approaches that uses models throughout systems and software development life cycle. Towards sustaining such a successful approach in practice, we present a model-based verification framework that supports the quantitative and qualitative analysis of SysML activity diagrams. To this end, we propose an algorithm that maps SysML activity diagrams into Markov decision processes expressed using the language of the probabilistic symbolic model checker PRISM. Furthermore, we elaborate on the correctness of our translation algorithm by proving its soundness with respect to a SysML activity diagrams operational semantics that we also present in this work. The generated models can be verified against a set of properties expressed in the probabilistic computation tree logic. To automate our approach, we developed a prototype tool that interfaces a modeling environment and the probabilistic model checker. We also show how to leverage adversary generation to provide the developer with a useful counterexample/witness as a feedback on the verified properties. Finally, the established theoretical foundations are complemented with an illustrative case study that demonstrates the usability and benefit of such a framework.     

基于SysML的机载软件分层精化建模与验证方法

机载软件被广泛应用于航空航天领域, 大幅提升了机载设备的性能.但随着机载软件规模逐渐增大、功能逐渐增多, 给软件的开发带来了难度, 如何保障机载软件的正确性和安全性也成为一个难题.基于模型的开发可以有效提升开发效率, 而形式化方法能够有效保障软件的正确性.为了降低开发难度, 同时保障机载软件的正确性、安全性, 本文提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先使用SysML状态机图对机载软件的动态行为进行建模, 根据提出的精化规则, 对初始模型进行手动逐层精化得到精化设计模型.然后针对软件模型动态变化的特性, 将SysML状态机模型自动转换为时间自动机网络, 并从软件需求中手动提取形式化TCTL性质进行模型检验.其次, 为了实现编码自动化, 将SysML模型自动转换至Simulink, 利用Simulink Coder生成源代码.最后, 以一个自动飞行控制软件为例进行了开发和验证, 实验结果表明了该方法的有效性.     

A tactic language for refinement of state-rich concurrent specifications

Circus is a refinement language in which specifications define both data and behavioural aspects of concurrent systems using a combination of Z and CSP. Its refinement theory and calculus are distinctive, but since refinements may be long and repetitive, the practical application of this technique can be hard. Useful strategies have been identified, described, and used, and by documenting them as tactics, they can be expressed and repeatedly applied as single transformation rules. Here, we present ArcAngelC, a language for defining such tactics; we present the language, its semantics, and its application in the formalisation of an existing strategy for verification of Ada implementations of control systems specified by Simulink diagrams. We also discuss its mechanisation in a theorem prover, ProofPower-Z.