Paper Info
Title
The Quest for Correct Systems: Model Checking of Diagrams and Datatypes
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.
Year
DOI
Venue
1999
10.1109/APSEC.1999.809636
APSEC
Keywords
Field
DocType
data type translation,data type,close integration,model checker smv,correct systems,model checking,functional style,graphical description technique,primitive data type,case-tool autofocus,embedded system,functional programming language,formal methods,case tool,primitive data types,system modeling,software development environments,software quality,embedded software,software systems,model checker,computer aided software engineering,embedded systems,data structures,quality assurance,autofocus,case tools,datatypes,testing,functional programming,mathematical model
Data structure,Programming language,Model checking,Autofocus,Functional programming,Computer science,Theoretical computer science,Software,Data type,Computer-aided software engineering,Formal methods
Conference
ISBN
Citations 
PageRank 
0-7695-0509-0
11
1.19
References 
Authors
14
2
Name
Order
Citations
PageRank
Jan Philipps116216.45
Oscar Slotosch217319.28