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 条

[31] VerMI: Verification Tool for Masked Implementations
Arribas, Victor
Nikova, Svetla
Rijmen, Vincent
2018 25TH IEEE INTERNATIONAL CONFERENCE ON ELECTRONICS, CIRCUITS AND SYSTEMS (ICECS), 2018, : 381 - 384
[32] Probabilistic Relational Verification for Cryptographic Implementations
Barthe, Gilles
Fournet, Cedric
Gregoire, Benjamin
Strub, Pierre-Yves
Swamy, Nikhil
Zanella-Beguelin, Santiago
ACM SIGPLAN NOTICES, 2014, 49 (01) : 193 - 205
[33] Automated Verification Of Cryptographic Protocol Implementations
Babenko, Liudmila
Pisarev, Ilya
12TH INTERNATIONAL CONFERENCE ON THE DEVELOPMENTS IN ESYSTEMS ENGINEERING (DESE 2019), 2019, : 849 - 854
[34] Cryptographically sound implementations for communicating processes
Adao, Pedro
Fournet, Cedric
AUTOMATA, LANGUAGES AND PROGRAMMING, PT 2, 2006, 4052 : 83 - 94
[35] Formal verification of statecharts using finite-state model checkers
Zhao, Qianchuan
Krogh, Bruce H.
IEEE TRANSACTIONS ON CONTROL SYSTEMS TECHNOLOGY, 2006, 14 (05) : 943 - 950
[36] Formal verification of Statecharts using finite-state model checkers
Zhao, QC
Krogh, BH
PROCEEDINGS OF THE 2001 AMERICAN CONTROL CONFERENCE, VOLS 1-6, 2001, : 313 - 318
[37] A framework for testing AIS implementations
Horvath, Tamas
Sulyan, Tibor
TESTING OF SOFTWARE AND COMMUNICATING SYSTEMS, PROCEEDINGS, 2007, 4581 : 186 - +
[38] Vivienne: Relational Verification of Cryptographic Implementations in WebAssembly
Tsoupidi, Rodothea Myrsini
Balliu, Musard
Baudry, Benoit
2021 IEEE SECURE DEVELOPMENT CONFERENCE (SECDEV 2021), 2021, : 94 - 102
[39] VERIFICATION OF HIGH-LEVEL PROTOCOL IMPLEMENTATIONS
WEAVING, K
COMPUTER COMMUNICATIONS, 1981, 4 (02) : 56 - 60
[40] Automatic Formal Verification of Block Cipher Implementations
Smith, Eric Whitman
Dill, David L.
2008 FORMAL METHODS IN COMPUTER-AIDED DESIGN, 2008, : 45 - 51

← 1 2 3 4 5 →