Title :
The quest for correct systems: model checking of diagrams and datatypes
Author :
Philipps, Jan ; Slotosch, Oscar
Author_Institution :
Inst. fur Inf., Tech. Univ. Munchen, Germany
Abstract :
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
Keywords :
computer aided software engineering; data structures; functional programming; program verification; program visualisation; AutoFocus; CASE tools; SMV; correct systems; data type translation; datatypes; diagram model checking; embedded systems; functional programming language compliation; functional style; graphical description techniques; model checker; primitive data types; provably correct software; system structure; verification tools; Computer aided software engineering; Embedded software; Embedded system; Functional programming; Humans; Mathematical model; Quality assurance; Software quality; Software systems; Testing;
Conference_Titel :
Software Engineering Conference, 1999. (APSEC '99) Proceedings. Sixth Asia Pacific
Conference_Location :
Takamatsu
Print_ISBN :
0-7695-0509-0
DOI :
10.1109/APSEC.1999.809636
