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 -