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, Laboratoire I3S - 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.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/hal-00650621
Contributor : Frédéric Mallet <>
Submitted on : Sunday, December 11, 2011 - 6:23:40 PM
Last modification on : Monday, November 5, 2018 - 3:36:03 PM

Identifiers

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〉

Share

Metrics

Record views

299