Optimizing Assume-Guarantee Contracts for Cyber-Physical System Design
Chanwook Oh1,a, Eunsuk Kang2, Shinichi Shiraishi3 and Pierluigi Nuzzo1,b
1Department of Electrical Engineering, University of Southern California, Los Angeles
achanwooo@usc.edu
bnuzzo@usc.edu
2School of Computer Science, Carnegie Mellon University, Pittsburgh
eskang@cmu.edu
3Toyota InfoTechnology Center, Mountain View
sshiraishi@us.toyota-itc.com
ABSTRACT
Assume-guarantee (A/G) contracts are mathematical models enabling modular and hierarchical design and verification of complex systems by rigorous decomposition of systemlevel 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 noncooperative 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.
