|
Abstract : |
Abstract. This paper presents a toolset we built for supporting verification of Statemate 1 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. 1, |
