Formal Verification of Timed Systems Using Cones and Foci

W.J. Fokkink, J. Pang

Research output: Contribution to JournalArticleAcademicpeer-review


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. © 2005 Elsevier B.V. All rights reserved.
Original languageEnglish
Pages (from-to)105-122
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 2005

Bibliographical note

Proceedings title: Proceedings of the 6th AMAST Workshop on Real-Time Systems (ARTS 2004)
Publisher: Elsevier


Dive into the research topics of 'Formal Verification of Timed Systems Using Cones and Foci'. Together they form a unique fingerprint.

Cite this