Verification of Synchronization-Related Properties for UML-MARTE RTES Models with a Set of Time Constraints Dedicated Formal Semantic

Ning Ge (1) , Marc Pantel (1, 2)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 Toulouse INP - Institut National Polytechnique (Toulouse)

Critical Real-Time Embedded Systems (RTES) have strong requirement with respect to system's reliability. In Model-Driven Engineering (MDE), verification at early phases of the system lifecycle is an important issue, especially for time constraints in UML-MARTE RTES model. In order to assess that the time requirements are met by the behavior models, the key challenging problem is to transform these time constraints from the UML-MARTE model to computable formal semantics that provide time properties verification. Moreover, to allow the application of this formal semantic to real industrial use cases, the performance of verification should scale well. In this paper, we present a set of time constraint dedicated semantics under the framework for UML-MARTE RTES model's time requirement assessment. We focus on how to specify a set of synchronization-related constraints between system's tasks relying on a formal semantics and to accomplish verification by an efficient observer-based model checking method using Time Petri Nets. We analyse the method's computational complexity and demonstrate the method's scalability by illustrating some performance results.

Mots clés: MDE; UML; MARTE; real-time embedded sys- tem; time requirements; formal semantic; verification; task synchronization

Domaines: Génie logiciel [cs.SE]

Ning Ge, Marc Pantel. Verification of Synchronization-Related Properties for UML-MARTE RTES Models with a Set of Time Constraints Dedicated Formal Semantic. 2012. ⟨hal-00677925⟩