Verification of MARTE/CCSL Time Requirements in Promela/SPIN

Ling Yin 1 Frédéric Mallet 2 Jing Liu 1
1 Software Engineering Institute
Software Engineering Institute [Shangaï]
2 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 : The Clock Constraint Specification Language (CCSL) provides expressions and relations to specify the time requirements and causal dependencies of systems. It was initially proposed, in the context of MARTE: the UML profile for Modeling and Analysis of Real-Time and Embedded Systems. In this paper, we propose a method to verify CCSL specifications. We give a formal state-based interpretation of a fundamental subset of CCSL clock constraints. Based on it, we translate a CCSL specification into a Promela model and feed the result into the model checker SPIN. Then we show some patterns for expressing the properties of the model and do the verification. A digital filter application is used as an example to illustrate the approach.
Type de document :
Communication dans un congrès
IEEE ICECCS 2011 - 16th IEEE International Conference on Engineering of Complex Computer Systems, Apr 2011, Las Vegas, United States. IEEE, 2011, 〈10.1109/ICECCS.2011.14〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00650621
Contributeur : Frédéric Mallet <>
Soumis le : dimanche 11 décembre 2011 - 18:23:40
Dernière modification le : mardi 6 octobre 2015 - 08:47:07

Identifiants

Collections

Citation

Ling Yin, Frédéric Mallet, Jing Liu. Verification of MARTE/CCSL Time Requirements in Promela/SPIN. IEEE ICECCS 2011 - 16th IEEE International Conference on Engineering of Complex Computer Systems, Apr 2011, Las Vegas, United States. IEEE, 2011, 〈10.1109/ICECCS.2011.14〉. 〈hal-00650621〉

Partager

Métriques

Consultations de la notice

231