Real-Time Verification of STATEMATE Designs -- Tool-Paper
Brockmeyer, U. and Wittich, G.
Computer Aided Verification
This tool-paper presents a toolset for real-time verification of STATEMATE designs.STATEMATE is a widely used design tool for embedded control applications. In our approach designs including all timing information are translated into untimed finite state machines (FSMs) which are verified by symbolic model-checking. Real-time requirements are expressed by TCTL formulae interpreted over discrete time. A reduction from TCTL model-checking to CTL model-checking in order is implemented to use a CTL model-checker for the verification task. Some experimental results of the toolset are given.
01 / 1998
inproceedings
Lecture Notes in Computer Science
537-541
