Synthia: Verification and Synthesis for Timed Automata
Hans-Jörg Peter, Rüdiger Ehlers, and Robert Mattmüller
We present Synthia, a new tool for the verification and synthesis of open real-time systems modeled as timed automata. The key novelty of Synthia is the underlying abstraction refinement approach that combines the efficient symbolic treatment of timing information by difference bound matrices (DBMs) with the usage of binary decision diagrams (BDDs) for the discrete parts of the system description. Our experiments show that the analysis of both closed and open systems greatly benefits from identifying large relevant and irrelevant system parts on coarse abstractions early in the solution process. Synthia is licensed under the GNU GPL and available from our website.
23rd International Conference on Computer Aided Verification (CAV 2011).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.