loading...
The Quest for Correct Systems: Model Checking of Diagrams and Datatypes
Takamatsu, Japan December 07-December 10
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.1999.809636Sixth Asia-Pacific Software Engineeri ...
 This Article 
 
Buy PURCHASE ARTICLE: $19
PDF
HTML
Buy IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
ASCII Text
x 
 
Jan Philipps, Oscar Slotosch, "The Quest for Correct Systems: Model Checking of Diagrams and Datatypes," Asia-Pacific Software Engineering Conference, pp. 449, Sixth Asia-Pacific Software Engineering Conference (APSEC'99), 1999.
 
 
BibTex
x
 
@article{ 10.1109/APSEC.1999.809636,
author = {Jan Philipps and Oscar Slotosch},
title = {The Quest for Correct Systems: Model Checking of Diagrams and Datatypes},
journal ={Asia-Pacific Software Engineering Conference},
volume = {0},
year = {1999},
issn = {1530-1362},
pages = {449},
doi = {http://doi.ieeecomputersociety.org/10.1109/APSEC.1999.809636},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Asia-Pacific Software Engineering Conference
TI - The Quest for Correct Systems: Model Checking of Diagrams and Datatypes
SN - 1530-1362
SP
EP
A1 - Jan Philipps,
A1 - Oscar Slotosch,
PY - 1999
KW - formal methods
KW - software development environments
KW - software development tools
KW - model checking
VL - 0
JA - Asia-Pacific Software Engineering Conference
ER -
 
Jan Philipps, Technical Univesit?t M?nchen
Oscar Slotosch, Technical Univesit?t M?nchen
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.
Index Terms:
formal methods, software development environments, software development tools, model checking
Citation:
Jan Philipps, Oscar Slotosch, "The Quest for Correct Systems: Model Checking of Diagrams and Datatypes," apsec, pp.449, Sixth Asia-Pacific Software Engineering Conference (APSEC'99), 1999
Usage of this product signifies your acceptance of the Terms of Use.