Assume/Guarantee Contracts for Dynamical Systems: Theory and Computational Tools

Miel Sharf, Bart Besselink*, Adam Molin, Qiming Zhao, Karl Henrik Johansson

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

13 Downloads (Pure)

Abstract

Modern engineering systems include many components of different types and functions. Verifying that these systems satisfy given specifications can be an arduous task, as most formal verification methods are limited to systems of moderate size. Recently, contract theory has been proposed as a modular framework for defining specifications. In this paper, we present a contract theory for discrete-time dynamical control systems relying on assume/guarantee contracts, which prescribe assumptions on the input of the system and guarantees on the output. We then focus on contracts defined by linear constraints, and develop efficient computational tools for verification of satisfaction and refinement based on linear programming. We exemplify these tools in a simulation example, proving a certain safety specification for a two-vehicle autonomous driving setting.
Original languageEnglish
Title of host publicationProceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems, Brussels, Belgium
EditorsRaphaël M. Jungers, Necmiye Ozay
PublisherElsevier
Pages25-30
Number of pages6
DOIs
Publication statusPublished - 2021
Event7th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2021 - Brussels, Belgium
Duration: 7-Jul-20219-Jul-2021

Publication series

NameIFAC-PapersOnLine
PublisherELSEVIER
Number5
Volume54
ISSN (Print)2405-8963

Conference

Conference7th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2021
Country/TerritoryBelgium
CityBrussels
Period07/07/202109/07/2021

Cite this