conference paper
Assume-guarantee reasoning for hierarchical hybrid systems
LNCS
published
yes
Thomas A
Henzinger
author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724
Marius
Minea
author
Vinayak
Prabhu
author
HSCC: Hybrid Systems - Computation and Control
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.
Springer2001Rome, Italy
eng
Proceedings of the 4th International Workshop on Hybrid Systems
978354041866510.1007/3-540-45351-2_24
2034275 - 290
yes
Henzinger, Thomas A, Marius Minea, and Vinayak Prabhu. “Assume-Guarantee Reasoning for Hierarchical Hybrid Systems.” In <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>, 2034:275–90. Springer, 2001. <a href="https://doi.org/10.1007/3-540-45351-2_24">https://doi.org/10.1007/3-540-45351-2_24</a>.
Henzinger, T. A., Minea, M., & Prabhu, V. (2001). Assume-guarantee reasoning for hierarchical hybrid systems. In <i>Proceedings of the 4th International Workshop on Hybrid Systems</i> (Vol. 2034, pp. 275–290). Rome, Italy: Springer. <a href="https://doi.org/10.1007/3-540-45351-2_24">https://doi.org/10.1007/3-540-45351-2_24</a>
T. A. Henzinger, M. Minea, and V. Prabhu, “Assume-guarantee reasoning for hierarchical hybrid systems,” in <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>, Rome, Italy, 2001, vol. 2034, pp. 275–290.
T.A. Henzinger, M. Minea, V. Prabhu, in:, Proceedings of the 4th International Workshop on Hybrid Systems, Springer, 2001, pp. 275–290.
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.
Henzinger TA, Minea M, Prabhu V. Assume-guarantee reasoning for hierarchical hybrid systems. In: <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>. Vol 2034. Springer; 2001:275-290. doi:<a href="https://doi.org/10.1007/3-540-45351-2_24">10.1007/3-540-45351-2_24</a>
Henzinger, Thomas A., et al. “Assume-Guarantee Reasoning for Hierarchical Hybrid Systems.” <i>Proceedings of the 4th International Workshop on Hybrid Systems</i>, vol. 2034, Springer, 2001, pp. 275–90, doi:<a href="https://doi.org/10.1007/3-540-45351-2_24">10.1007/3-540-45351-2_24</a>.
44772018-12-11T12:09:03Z2023-05-09T14:47:37Z