Name
Abstract | ||
|---|---|---|
This paper presents CHASE, a framework for requirement capture, formalization, and validation for cyberphysical 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. |
Year | Venue | Field |
|---|---|---|
2018 | PROCEEDINGS OF THE 2018 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE) | Industrial design,Software engineering,Computer science,Requirements engineering,Formal specification,Real-time computing,Cyber-physical system,Electronic design automation,Modular design,System requirements,Rotation formalisms in three dimensions |
DocType | ISSN | Citations |
Conference | 1530-1591 | 1 |
PageRank | References | Authors |
0.35 | 0 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Pierluigi Nuzzo | 1 | 305 | 33.35 |
| Michele Lora | 2 | 32 | 11.13 |
| Yishai A. Feldman | 3 | 282 | 49.29 |
| Alberto L. Sangiovanni-Vincentelli | 4 | 11385 | 1881.40 |