Synthia – Verification and Synthesis for Timed Automata

Maintainer: Hans-Jörg Peter
Contributors: Rüdiger Ehlers, Robert Mattmüller, Manuela Ortlieb, Hans-Jörg Peter

Synthia is the first certifying model checker for open real-time systems modeled as networks of timed automata.
The key innovation of Synthia is its ability to justify why a given system is correct by providing a correctness certificate to the user.
Such certificates are easy-to-validate deductive proofs that only reflect the specification-critical properties of the system.
Synthia can also handle partially implemented systems, in which case it certifies their realizability by synthesizing reference implementations for the unimplemented parts.

In the analysis of timed automata, the main technical challenge is to efficiently represent the arising infinite state space.
Synthia’s analysis algorithm is based on a novel abstraction refinement technique that enables a clean combination of binary decision diagrams with difference bound matrices for a symbolic representation of both the discrete control-related and the continuous part of the state space.

License and Download

Synthia is licenced under the GNU General Public Licence version 3.

Current version 1.2.1

Sources: synthia-1.2.1-src.tar.gz

Intel 386 Linux binary: synthia-1.2.1-i386.tar.gz

Intel x86_64 Linux binary: synthia-1.2.1-x86_64.tar.gz

AMD64 Linux binary: synthia-1.2.1-amd64.tar.gz

Documentation

There is a CAV 2011 tool paper.

Synthia’s underlying approach is explained in this FORMATS 2010 paper.

A Synthia online tutorial is available here.

Benchmarks

Coming soon…

Contact

Please feel free to contact Hans-Jörg Peter for questions, comments, or suggestions.