SCIENCE@home

Optimizing Assume-Guarantee Contracts for Cyber-Physical System Design

Chanwook Oh,Eunsuk Kang,Shin'ichi Shiraishi,P. Nuzzo

Published 2019 in Design, Automation and Test in Europe

ABSTRACT

Assume-guarantee (A/G) contracts are mathematical models enabling modular and hierarchical design and verifi-cation of complex systems by rigorous decomposition of system-level specifications into component-level specifications. Existing A/G contract frameworks, however, are not designed to effectively capture the behaviors of cyber-physical systems where multiple agents aim to maximize one or more objectives, and may interact with each other and the environment in a cooperative or non-cooperative way toward achieving their goals. We propose an extension of the A/G contract framework, namely optimizing A/G contracts, that can be used to specify and reason about properties of component interactions that involve optimizing objectives. The proposed framework includes methods for constructing new contracts via conjunction and composition, along with algorithms to verify system properties via contract refinement. We illustrate its effectiveness on a set of case studies from connected and autonomous vehicles.

PUBLICATION RECORD

CITATION MAP

EXTRACTION MAP

CLAIMS

  • No claims are published for this paper.

CONCEPTS

  • No concepts are published for this paper.

REFERENCES

Showing 1-17 of 17 references · Page 1 of 1

CITED BY

Showing 1-7 of 7 citing papers · Page 1 of 1