Contract composition for dynamical control systems: Definition and verification using linear programming

Designing large-scale control systems to satisfy complex specifications is hard in practice, as most formal methods are limited to systems of modest size. Contract theory has been proposed as a modular alternative, in which specifications are defined by assumptions on the input to a component and guarantees on its output. However, current contract-based methods for control systems either prescribe guarantees on the state of the system, going against the spirit of contract theory, or are not supported by efficient computational tools. In this paper, we present a contract-based modular framework for discrete-time dynamical control systems. We extend the definition of contracts by allowing the assumption on the input at a time k to depend on outputs up to time k−1, which is essential when considering feedback systems. We also define contract composition for arbitrary interconnection topologies, and prove that this notion supports modular design, analysis and verification. This is done using graph theory methods, and specifically using the notions of topological ordering and backward-reachable nodes. Lastly, we present an algorithm for verifying vertical contracts, which are claims of the form “the conjunction of given component-level contracts implies given contract on the integrated system”. These algorithms are based on linear programming, and scale linearly with the number of components in the interconnected network. A numerical example is provided to demonstrate the scalability of the presented approach, as well as the modularity achieved by using it.