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

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-00743874
Contributor : Team Kairos <>
Submitted on : Sunday, October 21, 2012 - 1:17:15 PM
Last modification on : Monday, November 5, 2018 - 3:36:03 PM
Document(s) archivé(s) le : Tuesday, January 22, 2013 - 3:38:59 AM

File

RR-8102.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

458

Files downloads

154