Sciweavers

FORMATS
2004
Springer

Decomposing Verification of Timed I/O Automata

13 years 7 months ago
Decomposing Verification of Timed I/O Automata
This paper presents assume-guarantee style substitutivity results for the recently published timed I/O automaton modeling framework. These results are useful for decomposing verification of systems where the implementation and the specification are represented as timed I/O automata. We first present a theorem that is applicable in verification tasks in which system specifications express safety properties. This theorem has an interesting corollary that involves the use of auxiliary automata in simplifying the proof obligations. We then derive a new result that shows how the same technique can be applied to the case where system specifications express liveness properties.
Dilsun Kirli Kaynar, Nancy A. Lynch
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2004
Where FORMATS
Authors Dilsun Kirli Kaynar, Nancy A. Lynch
Comments (0)