Schedulability analysis by exhaustive state space construction: translating CCSL to transition-based Generalized Buchi Automata

Ling Yin 1 Julien Deantoni 1 Frédéric Mallet 1 Robert De Simone 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 : In previous work we defined a language (CCSL) made to express real-time temporal scheduling constraints. It uses the notion of partially independent logical clocks (or time threads), of which seemingly physical discrete time is a special case, hence the name Clock Constraint Specification Language. Constraints can represent (asynchronous) causality and precedence relations, or (synchronous) simultaneity ones. A solution to a set of such constraints is called a schedule, as it brings back all the clocks down to a single, totally ordered discrete time (and thus allows to timing events a schedule slot). In the current paper we study the formal semantics of CCSL, by translation into specific automata recognizing infinite sequences of clock steps. We consider the appropriate acceptance criteria for omega-languages (transition-based generalized Buchi), and motivate this choice. We also study how the automata can be minimized, by removing useless states (which is more than the usual check for emptiness of the whole language in classical model-checking approaches). We feel our work builds a definite link between the scheduling and the formal semantic model-checking communities.
Keywords : CCSL Scheduling Automata
Type de document :
Rapport
[Research Report] RR-8102, 2012, pp.22
Liste complète des métadonnées


https://hal.inria.fr/hal-00743874
Contributeur : Team Aoste <>
Soumis le : dimanche 21 octobre 2012 - 13:17:15
Dernière modification le : samedi 17 septembre 2016 - 01:36:45
Document(s) archivé(s) le : mardi 22 janvier 2013 - 03:38:59

Fichier

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

Identifiants

  • HAL Id : hal-00743874, version 1

Collections

Citation

Ling Yin, Julien Deantoni, Frédéric Mallet, Robert De Simone. Schedulability analysis by exhaustive state space construction: translating CCSL to transition-based Generalized Buchi Automata. [Research Report] RR-8102, 2012, pp.22. <hal-00743874>

Partager

Métriques

Consultations de
la notice

330

Téléchargements du document

121