CHASE: Contract‐Based Requirement Engineering for Cyber‐Physical System Design
Pierluigi Nuzzo1, Michele Lora2, Yishai A. Feldman3 and Alberto L. Sangiovanni-Vincentelli4
1University of Southern California, Los Angeles
nuzzo@usc.edu
2University of Verona, Italy
michele.lora@univr.it
3IBM Research, Haifa, Israel.
yishai@il.ibm.com
4University of California, Berkeley
alberto@berkeley.edu
ABSTRACT
This paper presents CHASE, a framework for requirement capture, formalization, and validation for cyber physical systems. CHASE combines a practical front‐end formal specification language based on patterns with a rigorous verification back‐end based on assume‐guarantee contracts. The front‐end language can express temporal properties of networks using a declarative style, and supports automatic translation from natural‐language constructs to low‐level mathematical languages. The verification back‐end leverages the mathematical formalism of contracts to reason about system requirements and determine inconsistencies and dependencies between them. CHASE features a modular and extensible software infrastructure that can support different domain‐specific languages, modeling formalisms, and analysis tools. We illustrate its effectiveness on industrial design examples, including control of aircraft power distribution networks and arbitration of a mixed‐criticality automotive bus.
