The quest for correct systems: model checking of diagrams and datatypes
Jan Philipps, Oscar Slotosch · 2003
For the practical development of provably correct software for embedded systems, the close integration of CASE tools and verification tools is required. The paper describes the combination of the CASE tool, AutoFocus, with the model checker SMV. AutoFocus provides graphical description techniques for system structure and behavior. In AutoFocus, data types are specified in a functional style, while SMV supports only primitive data types. Hence, a data type translation based on the techniques used in compiling functional programming languages is a major part in the mapping from AutoFocus to SMV.