Liveness by invisible invariants

Yi Fang; Kenneth L. McMillan; Amir Pnueli; Lenore D. Zuck

doi:10.1007/11888116_26

Liveness by invisible invariants

Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

The method of Invisible Invariants was developed in order to verify safety properties of parametrized systems in a fully automatic manner. In this paper, we apply the method of invisible invariant to "bounded response" properties, i.e., liveness properties of the type p q that are bounded - once a p-state is reached, it takes a bounded number of rounds (where a round is a sequence of steps in which each process has been given a chance to proceed) to reach a q-state - thus, they are essentially safety properties. With a "liveness monitor" that observes certain behavior of a system, establishing "bounded response" properties over the system is reduced to the verification of invariant properties. It is often the case that the inductive invariants for systems with "liveness monitors" contain assertions of a certain form that the original method of invisible invariant is not able to generate, nor to check inductiveness. To accommodate invariants of such forms, we extend the techniques used for invariant generation, as well as the small model theorem for validity check.

Original language	English (US)
Title of host publication	Formal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings
Editors	Elie Najm, Jean-François Pradat-Peyre, Véronique Viguié Donzeau-Gouge
Publisher	Springer Verlag
Pages	356-371
Number of pages	16
ISBN (Print)	3540462198, 9783540462194
DOIs	https://doi.org/10.1007/11888116_26
State	Published - 2006
Event	26th IFIP WG 6.1 International Conference - Paris, France Duration: Sep 26 2006 → Sep 29 2006

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4229 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	26th IFIP WG 6.1 International Conference
Country/Territory	France
City	Paris
Period	9/26/06 → 9/29/06

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/11888116_26

Cite this

Fang, Y., McMillan, K. L., Pnueli, A., & Zuck, L. D. (2006). Liveness by invisible invariants. In E. Najm, J.-F. Pradat-Peyre, & V. V. Donzeau-Gouge (Eds.), Formal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings (pp. 356-371). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4229 LNCS). Springer Verlag. https://doi.org/10.1007/11888116_26

Liveness by invisible invariants. / Fang, Yi; McMillan, Kenneth L.; Pnueli, Amir et al.
Formal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings. ed. / Elie Najm; Jean-François Pradat-Peyre; Véronique Viguié Donzeau-Gouge. Springer Verlag, 2006. p. 356-371 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4229 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Fang, Y, McMillan, KL, Pnueli, A & Zuck, LD 2006, Liveness by invisible invariants. in E Najm, J-F Pradat-Peyre & VV Donzeau-Gouge (eds), Formal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4229 LNCS, Springer Verlag, pp. 356-371, 26th IFIP WG 6.1 International Conference, Paris, France, 9/26/06. https://doi.org/10.1007/11888116_26

Fang Y, McMillan KL, Pnueli A, Zuck LD. Liveness by invisible invariants. In Najm E, Pradat-Peyre JF, Donzeau-Gouge VV, editors, Formal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings. Springer Verlag. 2006. p. 356-371. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11888116_26

Fang, Yi ; McMillan, Kenneth L. ; Pnueli, Amir et al. / Liveness by invisible invariants. Formal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings. editor / Elie Najm ; Jean-François Pradat-Peyre ; Véronique Viguié Donzeau-Gouge. Springer Verlag, 2006. pp. 356-371 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{713b8a718ce44f4382f3b5ab75071074,

title = "Liveness by invisible invariants",

abstract = "The method of Invisible Invariants was developed in order to verify safety properties of parametrized systems in a fully automatic manner. In this paper, we apply the method of invisible invariant to {"}bounded response{"} properties, i.e., liveness properties of the type p q that are bounded - once a p-state is reached, it takes a bounded number of rounds (where a round is a sequence of steps in which each process has been given a chance to proceed) to reach a q-state - thus, they are essentially safety properties. With a {"}liveness monitor{"} that observes certain behavior of a system, establishing {"}bounded response{"} properties over the system is reduced to the verification of invariant properties. It is often the case that the inductive invariants for systems with {"}liveness monitors{"} contain assertions of a certain form that the original method of invisible invariant is not able to generate, nor to check inductiveness. To accommodate invariants of such forms, we extend the techniques used for invariant generation, as well as the small model theorem for validity check.",

author = "Yi Fang and McMillan, {Kenneth L.} and Amir Pnueli and Zuck, {Lenore D.}",

year = "2006",

doi = "10.1007/11888116_26",

language = "English (US)",

isbn = "3540462198",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "356--371",

editor = "Elie Najm and Jean-Fran{\c c}ois Pradat-Peyre and Donzeau-Gouge, {V{\'e}ronique Vigui{\'e}}",

booktitle = "Formal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings",

note = "26th IFIP WG 6.1 International Conference ; Conference date: 26-09-2006 Through 29-09-2006",

}

TY - GEN

T1 - Liveness by invisible invariants

AU - Fang, Yi

AU - McMillan, Kenneth L.

AU - Pnueli, Amir

AU - Zuck, Lenore D.

PY - 2006

Y1 - 2006

N2 - The method of Invisible Invariants was developed in order to verify safety properties of parametrized systems in a fully automatic manner. In this paper, we apply the method of invisible invariant to "bounded response" properties, i.e., liveness properties of the type p q that are bounded - once a p-state is reached, it takes a bounded number of rounds (where a round is a sequence of steps in which each process has been given a chance to proceed) to reach a q-state - thus, they are essentially safety properties. With a "liveness monitor" that observes certain behavior of a system, establishing "bounded response" properties over the system is reduced to the verification of invariant properties. It is often the case that the inductive invariants for systems with "liveness monitors" contain assertions of a certain form that the original method of invisible invariant is not able to generate, nor to check inductiveness. To accommodate invariants of such forms, we extend the techniques used for invariant generation, as well as the small model theorem for validity check.

AB - The method of Invisible Invariants was developed in order to verify safety properties of parametrized systems in a fully automatic manner. In this paper, we apply the method of invisible invariant to "bounded response" properties, i.e., liveness properties of the type p q that are bounded - once a p-state is reached, it takes a bounded number of rounds (where a round is a sequence of steps in which each process has been given a chance to proceed) to reach a q-state - thus, they are essentially safety properties. With a "liveness monitor" that observes certain behavior of a system, establishing "bounded response" properties over the system is reduced to the verification of invariant properties. It is often the case that the inductive invariants for systems with "liveness monitors" contain assertions of a certain form that the original method of invisible invariant is not able to generate, nor to check inductiveness. To accommodate invariants of such forms, we extend the techniques used for invariant generation, as well as the small model theorem for validity check.

UR - http://www.scopus.com/inward/record.url?scp=33750567735&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33750567735&partnerID=8YFLogxK

U2 - 10.1007/11888116_26

DO - 10.1007/11888116_26

M3 - Conference contribution

AN - SCOPUS:33750567735

SN - 3540462198

SN - 9783540462194

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 356

EP - 371

BT - Formal Techniques for Networked and Distributed Systems - FORTE 2006 - 26th IFIP WG 6.1 International Conference, Proceedings

A2 - Najm, Elie

A2 - Pradat-Peyre, Jean-François

A2 - Donzeau-Gouge, Véronique Viguié

PB - Springer Verlag

T2 - 26th IFIP WG 6.1 International Conference

Y2 - 26 September 2006 through 29 September 2006

ER -

Liveness by invisible invariants

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this