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. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Henzinger, T. A., Minea, M., & Prabhu, V. (2001). Assume-guarantee reasoning for hierarchical hybrid systems. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2034, 275–290. https://doi.org/10.1007/3-540-45351-2_24
Mendeley helps you to discover research relevant for your work.