Subproject

S1

Categories

Model checker for hard & soft real-time systems

Overview

Converter to transform timed automata and timed games into FSMTs (finite state machine with time) based on LinAIGs. The resulting FSMT can be verified using fsmtMC.

Publications

G. Morbe, F. Pigorsch, and C. Scholl. Fully Symbolic Model Checking for Timed Automata. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), volume 6806 of Lecture Notes in Computer Science (LNCS), pages 616-632, 2011.

G. Morbe and C. Scholl. Fully Symbolic Model Checking for Timed Automata. In Frank Oppenheimer, editor, 14th Workshop "Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen", pages 9-18, 2011.

Benchmarks

See www.informatik.uni-freiburg.de/~morbe/fsmt/

Download

Click here for the binary.

Manual

Just type ./ta2fsmt on the command line to see how it can be used.

Status

Prototype