Composition of behavioural assume-guarantee contracts

Brayan M. Shali*, Arjan van der Schaft, Bart Besselink

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

19 Downloads (Pure)

Abstract

The growing complexity of modern engineering systems necessitates a method for design and analysis that is inherently modular. Methods based on using contracts for system design have successfully tackled this issue for a variety of system classes, but mostly in the context of discrete software systems. Motivated by this, we present assume-guarantee contracts for continuous linear dynamical systems with inputs and outputs. Such contracts serve as system specifications through two aspects. The assumptions specify the dynamic behaviour of the environment of the system, which provides inputs for it, while the guarantees specify the desired dynamic behaviour of the output of the system when interconnected with a relevant environment. This is formalized by utilizing the behavioural approach to system theory. We define and characterize notions of contract implementation and contract refinement, where the latter is used to compare contracts. We also define and characterize two notions of contract composition that allow one to reason about two types of system interconnections: series and feedback. The properties of refinement and composition allow contracts to be used for modular design and analysis.

Original languageEnglish
Pages (from-to)5991-6006
Number of pages16
JournalIEEE Transactions on Automatic Control
Volume68
Issue number10
Early online date30-Dec-2022
DOIs
Publication statusPublished - Oct-2023

Keywords

  • Contract-based design
  • Contracts
  • Decentralized control
  • Dynamical systems
  • interconnected systems
  • Interconnected systems
  • Linear systems
  • linear systems
  • modular design
  • Software systems
  • Trajectory

Cite this