@inproceedings{ee188b7952ca4461859ecaea73214fed,
title = "Assume/Guarantee Contracts for Dynamical Systems: Theory and Computational Tools",
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.",
author = "Miel Sharf and Bart Besselink and Adam Molin and Qiming Zhao and Johansson, {Karl Henrik}",
year = "2021",
doi = "10.1016/j.ifacol.2021.08.469",
language = "English",
series = "IFAC-PapersOnLine",
publisher = "Elsevier",
number = "5",
pages = "25--30",
editor = "{ Jungers}, {Rapha{\"e}l M.} and { Ozay}, {Necmiye }",
booktitle = "Proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems, Brussels, Belgium",
note = "7th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2021 ; Conference date: 07-07-2021 Through 09-07-2021",
}