DocumentCode :
2783831
Title :
Introducing Fairness into Compositional Verification via Unidirectional Counters
Author :
Siirtola, Antti ; Puhakka, Antti ; Lüttgen, Gerald
Author_Institution :
Dept. of Inf. Process. Sci., Univ. of Oulu, Oulu, Finland
fYear :
2012
fDate :
27-29 June 2012
Firstpage :
32
Lastpage :
41
Abstract :
We equip labelled transition systems (LTSs) with unidirectional counters (UCs) which can be initialised to an arbitrary positive value and decremented but not incremented. This formalism, called UCLTSs, enables one to express fairness properties of concurrent systems in a finite form and reason about them in a compositional, refinement-based fashion. Technically, we first show how to apply CSP-style parallel composition and hiding directly on UCLTSs while maintaining compositionality. As our main result, we prove that the refinement checking of UCLTSs under the chaos-free failures-divergences semantics can be reduced to two decidable tasks that can be solved by the popular FDR2 and NuSMV model checkers, respectively.
Keywords :
finite automata; formal verification; CSP-style parallel composition; FDR2 model checkers; NuSMV model checkers; UCLTS; compositional verification; compositionality; formalism; labelled transition systems; refinement checking; unidirectional counters; Algebra; Automata; Educational institutions; Kernel; Radiation detectors; Semantics; Standards; decidability; fairness; formal verification; process algebra; refinement; unidirectional counter;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Application of Concurrency to System Design (ACSD), 2012 12th International Conference on
Conference_Location :
Hamburg
ISSN :
1550-4808
Print_ISBN :
978-1-4673-1687-3
Type :
conf
DOI :
10.1109/ACSD.2012.21
Filename :
6253454
Link To Document :
بازگشت