SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Wed 7 Dec 2022 11:00 - 11:30 at Seminar Room LG004 - Session 1: Time and State

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).

Wed 7 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
Session 1: Time and StateFTSCS at Seminar Room LG004
10:30
30m
Talk
Rewriting Logic Semantics and Symbolic Analysis for Parametric Timed AutomataIn Person
FTSCS
Jaime Arias CNRS; LIPN; Université Sorbonne Paris Nord, Kyungmin Bae POSTECH, Carlos Olarte CNRS; LIPN; Université Sorbonne Paris Nord, Peter Ölveczky University of Oslo, Laure Petrucci CNRS; LIPN; Université Sorbonne Paris Nord, Fredrik Rømming University of Oslo
DOI
11:00
30m
Talk
Q: A Sound Verification Framework for Statecharts and Their ImplementationsIn Person
FTSCS
Samuel D. Pollard Sandia National Laboratories, Robert C. Armstrong Sandia National Laboratories, Jon Aytac Sandia National Laboratories, John Bender Sandia National Laboratories, Geoffrey C. Hulette Sandia National Laboratories, Raheel S. Mahmood Sandia National Laboratories, Karla Morris Sandia National Laboratories, Blake C. Rawlings Sandia National Laboratories
DOI
11:30
30m
Talk
strategFTO: Untimed Control for Timed OpacityIn Person
FTSCS
Étienne André Université Sorbonne Paris Nord; LIPN; CNRS, Shapagat Bolat Université de Lorraine; CNRS; Inria; LORIA, Engel Lefaucheux Université de Lorraine; CNRS; Inria; LORIA, Dylan Marinho Université de Lorraine; CNRS; Inria; LORIA
DOI