Safe CCSL Specifications and Marked Graphs

Frédéric Mallet 1, * Jean-Vivien Millo 1 Robert De Simone 1
* Auteur correspondant
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, Laboratoire I3S - COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : The Clock Constraint Specification Language (CCSL) proposes a rich polychronous time model dedicated to the specification of constraints on logical clocks: i.e., sequences of event occurrences. A priori independent clocks are progressively constrained through a set of clock operators that define when an event may occur or not. These operators can be described as labeled transition systems that can potentially have an infinite number of states. A CCSL specification can be scheduled by performing the synchronized product of the transition systems for each operator. Even when some of the composed transition systems are infinite, the number of reachable states in the product may still be finite: the specification is safe. The purpose of this paper is to propose a sufficient condition to detect that the product is actually safe. This is done by abstracting each CCSL constraint (relation and expression) as a marked graph. Detecting that some specific places, called counters, in the resulting marked graph are safe is sufficient to guarantee that the composition is safe.
Type de document :
Communication dans un congrès
Roncken, Marly and Talpin, Jean-Pierre. MEMOCODE - 11th IEEE/ACM International Conference on Formal Methods and Models for Codesign, Oct 2013, Portland, United States. IEEE CS, pp.157-166, 2013, 〈http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6670955〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00913962
Contributeur : Team Kairos <>
Soumis le : jeudi 5 décembre 2013 - 10:43:17
Dernière modification le : lundi 5 novembre 2018 - 15:36:03
Document(s) archivé(s) le : jeudi 6 mars 2014 - 01:25:11

Fichier

memocodePub.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00913962, version 1

Collections

INRIA | I3S | UNICE | UNIV-COTEDAZUR | INRIA-ROCQ

Citation

Frédéric Mallet, Jean-Vivien Millo, Robert De Simone. Safe CCSL Specifications and Marked Graphs. Roncken, Marly and Talpin, Jean-Pierre. MEMOCODE - 11th IEEE/ACM International Conference on Formal Methods and Models for Codesign, Oct 2013, Portland, United States. IEEE CS, pp.157-166, 2013, 〈http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6670955〉. 〈hal-00913962〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

377

Téléchargements de fichiers

181

Contact


archive-ouverte@inria.fr