The Quest for Correct Systems: Model Checking of Diagrams and Datatypes

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 the techniques used in compiling functional programming languages is a major part in the mapping from AutoFocus to SMV.

• Type: Conference
• Year: 1999
• Where: APSEC
• Authors: Jan Philipps, Oscar Slotosch
• Keywords: APSEC 1999, AutoFocus, Case Tool Autofocus, Data Type, Software Engineering