Abstract:
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 overall 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.
Venue:
Proceedings of the Seventh IEEE High Assurance in Systems Engineering Workshop}, Tokyo, Japan, October 2002
bibtex:
@InProceedings{CH02,
author = {Yunja Choi and Mats Heimdahl},
title = {Model Checking \rsml\ Requirements},
booktitle = {Proceedings of the 7th IEEE/IEICE International
Symposium on High Assurance Systems Engineering},
pages = {},
year = 2002,
number = {},
series = {},
month = {October},
address = {},
annote = {}
}
