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.

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.

Software engineering tasks as design and programming require the concurrent participation of multiple users, possibly geographically dispersed. But traditional software environments have not been designed to facilitate collaborative work. In this paper we present briefly a tool for communication among many persons in which users can elaborate documents with synchronous and asynchronous interaction modes.>

This paper states the following result. Replacing a pair of actions (rev x; send y) with another pair of actions (send y; rev x) in a machine M cannot introduce deadlocks or unspecified receptions when this machine communicates with another machine N. This result is utilized in identifying for any given machine M a large family of machines (N1, N2, ...) such that the communication between M and any Ni is free from deadlocks and unspecified receptions. Processes exchanged messages through FIFO channels and modelled with finite states machines labelled with actions of receiving and transmitting messages. Some special classes are discussed with guaranteed progress.>