Verified Model Checking of Timed Automata

Simon Wimmer, Peter Lammich

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


We have constructed a mechanically verified prototype implementation of a model checker for timed automata, a popular formalism for modeling real-time systems. Our goal is two-fold: first, we want to provide a reference implementation that is fast enough to check other model checkers against it on reasonably sized benchmarks; second, we strive for maximal feature compatibility with the state-of-the-art tool Uppaal. The starting point of our work is an existing highly abstract formalization of reachability checking of timed automata. We reduce checking of Uppaal-style models to the problem of model checking a single automaton in this abstract formalization, while retaining the ability to perform on the fly model-checking. Using the Isabelle Refinement Framework, the abstract specification of the model checker is refined, via multiple intermediate steps, to an actual imperative implementation in Standard ML. The resulting tool is evaluated on a set of standard benchmarks to demonstrate its practical usability.
Original languageEnglish
Title of host publicationInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems
Number of pages17
Publication statusPublished - 2018

Publication series

NameTools and Algorithms for the Construction and Analysis of Systems
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Verified Model Checking of Timed Automata'. Together they form a unique fingerprint.

Cite this