Tamagotchis Need Not Die - Verification of STATEMATE Designs
Brockmeyer, U. and Wittich, G.
Tools and Algorithms for the Construction and Analysis of Systems
This paper presents a toolset we built for supporting verification of STATEMATE designs. STATEMATE is a widely used design tool for embedded control applications. Designs are translated into finite state machines which are optimized and then verified by symbolic model checking. To express requirement specifications the visual formalism of symbolic timing diagrams is used. Their semantics is given by translation into temporal logic. If the model checker generates a counterexample, it is retranslated into either a symbolic timing diagram or a stimulus for the STATEMATE simulator.
01 / 1998
inproceedings
Lecture Notes in Computer Science
217-231
