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

TL;DR

This paper develops a contract-based framework for verifying discrete-time dynamical systems using assume/guarantee contracts, with computational tools for linear constraints, demonstrated on autonomous vehicle safety.

Contribution

It introduces a novel contract theory for discrete-time systems and provides efficient linear programming tools for verification and refinement.

Findings

Verification of safety specifications achieved via linear programming.

Contract-based approach enables modular system verification.

Application demonstrated on autonomous vehicle safety scenario.

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.