Pierluigi Nuzzo, Nikunj Bajaj, et al.
IEEE TCADIS
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.
Pierluigi Nuzzo, Nikunj Bajaj, et al.
IEEE TCADIS
Yishai A. Feldman
CSDM 2014
Georgios Karakonstantis, Konstantinos Tovletoglou, et al.
DATE 2018
Benjamin Uhlig, Jie Liang, et al.
DATE 2018