# Assume-guarantee reasoning for hierarchical hybrid systems

Henzinger TA, Minea M, Prabhu V. 2001. Assume-guarantee reasoning for hierarchical hybrid systems. Proceedings of the 4th International Workshop on Hybrid Systems. HSCC: Hybrid Systems - Computation and Control, LNCS, vol. 2034, 275–290.

Download

**No fulltext has been uploaded. References only!**

*Conference Paper*|

*Published*|

*English*

**Scopus indexed**

Author

Henzinger, Thomas A

^{ISTA}^{}; Minea, Marius; Prabhu, VinayakSeries Title

LNCS

Abstract

The assume-guarantee paradigm is a powerful divide-and-conquer mechanism for decomposing a verification task about a system into subtasks about the individual components of the system. The key to assume-guarantee reasoning is to consider each component not in isolation, but in conjunction with assumptions about the context of the component. Assume-guarantee principles are known for purely concurrent contexts, which constrain the input data of a component, as well as for purely sequential contexts, which constrain the entry configurations of a component. We present a model for hierarchical system design which permits the arbitrary nesting of parallel as well as serial composition, and which supports an assume-guarantee principle for mixed parallel-serial contexts. Our model also supports both discrete and continuous processes, and is therefore well-suited for the modeling and analysis of embedded software systems which interact with real-world environments. Using an example of two cooperating robots, we show refinement between a high-level model which specifies continuous timing constraints and an implementation which relies on discrete sampling.

Publishing Year

Date Published

2001-03-14

Proceedings Title

Proceedings of the 4th International Workshop on Hybrid Systems

Acknowledgement

Support for this research was provided in part by the AFOSR MURI grant F49620- 00-1-0327, and the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the NSF ITR grant CCR-0085949.

Volume

2034

Page

275 - 290

Conference

HSCC: Hybrid Systems - Computation and Control

Conference Location

Rome, Italy

Conference Date

2001-03-28 – 2001-03-30

ISBN

IST-REx-ID

### Cite this

Henzinger TA, Minea M, Prabhu V. Assume-guarantee reasoning for hierarchical hybrid systems. In:

*Proceedings of the 4th International Workshop on Hybrid Systems*. Vol 2034. Springer; 2001:275-290. doi:10.1007/3-540-45351-2_24Henzinger, T. A., Minea, M., & Prabhu, V. (2001). Assume-guarantee reasoning for hierarchical hybrid systems. In

*Proceedings of the 4th International Workshop on Hybrid Systems*(Vol. 2034, pp. 275–290). Rome, Italy: Springer. https://doi.org/10.1007/3-540-45351-2_24Henzinger, Thomas A, Marius Minea, and Vinayak Prabhu. “Assume-Guarantee Reasoning for Hierarchical Hybrid Systems.” In

*Proceedings of the 4th International Workshop on Hybrid Systems*, 2034:275–90. Springer, 2001. https://doi.org/10.1007/3-540-45351-2_24.T. A. Henzinger, M. Minea, and V. Prabhu, “Assume-guarantee reasoning for hierarchical hybrid systems,” in

*Proceedings of the 4th International Workshop on Hybrid Systems*, Rome, Italy, 2001, vol. 2034, pp. 275–290.Henzinger, Thomas A., et al. “Assume-Guarantee Reasoning for Hierarchical Hybrid Systems.”

*Proceedings of the 4th International Workshop on Hybrid Systems*, vol. 2034, Springer, 2001, pp. 275–90, doi:10.1007/3-540-45351-2_24.