Formal Requirement Debugging for Testing and Verification of Cyber-Physical Systems

被引：15
|
作者：
Dokhanchi, Adel [1 ]
Hoxha, Bardh [2 ]
Fainekos, Georgios [1 ]
机构：
[1] Arizona State Univ, Sch Comp Informat & Decis Syst Engn, Tempe, AZ 85281 USA
[2] Southern Illinois Univ, Dept Comp Sci, Carbondale, IL 62901 USA
来源：
ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS | 2018年 / 17卷 / 02期
基金：
美国国家科学基金会;
关键词：
MITL; SAT; LTL; STL; SMT; CPS; TEMPORAL PROPERTIES; SATISFIABILITY; VACUITY;
D O I：
10.1145/3147451
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
A framework for the elicitation and debugging of formal specifications for Cyber-Physical Systems is presented. The elicitation of specifications is handled through a graphical interface. Two debugging algorithms are presented. The first checks for erroneous or incomplete temporal logic specifications without considering the system. The second can be utilized for the analysis of reactive requirements with respect to system test traces. The specification debugging framework is applied on a number of formal specifications collected through a user study. The user study establishes that requirement errors are common and that the debugging framework can resolve many insidious specification errors.
引用
收藏
页数：26
相关论文
共 50 条
  • [21] Statistical Verification of Hyperproperties for Cyber-Physical Systems
    Wang, Yu
    Zarei, Mojtaba
    Bonakdarpour, Borzoo
    Pajic, Miroslav
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2019, 18 (05)
  • [22] Ensuring the federation correctness: Formal verification of Federated Learning in industrial cyber-physical systems
    Guendouzi, Badra Souhila
    Ouchani, Samir
    Al Assaad, Hiba
    El Zaher, Madeleine
    FUTURE GENERATION COMPUTER SYSTEMS-THE INTERNATIONAL JOURNAL OF ESCIENCE, 2025, 166
  • [23] Towards Foundational Verification of Cyber-physical Systems
    Malecha, Gregory
    Ricketts, Daniel
    Alvarez, Mario M.
    Lerner, Sorin
    2016 SCIENCE OF SECURITY FOR CYBER-PHYSICAL SYSTEMS WORKSHOP (SOSCYPS), 2016,
  • [24] Towards Verification of Uncertain Cyber-Physical Systems
    Radojicic, Carna
    Grimm, Christoph
    Jantsch, Axel
    Rathmair, Michael
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (247): : 1 - 17
  • [25] A Hybrid Approach to Cyber-Physical Systems Verification
    Kumar, Pratyush
    Goswami, Dip
    Chakraborty, Samarjit
    Annaswamy, Anuradha
    Lampka, Kai
    Thiele, Lothar
    2012 49TH ACM/EDAC/IEEE DESIGN AUTOMATION CONFERENCE (DAC), 2012, : 688 - 696
  • [26] BraceAssertion: Runtime Verification of Cyber-Physical Systems
    Zheng, Xi
    Julien, Christine
    Podorozhny, Rodion
    Cassez, Franck
    2015 IEEE 12th International Conference on Mobile Ad Hoc and Sensor Systems (MASS), 2015, : 298 - 306
  • [27] Modeling Cyber-Physical Systems for Automatic Verification
    Driouich, Youssef
    Parente, Mimmo
    Tronci, Enrico
    2017 14TH INTERNATIONAL CONFERENCE ON SYNTHESIS, MODELING, ANALYSIS AND SIMULATION METHODS AND APPLICATIONS TO CIRCUIT DESIGN (SMACD), 2017,
  • [28] Boosting Simulation and Debugging of Cyber-physical Systems with Symbolic Exploration
    Kolesnikov, Ivan
    Ada User Journal, 2022, 43 (03):
  • [29] Cyber/Physical Co-Verification for Developing Reliable Cyber-Physical Systems
    Zhang, Yu
    Xie, Fei
    Dong, Yunwei
    Zhou, Xingshe
    Ma, Chunyan
    2013 IEEE 37TH ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 2013, : 539 - 548
  • [30] Formal methods for reconfigurable cyber-physical systems in production
    Grochowski, Marco
    Simon, Hendrik
    Bohlender, Dimitri
    Kowalewski, Stefan
    Loecklin, Andreas
    Mueller, Timo
    Jazdi, Nasser
    Und, Andreas Zeller
    Weyrich, Michael
    AT-AUTOMATISIERUNGSTECHNIK, 2020, 68 (01) : 3 - 14
12345