Schedulability analysis by exhaustive state space construction: translating CCSL to transition-based Generalized Buchi Automata - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2012

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

(1) , (1) , (1) , (1)
1

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

Fichier principal
Vignette du fichier
RR-8102.pdf (1.02 Mo) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00743874 , version 1 (21-10-2012)

Identifiers

  • HAL Id : hal-00743874 , version 1

Cite

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⟩
247 View
105 Download

Share

Gmail Facebook Twitter LinkedIn More