CHASE: Contract-Based Requirement Engineering for Cyber-Physical System Design

被引：0
作者：
Nuzzo, Pierluigi [1 ]
Lora, Michele [2 ]
Feldman, Yishai A. [3 ]
Sangiovanni-Vincentelli, Alberto L. [4 ]
机构：
[1] Univ Southern Calif, Dept Elect Engn, Los Angeles, CA USA
[2] Univ Verona, Dept Comp Sci, Verona, Italy
[3] IBM Res, Haifa, Israel
[4] Univ Calif Berkeley, Dept Elect Engn & Comp Sci, Berkeley, CA 94720 USA
来源：
PROCEEDINGS OF THE 2018 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE) | 2018年
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
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.
引用
收藏
页码：839 / 844
页数：6
相关论文
共 23 条
  • [1] [Anonymous], IBM J RES DEV
  • [2] [Anonymous], MODEL CHECKING
  • [3] Badger J, 2014, INT REQUIR ENG CONF, P325, DOI 10.1109/RE.2014.6912279
  • [4] Benveniste Albert., 2012, Research Report RR-8147, P65
  • [5] Caillaud Benoit, 2011, MICA MODAL INTERFACE
  • [6] Castillos K.C., 2013, IFM 2013, V7940, P316, DOI [10.1007/978-3-642-38613-822, DOI 10.1007/978-3-642-38613-822]
  • [7] Contracts-refinement proof system for component-based embedded systems
    Cimatti, Alessandro
    Tonetta, Stefano
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2015, 97 : 333 - 348
  • [8] Cimatti A, 2009, LECT NOTES COMPUT SC, V5643, P188, DOI 10.1007/978-3-642-02658-4_17
  • [9] Damm W, 2011, DES AUT TEST EUROPE, P1023
  • [10] Dwyer M. B., 1999, Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No.99CB37002), P411, DOI 10.1109/ICSE.1999.841031
123