Synthia: Verification and synthesis for timed automata. 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.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Waez, Md Tawhid Bin; Wąsowski, Andrzej; Dingel, Juergen; Rudie, Karen: A model for industrial real-time systems (2015)
- Fontana, Peter; Cleaveland, Rance: The power of proofs: new algorithms for timed automata model checking (2014)
- Waez, Md Tawhid Bin; Dingel, Juergen; Rudie, Karen: A survey of timed automata for the development of real-time systems (2013)
- Finkbeiner, Bernd; Peter, Hans-Jörg: Template-based controller synthesis for timed systems (2012)
- Peter, Hans-Jörg; Ehlers, Rüdiger; Mattmüller, Robert: Synthia: Verification and synthesis for timed automata (2011)