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.