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

This paper presents a rewriting logic semantics for parametric timed automata (PTAs) and shows that symbolic reachability analysis using Maude-with-SMT is sound and complete for the PTA reachability problem. We then refine standard Maude-with-SMT reachability analysis so that the analysis terminates when the symbolic state space of the PTA is finite. We show how we can synthesize parameters with our methods, and compare their performance with Imitator, a state-of-the-art tool for PTAs. The practical contributions are two-fold: providing new analysis methods for PTAs—e.g. allowing more general state properties in queries and supporting reachability analysis combined with user-defined execution strategies—not supported by Imitator, and developing symbolic analysis methods for real-time rewrite theories.

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