Priority systems [deadlock-free systems]

We present a framework for the incremental construction of deadlock-free systems meeting given safety properties. The framework borrows concepts and basic results from the controller synthesis paradigm by considering a step in the construction process as a controller synthesis problem. We show that priorities are expressive enough to represent restrictions induced by deadlock-free controllers preserving safety properties. We define a correspondence between such restrictions and priorities and provide compositionality results about the preservation of this correspondence by operations on safety properties and priorities. Finally, we provide an example illustrating an application of the results


Published in:
Formal Methods for Components and Objects. Second International Symposium, FMCO 2003. Revised Lectures (Lecture Notes in Computer Science Vol.3188), 314 - 29
Presented at:
Formal Methods for Components and Objects. Second International Symposium, FMCO 2003. Revised Lectures (Lecture Notes in Computer Science Vol.3188), Berlin, Germany
Year:
2004
Keywords:
Laboratories:




 Record created 2013-03-14, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)