SYNTHIA
Subproject |
S1 |
Categories |
Synthesis tools, Model checker for hard & soft real-time systems |
Overview |
SYNTHIA is a verification tool for checking safety requirements of open real-time systems modeled as networks of 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. An open system distinguishes between external and internal nondeterminism, of which one type represents an unpredictable environment and the other type represents a partial implementation. SYNTHIA checks if the system is realizable (i.e., whether there exists a full implementation) such that, independent of the environment, some safety requirements are satisfied. SYNTHIA can also certify the (un)realizability by generating a controller that represents safe (violating) implementations (environments). The verification of closed systems, where the implementation is deterministic and complete, is a special case and can equally well be handled by SYNTHIA. |
H.-J. Peter, R. Ehlers, R. Mattmüller. Synthia: Verification and Synthesis for Timed Automata. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, 23rd International Conference on Computer Aided Verification (CAV), volume 6806 of Lecture Notes in Computer Science (LNCS), pages 649-655, 2011. R. Ehlers, R. Mattmüller, and H.-J. Peter. Combining symbolic representations for solving timed games. In Krishnendu Chatterjee and Thomas A. Henzinger, editors, 8th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2010), volume 6246 of Lecture Notes in Computer Science (LNCS), pages 107-121, 2010. |
|
Formats |
|
Download |
|
Manual |
|
Status |
Stable |