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.
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.