Using a visual formalism for design verification in industrial environments

Schlör, R. and Josko, B. and Werth, D.
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.
01 / 1998
Lecture Notes in Computer Science 1385