Sciweavers

APSEC
1999
IEEE

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

13 years 8 months ago
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.
Jan Philipps, Oscar Slotosch
Added 02 Aug 2010
Updated 02 Aug 2010
Type Conference
Year 1999
Where APSEC
Authors Jan Philipps, Oscar Slotosch
Comments (0)