Verifying Compositional Refinement of Assume/Guarantee Contracts using Linear Programming

TL;DR

This paper introduces a linear programming-based method to verify that component-level contracts in large systems correctly refine to system-level contracts, enhancing modular verification efficiency.

Contribution

It extends assume/guarantee contracts with necessary and sufficient conditions for refinement, verified via scalable linear programs, demonstrated through a vehicle safety case study.

Findings

Linear programs verify contract refinement efficiently.

Conditions grow linearly with the number of contracts.

Case study confirms practical applicability.

Abstract

Verifying specifications for large-scale modern engineering systems can be a time-consuming task, as most formal verification methods are limited to systems of modest size. Recently, contract-based design and verification has been proposed as a modular framework for specifications, and linear-programming-based techniques have been presented for verifying that a given system satisfies a given contract. In this paper, we extend this assume/guarantee framework by presenting necessary and sufficient conditions for a collection of contracts on individual components to refine a contract on the composed system. These conditions can be verified by solving linear programs, whose number grows linearly with the number of specifications defined by the contracts. We exemplify the tools developed using a case study considering safety in a car-following scenario, where noise and time-varying delay are considered.