Automated reasoning technologies will enable a correct-by-construction approach to systems engineering
Abstract not provided.
Publications
Search results
Jump to search filtersQ: A Sound Verification Framework for Statecharts and Their Implementations
Abstract not provided.
Q: A Sound Verification Framework for Statecharts and Their Implementations
FTSCS 2022 - Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, co-located with SPLASH 2022
We present Q Framework: a verification framework used at Sandia National Laboratories. Q is 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).
Q: A Sound Verification Framework for Statecharts and their Implementations
Abstract not provided.
4 Results