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

	This Article
	Subscribers, please Login Purchase article: $19 PDF IEEE Xplore Subscribers RSS feed
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Jan Philipps Articles by Oscar Slotosch

Sixth Asia-Pacific Software Engineering Conference (APSEC'99)

Takamatsu, Japan

December 07-December 10

ISBN: 0-7695-0509-0

	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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.1999.809636

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

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.