Formal Verification of Timed Systems Using Cones and Foci

The cones and foci verification method from Groote and Springintveld [J.F. Groote and J. Springintveld. Focus points and convergent process operators. A proof strategy for protocol verification. Journal of Logic and Algebraic Programming, 49(1/2): 31-60, 2001] was extended to timed systems by van der Zwaag [M.B. van der Zwaag. The cones and foci proof technique for timed transition systems. Information Processing Letters, 80(1): 33-40, 2001]. We present an extension of this cones and foci method for timed systems, which can cope with infinite τ-sequences. We prove soundness of our approach and give small verification examples.