Layering Assume-guarantee Contracts for Hierarchical System Design

  • Authors:
    Ioannis Filippidis (Caltech), Richard Murray (Caltech)
    Publication ID:
    Publication Type:
    Received Date:
    Last Edit Date:
    2386.004 (University of California/Berkeley)


Specifications for complex engineering systems are typically decomposed into specifications for individual subsystems in a manner that ensures they are implementable and simpler to develop further. We describe a method to algorithmically construct component specifications that implement a given specification when assembled. By eliminating variables that are irrelevant to realizability of each component, we simplify the specifications and reduce the amount of information necessary for operation. To identify which variables can be hidden while preserving realizability, we parameterize the information flow between components, and eliminate the selected variables from component specifications. The resulting specifications describe component viewpoints with full information with respect to the remaining variables, which is essential for tractable algorithmic synthesis of implementations. The specifications are written in TLA+, with liveness properties restricted to an implication of conjoined recurrence properties, known as GR(1). We define an operator for forming open-systems from closed-systems, based on a variant of the "while-plus" operator. The resulting open-system properties are realizable when expected to be, without need for separate side conditions. To convert the generated specifications from binary decision diagrams to readable formulas over integer variables, we symbolically solve a minimal covering problem. We show with examples how the method can be applied to obtain contracts that formalize the hierarchical structure of system design.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.