Modeling language based on a UML/SysML Profile (2009-2011)
This research was conducted in the OMEGA UML2 Project whose purpose was to upgrade the OMEGA Profile, initially developed for UML 1.1, and the IFx Toolset for UML 2.x. The problematics consisted in defining a compliant and sound typing system and execution model for composite structures and their communication elements (port, connector). We have defined a set of concepts and well-formedness rules for the new OMEGA2 profile and we extended the verification techniques for the new notions while preserving their properties. My work consisted in developing the compiler for UML 2.2 OMEGA models and to adapt the simulator to take into account the new features. Thereafter, I formalized the set of well-formedness rules with OCL and Isabelle/HOL proof assistant in order to prove that the OMEGA language defines a sound type system. I have also extended the compiler and the toolkit for SysML models. The new OMEGA SysML Profile and toolset were applied for the modeling and validation of ambient systems and they are used by the development process of embedded real-time systems implemented in the FullMDE project. Thus, our toolset was applied for the verification of an industry-grade system model, the Solar Wing Generation System of the ATV. Our observations have focused on the toolset limits while verifying large systems. A first optimization approach consisted in defining a simpler semantics for certain notions from the OMEGA2 Profile in order to reduce the representation of a state and the state space of the model. A second solution, explored and detailed in my thesis, is based on using abstractions, notably contracts, for the verification of system models in SysML.
Nowadays computer systems grow larger in size and more complex. Embedded in devices from different domains like avionics, aeronautics, consumer electronics, etc., they are often considered critical with respect to human life, costs and environment. A development that results in safe and reliable critical real-time embedded systems is a challenging task and often error-prone. A way for system designers to tackle this issue is to use a technique that has been proved efficient a large number of times, divide and conquer, based on components and driven by requirements.
However, deriving components from requirements is a difficult task. As well as establishing a network of components whose interaction has to satisfy a requirement. Thus, a development method based on partial and abstract specifications for components as intermediate layer between requirements and components is of gain for system development. Hereafter, we propose to use contracts as such specifications. A contract for a component is a pair (assumption, guarantee) where the assumption is an abstraction of the behavior of component's environment and the guarantee is an abstraction of the component's behavior given that the environment behaves like the assumption. Informally, a contract models the abstract behavior of a component within a given context from the point of view of the requirement to be satisfied. The motivation for using contracts goes, however, beyond their aid for system design. Contracts can be used to decompose requirements, to trace them at different levels of abstraction during iterative refinement steps and, even more, to perform compositional verification of requirement satisfaction.
In this thesis, we implement a methodology for reasoning within contracts at system design and verification within SysML. Thus we define a syntax and semantics of contracts in UML/SysML, as well as a set of refinement relations between contracts and/or components in order to prove requirement satisfaction. Next we provide a formal framework that models the semantics of a UML/SysML model extended with contracts as a variant of Timed Input/Output Automata and a mapping between concepts. The refinement relations are formalized based on the trace inclusion relation and compositional properties are proved to ensure the soundness of the methodology. The approach is instantiated for the OMEGA Profile and IFx toolset with automatic generation of proof obligations. Finally, the approach is applied on an industry grade system model, the Solar Wing Generation System of the Automated Transfer Vehicle, which shows its efficiency by serving comparative verification results.