Formal Verification of Timed Systems Using Cones and Foci

W.J. Fokkink; J. Pang

doi:10.1016/j.entcs.2005.09.003

Formal Verification of Timed Systems Using Cones and Foci

Research output: Contribution to Journal › Article › Academic › peer-review

Abstract

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 language	English
Pages (from-to)	105-122
Journal	Electronic Notes in Theoretical Computer Science
Volume	139
DOIs	https://doi.org/10.1016/j.entcs.2005.09.003
Publication status	Published - 2005

Bibliographical note

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

Access to Document

10.1016/j.entcs.2005.09.003

Cite this

@article{84e5cfbdb4d6426ba007075d1ee55eb8,

title = "Formal Verification of Timed Systems Using Cones and Foci",

abstract = "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. {\textcopyright} 2005 Elsevier B.V. All rights reserved.",

author = "W.J. Fokkink and J. Pang",

note = "DBLP:journals/entcs/FokkinkP05a Proceedings title: Proceedings of the 6th AMAST Workshop on Real-Time Systems (ARTS 2004) Publisher: Elsevier",

year = "2005",

doi = "10.1016/j.entcs.2005.09.003",

language = "English",

volume = "139",

pages = "105--122",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

}

TY - JOUR

T1 - Formal Verification of Timed Systems Using Cones and Foci

AU - Fokkink, W.J.

AU - Pang, J.

N1 - DBLP:journals/entcs/FokkinkP05a Proceedings title: Proceedings of the 6th AMAST Workshop on Real-Time Systems (ARTS 2004) Publisher: Elsevier

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

U2 - 10.1016/j.entcs.2005.09.003

DO - 10.1016/j.entcs.2005.09.003

M3 - Article

VL - 139

SP - 105

EP - 122

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

ER -

Formal Verification of Timed Systems Using Cones and Foci

Abstract

Bibliographical note

Access to Document

Fingerprint

Cite this