@inproceedings{Bro1998,
Author = {Brockmeyer, U. and Wittich, G.},
Title = {Tamagotchis Need Not Die - Verification of STATEMATE Designs},

Year = {1998},
Pages = {217-231},
Month = {01},
Series = {Lecture Notes in Computer Science},
Booktitle = {Tools and Algorithms for the Construction and Analysis of Systems},
type = {inproceedings},
note = {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 s},
Abstract = {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.}
}
@COMMENT{Bibtex file generated on }