### 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 |

Publisher | Springer-Verlag |

Pages | 356-371 |

Number of pages | 16 |

ISBN (Electronic) | 9783540462194 |

ISBN (Print) | 3540462198, 9783540462194 |

State | Published - Jan 1 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 | France |

City | Paris |

Period | 9/26/06 → 9/29/06 |

### Fingerprint

### ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)

### Cite this

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

**Liveness by invisible invariants.** / Fang, Yi; McMillan, Kenneth L.; Pnueli, Amir; Zuck, Lenore D.

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

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

}

TY - GEN

T1 - Liveness by invisible invariants

AU - Fang, Yi

AU - McMillan, Kenneth L.

AU - Pnueli, Amir

AU - Zuck, Lenore D.

PY - 2006/1/1

Y1 - 2006/1/1

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

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

PB - Springer-Verlag

ER -