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 条

[21] Design verification of FPGA implementations
Fudan University, Shanghai, China
不详
不详
不详
IEEE Des Test Comput, 2 (66-73):
[22] Runtime verification of statechart implementations
Pintér, G
Majzik, I
ARCHITECTING DEPENDABLE SYSTEMS III, 2005, 3549 : 148 - 172
[23] Modeling and verification of ISA implementations
Shen, XW
Arvind
PROCEEDINGS OF THE 3RD AUSTRALASIAN COMPUTER ARCHITECTURE CONFERENCE, ACAC'98, 1998, 20 (04): : 157 - 168
[24] Slede: A Domain-Specific Verification Framework for Sensor Network Security Protocol Implementations
Hanna, Youssef
Rajan, Hridesh
Zhang, Wensheng
WISEC'08: PROCEEDINGS OF THE FIRST ACM CONFERENCE ON WIRELESS NETWORK SECURITY, 2008, : 109 - 118
[25] Specification and verification of a safety shell with statecharts and extended timed graphs
van Katwijk, J
Toetenel, H
Sahraoui, AE
Anderson, E
Zalewski, J
COMPUTER SAFETY, RELIABILITY AND SECURITY, PROCEEDINGS, 2000, 1943 : 37 - 52
[26] Formal verification of UML statecharts with real-time extensions
David, A
Möller, MO
Yi, W
FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS, 2002, 2306 : 218 - 232
[27] Using a process algebra interface for verification and validation of UML statecharts
Doostali, Saeed
Babamir, Seyed Morteza
Javani, Mohammad
COMPUTER STANDARDS & INTERFACES, 2023, 86
[28] Formal Verification of UML Statecharts using the LOTOS Formal Language
Javani, Mohamad
Neysiani, Behzad Soleimani
Babamir, Seyed Morteza
2015 2ND INTERNATIONAL CONFERENCE ON KNOWLEDGE-BASED ENGINEERING AND INNOVATION (KBEI), 2015, : 754 - 760
[29] Verification of Implementations of Cryptographic Hash Functions
Wang, Dexi
Jiang, Yu
Song, Houbing
He, Fei
Gu, Ming
Sun, Jiaguang
IEEE ACCESS, 2017, 5 : 7816 - 7825
[30] Design verification and debugging FPGA implementations
Hajimowlana, H
EDN, 2003, 48 (25) : 69 - +

← 1 2 3 4 5 →