Assume-guarantee reasoning for hybrid I/O-automata by over-approximation of continuous interaction
- 1 January 2004
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 527 (01912216) , 479-484 Vol.1
- https://doi.org/10.1109/cdc.2004.1428676
Abstract
Assume-guarantee reasoning (AGR) is recognized as a means to counter the state explosion problem in the verification of safety properties. We propose a novel assume-guarantee rule for hybrid systems based on simulation relations. This makes it possible to perform compositional reasoning that is conservative in the sense of over-approximating the composed behaviors. The framework is formally based on hybrid input/output automata and their labeled transition system semantics. In contrast to previous approaches that require global receptivity conditions, the circularity is broken in our approach by a state-based nonblocking condition that can be checked in the course of computing the AGR simulation relations. The proposed procedures for AGR are implemented in a computational tool, called PHAVer, for the class of linear hybrid I/O automata, and the approach is illustrated with a simple example.Keywords
This publication has 8 references indexed in Scilit:
- Compositional verification of hybrid systems with discrete interaction using simulation relationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2005
- Hybrid I/O automataInformation and Computation, 2003
- The theory of hybrid automataPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Computing simulations on finite and infinite graphsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- An assume-guarantee rule for checking simulationACM Transactions on Programming Languages and Systems, 2002
- Assume-Guarantee Reasoning for Hierarchical Hybrid SystemsPublished by Springer Nature ,2001
- The algorithmic analysis of hybrid systemsTheoretical Computer Science, 1995
- Hybrid automata: An algorithmic approach to the specification and verification of hybrid systemsPublished by Springer Nature ,1993