FORMATS-FTRTFT 2004 START ConferenceManager    

Decomposing Verification of Timed I/O Automata

Dilsun Kaynar and Nancy Lynch

Presented at Formal Modelling and Analysis of Timed Systems - Formal Techniques in Real-Time and Fault Tolerant System (FORMATS-FTRTFT 2004), Grenoble, France, September 22-24, 2004


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.

START Conference Manager (V2.47.2)