Model Checking RSML<sup>-e</sup> Requirements

	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
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Yunja Choi Articles by Mats P.E. Heimdahl

7th IEEE International Symposium on High Assurance Systems Engineering (HASE'02)

Model Checking RSML^-e Requirements

Tokyo, Japan

October 23-October 25

ISBN: 0-7695-1769-2

	ASCII Text	x
	Yunja Choi, Mats P.E. Heimdahl, "Model Checking RSML<sup>-e</sup> Requirements," High-Assurance Systems Engineering, IEEE International Symposium on, pp. 109, 7th IEEE International Symposium on High Assurance Systems Engineering (HASE'02), 2002.

	BibTex	x
	@article{ 10.1109/HASE.2002.1173111, author = {Yunja Choi and Mats P.E. Heimdahl}, title = {Model Checking RSML<sup>-e</sup> Requirements}, journal ={High-Assurance Systems Engineering, IEEE International Symposium on}, volume = {0}, year = {2002}, issn = {1530-2059}, pages = {109}, doi = {http://doi.ieeecomputersociety.org/10.1109/HASE.2002.1173111}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - High-Assurance Systems Engineering, IEEE International Symposium on TI - Model Checking RSML<sup>-e</sup> Requirements SN - 1530-2059 SP EP A1 - Yunja Choi, A1 - Mats P.E. Heimdahl, PY - 2002 KW - null VL - 0 JA - High-Assurance Systems Engineering, IEEE International Symposium on ER -

Yunja Choi, University of Minnesota

Mats P.E. Heimdahl, University of Minnesota

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/HASE.2002.1173111

Model checking is a promising technique for automated verification or refutation of software systems. Nevertheless, it has not been used widely in practice mainly due to the lack of the supporting tools that incorporate the model checking activity into the development process. As a part of our over-all method supporting specification centered system development, we have implemented a translator between a formal specification language RSML^-e and a symbolic model checker NuSMV.

Our translation and abstraction approach aims at usability in practice so that model checking can be used as a routine process during requirement analysis without requiring much knowledge about formal methods. Preliminary result from applying the system in a commercial setting is quite promising. In this paper, we discuss our translation and abstraction approach in some depth and illustrate its feasibility with some preliminary results.

Citation:

Yunja Choi, Mats P.E. Heimdahl, "Model Checking RSML^-e Requirements," hase, pp.109, 7th IEEE International Symposium on High Assurance Systems Engineering (HASE'02), 2002

Peer Review Notice | Give Us Feedback

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