## Assume-guarantee Reasoning for Hierarchical Hybrid Systems

*
Thomas A. Henzinger,
Marius Minea, and Vinayak Prabhu*

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.

*Proceedings of the
Fourth International Workshop on Hybrid Systems: Computation and Control*
(HSCC),
Lecture Notes in Computer Science 2034,
Springer, 2001, pp. 275-290.

Download inofficial, sometimes updated
PostScript /
PDF document.
© 2001 Springer.