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

fYear

1999

fDate

1999

Firstpage

449

Lastpage

458

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering Conference, 1999. (APSEC '99) Proceedings. Sixth Asia Pacific

Conference_Location

Takamatsu

Print_ISBN

0-7695-0509-0

Type

conf

DOI

10.1109/APSEC.1999.809636

Filename

809636