Assume-Guarantee Reasoning for Hierarchical Hybrid Systems

Abstract. The assume-guarantee paradigm is a powerful divide-andconquer mechanism for decomposing a veri cation task about a system into subtasks about the individual components of the system. The key to assume-guaranteereasoning 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 forpurelysequentialcontexts,whichconstraintheentrycon gurationsof 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 parallelserial contexts. Our model also supports both discrete and continuous processes, and is therefore well-suited for the modeling and analysis of embeddedsoftwaresystemswhich interactwith real-worldenvironments. Using an exampleof twocooperatingrobot...

• Type: Conference
• Year: 2001
• Where: HYBRID
• Authors: Thomas A. Henzinger, Marius Minea, Vinayak S. Prabhu
• Keywords: Assume-guarantee Principle, Control Systems, HYBRID 2001, Powerful Divide-andconquer Mechanism, Veri Cation Task