TY - JOUR
T1 - Contract composition for dynamical control systems
T2 - Definition and verification using linear programming
AU - Sharf, Miel
AU - Besselink, Bart
AU - Johansson, Karl Henrik
N1 - Publisher Copyright:
© 2024 Elsevier Ltd
PY - 2024/6
Y1 - 2024/6
N2 - 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.
AB - 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.
KW - Contracts
KW - Formal methods
KW - Graph theory
KW - Interconnection topology
KW - Linear programming
KW - Modular design
UR - http://www.scopus.com/inward/record.url?scp=85189076874&partnerID=8YFLogxK
U2 - 10.1016/j.automatica.2024.111637
DO - 10.1016/j.automatica.2024.111637
M3 - Article
AN - SCOPUS:85189076874
SN - 0005-1098
VL - 164
JO - Automatica
JF - Automatica
M1 - 111637
ER -