@inproceedings{4477,
  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.},
  author       = {Henzinger, Thomas A and Minea, Marius and Prabhu, Vinayak},
  booktitle    = {Proceedings of the 4th International Workshop on Hybrid Systems},
  isbn         = {9783540418665},
  location     = {Rome, Italy},
  pages        = {275 -- 290},
  publisher    = {Springer},
  title        = {{Assume-guarantee reasoning for hierarchical hybrid systems}},
  doi          = {10.1007/3-540-45351-2_24},
  volume       = {2034},
  year         = {2001},
}