Verification of clock constraints: CCSL Observers in Esterel

Charles André 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 Clock Constraint Specification Language (CCSL) has been informally introduced in the specifications of the UML Profile for Modeling and Analysis of Real-Time and Embedded systems (MARTE). In a previous report entitled ``Syntax and Semantics of the Clock Constraint Specification Language'', we equipped a kernel of CCSL with an operational semantics. In the present report we pursue this clarification effort by giving a mathematical characterization to each CCSL constructs. We also propose a systematic approach to the formal verification of CCSL constraints with dedicated Observers. A comprehensive library of Esterel modules, which supports this approach, is provided.
Type de document :
Rapport
[Research Report] RR-7211, INRIA. 2010, pp.59
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00458847
Contributeur : Charles André <>
Soumis le : lundi 22 février 2010 - 14:36:42
Dernière modification le : mardi 17 avril 2018 - 11:31:10
Document(s) archivé(s) le : vendredi 18 juin 2010 - 21:36:40

Fichier

RR-7211.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00458847, version 1

Collections

Citation

Charles André. Verification of clock constraints: CCSL Observers in Esterel. [Research Report] RR-7211, INRIA. 2010, pp.59. 〈inria-00458847〉

Partager

Métriques

Consultations de la notice

381

Téléchargements de fichiers

252