« BACK TO PROGRAM
The Q-compiler for verifying high-consequence controls
John Aytac - Sandia National Labs
The purpose of the Q compiler is to prove relatively complexproperties about relatively simple digital controls -- controls for high-consequence systems where correctness is critical to safety. Starting with a generalized state machine, called a statechart, and progressing through multiple refinements, the state machine transition relation is proven against implementation code. The implementation can take the form of either C, using ACSL and Frama-C, or VHDL/Verilog using SVA in a commercial prover (e.g. Jasper). Refinements, and refinement across language boundaries afford a number of advantages. It enables proofs for more complex properties, more scalably than would otherwise be possible. The presentation will include some theory and an example of the development process.