Liveness in timed and untimed systems (Q1271471)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Liveness in timed and untimed systems |
scientific article |
Statements
Liveness in timed and untimed systems (English)
0 references
10 November 1998
0 references
When proving the correctness of algorithms in distributed systems, one generally considers safety conditions and liveness conditions. The Input/Output (I/O) automaton model and its timed version have been used successfully, but have focused on safety conditions and on a restricted form of liveness called fairness. In this paper, we develop a new I/O automaton model, and a new timed I/O automaton model, that permit the verification of general liveness properties on the basis of existing verification techniques. Our models include a notion of receptiveness which extends the idea of receptiveness of other existing formalisms, and enables the use of compositional verification techniques. The presentation includes an embedding of the untimed model into the timed model which preserves all the interesting attributes of the untimed model. Thus, our models constitute a coordinated framework for the description of concurrent and distributed systems satisfying general liveness properties. \(\copyright\) Academic Press.
0 references
safety
0 references
liveness
0 references
receptiveness
0 references