Verifying MARTE/CCSL Mode Behaviors Using UPPAAL

Jagadish Suryadevara Cristina Seceleanu Frédéric Mallet 1 Paul Pettersson
1 AOSTE - Models and methods of analysis and optimization for systems with real-time and embedding constraints
CRISAM - Inria Sophia Antipolis - Méditerranée , Inria Paris-Rocquencourt, COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : In the development of safety-critical embedded systems, the ability to formally analyze system behavior models, based on timing and causality, helps the designer to get insight into the systems overall timing behavior. To support the design and analysis of real-time embedded systems, the UML modeling profile MARTE provides CCSL - a time model and a clock constraint specification language. CCSL is an expressive language that supports specification of both logical and chronometric constraints for MARTE models. On the other hand, semantic frameworks such as timed automata provide verification support for real-time systems. To address the challenge of verifying CCSL-based behavior models, in this paper, we propose a technique for transforming MARTE/CCSL mode behaviors into Timed Automata for model-checking using the UPPAAL tool. This enables verification of both logical and chronometric properties of the system, which has not been possible before. We demonstrate the proposed transformation and verification approach using two relevant examples of real-time embedded systems.
Type de document :
Communication dans un congrès
Software Engineering and Formal Methods, Sep 2013, Madrid, Spain. Springer, 8137, pp.1-15, 2013, Lecture Notes in Computer Science. <10.1007/978-3-642-40561-7_1>
Liste complète des métadonnées

https://hal.inria.fr/hal-00866477
Contributeur : Frédéric Mallet <>
Soumis le : jeudi 26 septembre 2013 - 16:31:17
Dernière modification le : lundi 5 octobre 2015 - 16:59:26

Identifiants

Collections

Citation

Jagadish Suryadevara, Cristina Seceleanu, Frédéric Mallet, Paul Pettersson. Verifying MARTE/CCSL Mode Behaviors Using UPPAAL. Software Engineering and Formal Methods, Sep 2013, Madrid, Spain. Springer, 8137, pp.1-15, 2013, Lecture Notes in Computer Science. <10.1007/978-3-642-40561-7_1>. <hal-00866477>

Partager

Métriques

Consultations de la notice

206