Specification and Verification of Time Requirements with CCSL and Esterel

Charles André 1 Frédéric Mallet 1
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 : The UML Profile for Modeling and Analysis of Real-Time and Embedded (RTE) systems has recently been adopted by the OMG. Its Time Model extends the informal and simplistic Simple Time package proposed by UML2 and others a broad range of capabilities required to model RTE systems including both discrete/dense and chronometric/logical time. MARTE OMG specification introduces a Time Structure inspired from Time models of the concurrency theory and proposes a new clock constraint specification language (CCSL) to specify, within the context of UML, logical and chronometric time constraints. This paper introduces the formal semantics of CCSL clock constraints and proposes a process to use CCSL both as a high-level specification language for UML models and as a golden model to verify the conformance of implementations. A digital filtering video application is used as a running example to support the discussion. The application is first formally specified with CCSL and the specification is refined based on feedback from the CCSL-dedicated simulator. In a second phase, an Esterel program of the application is considered. This program is instrumented with observers derived from the CCSL specification. Esterel Studio formal verification facilities are then used to check the conformity of the Esterel implementation with the CCSL specification. A specific library of Esterel observers has been built for this purpose.
Type de document :
Communication dans un congrès
Christoph Kirsch and Mahmut Kandemir. Languages, Compilers, and Tools for Embedded Systems, Jun 2009, Dublin, Ireland. ACM SIGPLAN/SIGBED, 44, pp.167-176, 2009, ACM SIGPLAN Notices. <10.1145/1543136.1542475>
Liste complète des métadonnées

https://hal.inria.fr/inria-00416654
Contributeur : Frédéric Mallet <>
Soumis le : lundi 14 septembre 2009 - 18:18:11
Dernière modification le : mercredi 7 octobre 2015 - 01:16:19

Identifiants

Collections

Citation

Charles André, Frédéric Mallet. Specification and Verification of Time Requirements with CCSL and Esterel. Christoph Kirsch and Mahmut Kandemir. Languages, Compilers, and Tools for Embedded Systems, Jun 2009, Dublin, Ireland. ACM SIGPLAN/SIGBED, 44, pp.167-176, 2009, ACM SIGPLAN Notices. <10.1145/1543136.1542475>. <inria-00416654>

Partager

Métriques

Consultations de la notice

302