@inproceedingsSch1998, Author = {Schlör, R. and Josko, B. and Werth, D.}, Title = {Using a visual formalism for design verification in industrial environments}, Year = {1998}, Pages = {208-221}, Month = {01}, Editor = {Springer-Verlag}, Publisher = {Springer-Verlag}, Series = {Lecture Notes in Computer Science 1385}, Booktitle = {VISUAL'98}, type = {inproceedings}, note = {This paper reports experiences and results gained during the evaluation of the visual formalism STD as specification method for formal verification, performed in cooperation with industrial partners. The visual formalism STD (Symbolic Timing Diagrams) w}, Abstract = {This paper reports experiences and results gained during the evaluation of the visual formalism STD as specification method for formal verification, performed in cooperation with industrial partners. The visual formalism STD (Symbolic Timing Diagrams) was developed continuously since 1993 by OFFIS as a specification method, which satisfies several needs: (1) It is based on the principles used in the familiar notation of timing diagrams (as conventionally used by hardware designers). (2) It is a method amenable to formal verification, using state-of-the art verification tools efficiently (in particular, symbolic model-checking). (3) It supports compositional verification, which is an approach to verify large designs in a compositional way (breaking up proofs of requirements stated for a full design into a sequence of smaller proof tasks, which imply the global proof task). The formalism (with the supporting tools) has been integrated into an established verification environment ( CheckOff-M), which allows to verify industrial-scale designs by model-checking.} @COMMENTBibtex file generated on