Q: A Sound Verification Framework for Statecharts and Their Implementations
summary
The Q Framework compiles Stateflow-style statecharts into SMV and generates ACSL contracts for a constrained C subset, proving a refinement relation between model and implementation with NuSMV and Frama‑C. It uses a Clang tool (Qfact) and a CompCert C‑light translation to remove undefined behavior and annotate C, models volatiles as observables with ghost state, and flattens parallel/nested charts — causing an acknowledged exponential state blowup that limits scalability. The workflow is largely automated.
AI-written summary · about
chapters (8)
- 0:00Q framework for Statecharts
- 2:50Framework overview
- 8:46Q Lang compiler
- 13:20Refinement argument
- 17:30Statechart semantics
- 19:40Related work comparison
- 21:45Future work limits
- 22:31Conclusion & Q&A
related talks
40mAn Interdisciplinary View on Prototypes - Towards Executable Models That Can Be...
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
39mCHASM: A High Level Analysis of Temporal's New State Machine SDK
24mQSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing
49mHow to scale QML based projects an Architecture vision
01h 04mCoq's vibrant ecosystem for verification engineering
27mLet's Bring System Dynamics Back to CS!