Q: A Sound Verification Framework for Statecharts and Their Implementations

被引：1
|
作者：
Pollard, Samuel D. [1 ]
Armstrong, Robert C. [1 ]
Bender, John [1 ]
Hulette, Geoffrey C. [1 ]
Mahmood, Raheel S. [1 ]
Morris, Karla [1 ]
Rawlings, Blake C. [1 ]
Aytac, Jon M. [1 ]
机构：
[1] Sandia Natl Labs, Livermore, CA 87185 USA
来源：
PROCEEDINGS OF THE 8TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2022 | 2022年
关键词：
formal methods; state machines; C; specification languages; temporal logic; model checking;
D O I：
10.1145/3563822.3568014
中图分类号：
TP39 [计算机的应用];
学科分类号：
081203 ; 0835 ;
摘要：
We present Q Framework: a verification framework used at Sandia National Laboratories. Qis a collection of tools used to verify safety and correctness properties of high-consequence embedded systems and captures the structure and compositionality of system specifications written with state machines in order to prove system-level properties about their implementations. Q consists of two main workflows: 1) compilation of temporal properties and state machine models (such as those made with Stateflow) into SMV models and 2) generation of ACSL specifications for the C code implementation of the state machine models. These together prove a refinement relation between the state machine model and its C code implementation, with proofs of properties checked by NuSMV (for SMV models) and Frama-C (for ACSL specifications).
引用
收藏
页码：16 / 26
页数：11
相关论文
共 50 条
  • [41] Formal verification of parametric multiplicative division implementations
    Kikkeri, N
    Seidel, PM
    2005 IEEE INTERNATIONAL CONFERENCE ON COMPUTER DESIGN: VLSI IN COMPUTERS & PROCESSORS, PROCEEDINGS, 2005, : 599 - 602
  • [42] Equivalence verification of FPGA and structured ASIC implementations
    Pistorius, Joachim
    Hutton, Mike
    Schleicher, Jay
    Lotov, Mihail
    Julias, Enoch
    Tharmalingam, Kumara
    2007 INTERNATIONAL CONFERENCE ON FIELD PROGRAMMABLE LOGIC AND APPLICATIONS, PROCEEDINGS, VOLS 1 AND 2, 2007, : 423 - 428
  • [43] Statecharts for reconfigurable control of complex reactive systems: A new formal verification methodology
    Dewasurendra, S. Devapriya
    2006 International Conference on Industrial and Information Systems, Vols 1 and 2, 2006, : 274 - 278
  • [44] Formal verification of security protocol implementations: a survey
    Avalle, Matteo
    Pironti, Alfredo
    Sisto, Riccardo
    FORMAL ASPECTS OF COMPUTING, 2014, 26 (01) : 99 - 123
  • [45] SOFTWARE IMPLEMENTATIONS OF THE Q-CODER
    MITCHELL, JL
    PENNEBAKER, WB
    IBM JOURNAL OF RESEARCH AND DEVELOPMENT, 1988, 32 (06) : 753 - 774
  • [46] Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification
    Gruer, JP
    Hilaire, V
    Koukam, A
    Rovarini, P
    JOURNAL OF SYSTEMS AND SOFTWARE, 2004, 70 (1-2) : 95 - 105
  • [47] Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers
    Czipo, Bence
    Hajdu, Akos
    Toth, Tamas
    Majzik, Istvan
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (245): : 31 - 45
  • [48] A Dynamic Assertion-based verification platform for UML Statecharts over Rhapsody
    Banerjee, A.
    Ray, S.
    Dasgupta, P.
    Chakrabarti, P. P.
    Ramesh, S.
    Vignesh, P.
    Ganesan, V.
    2008 IEEE REGION 10 CONFERENCE: TENCON 2008, VOLS 1-4, 2008, : 473 - +
  • [49] Distributed data mining - Framework and implementations
    Kumar, Anup
    Kantardzic, Mehmed
    Madden, Samuel
    IEEE INTERNET COMPUTING, 2006, 10 (04) : 15 - 17
  • [50] A Financial Evaluation Framework for Blockchain Implementations
    Demir, Mehmet
    Turetken, Ozgur
    Ferworn, Alexander
    2019 IEEE 10TH ANNUAL INFORMATION TECHNOLOGY, ELECTRONICS AND MOBILE COMMUNICATION CONFERENCE (IEMCON), 2019, : 715 - 722
12345