swMATH ID: 
12933

Software Authors: 
Peter, H.J., Ehlers, R., Mattmüller, R.

Description: 
Synthia: Verification and synthesis for timed automata. Synthia is the first certifying model checker for open realtime 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 easytovalidate deductive proofs that only reflect the specificationcritical 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 controlrelated and the continuous part of the state space. 
Homepage: 
https://www.react.unisaarland.de/tools/synthia/

Related Software: 
UPPAAL TIGA;
Uppaal;
PRISM;
REDLIB;
CMC;
Kronos;
ROS;
NuSMV;
PuRSUE;
LTLMoP;
GitHub;
PRISMgames;
Modechart;
TINA;
LOTOS;
TAPAAL;
Romeo;
Tempo;
CoVer;
McAiT

Cited in: 
7 Publications
