With the increasing complexity of Cyber-Physical Systems (CPS), it is interesting to decompose a CPS into sub-systems. This provides greater modularity and flexibility so that each system can be developed independently, making it easier to maintain. Also, it can improve its fault tolerance. However, this decomposition of the system can lead to inconsistency. This article proposes an approach for early verification of CPS decomposition using SysML. We address the limitations of SysML as a semi-formal language by introducing syntax and static semantics for its structural diagrams. The aim is to verify structural consistency before defining behavioral aspects. For that, the proposed approach verifies a set of structural consistency rules within a refinement relation to ensure that sub-components offer at least the same services as the abstract block and require the same services. Furthermore, the sub-blocks must satisfy all the requirements that the abstract block is supposed to verify. We used the CyCab as a case study to demonstrate the effectiveness of this approach.

International audience

International audience

International audience

International audience

The complexity of heterogeneous systems has been increased during last years. One challenge of designing these systems is to deal with the application of methodologies based on Model Driven Architecture (MDA). MDA is a development framework that enables the description of systems by means of different models with transformations. This is an important area of research and consists on developping methodologies to reduce cost and time spent during their development. In our case, SysML, targets system descriptions in a high level of abstraction and provide diagrams for requirements. SystemC language is chosen as an alternative to the traditional languages and its simulation kernel is an important aspect which allows the designer to evaluate the system behaviours through simulations. This paper proposes a combined approach based onMDA concepts and rules to transform SysML semi-formal model to SystemC. The transformations are ensured by ATL language. A traffic light system is taken as a reference case study and used to illustrate our practical application. It is implemented on TopCased platform.

This paper proposes an approach to verify SysML models consistency and to validate the transformation of SysML models to VHDL-AMS code. This approach is based on two main solutions: the use of model-to-model transformation to verify SysML models consistency and writing unit tests to validate model transformations. The translation of SysML models into VHDL-AMS simulable code uses MMT (Model to Model Transformation) ATL Atlas Transformation Language and M2T (Model To Text) Acceleo tooling. The test validation of the model transformations is performed using EUNIT framework.

International audience

International audience

In this paper, we are interested in verifying temporal properties of hierarchical systems when states are refined by automata. The system is modeled by hierarchical automata and temporal properties are expressed by theLTL(linear temporal logic). We present a technique to cope with state explosion problem induced by the complexity of the system. The first aim is to define a refinement relation between hierarchical automata. We show that this relation preserves theLTLproperties under some conditions. The advantage is that the model checking is done only on an abstraction with few states and the property is preserved in the following refinement process of systems. The second part concerns only local properties specified on the new introduced automata when the systems is refined from the abstract model. We show how to verify an usual class of patterns without using the model checking technique. The proposed approach is illustrated by a simple autopilot control.