An efficient modeling and execution framework for complex systems development

In this paper, we present different modeling and execution frameworks that allow us to efficiently analyze, design and verify complex systems, mainly to cope with the specific concerns of the Real-time and embedded systems (RTE) domain. First we depict a UML¹/MARTE² based methodology for executable RTE systems modeling with a framework and its underlying model transformations required to execute UML models conforming to the MARTE standard. The advantages of adopting a more generic action language with formal features are highlighted, in order to raise the level of abstraction with formal features. Then, we investigate how MARTE, with its Time Model facilities, can be made to represent faithfully AADL³ periodic/aperiodic tasks communicating through event or data ports, in an approach to end-to-end flow latency analysis. An analytical framework allows us to optimize port-based communication by generating a runtime executive that utilizes shared data areas where appropriate, while ensuring the timing semantic assumed by the control application. An analysis of the AADL mode change protocol is also provided, exposing a translation process that takes as an input an AADL model and produces as an output a time Petri net. We show how an AADL model transformation provides a formal model for model checking activities and we suggest that model transformation provides useful support to improve the integration of formal verification in an industrial engineering process. As a case study we use an implementation of a UDP⁴/IP⁵ protocol stack.