Abstract
For the practical development of provably correct software for embedded systems the close integration of CASE-tools and verification tools is required. This 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 techniques used in compilers for functional programming languages is a major part in the mapping from AutoFocus to SMV.