engleski

Model Checking Executable Specification for Reactive Components

Finding design errors in the earliest phase of software developments is still challenging area of research. This paper deals with model checking of executable specification. Executable specification is introduced as C program. After that, C program is transformed into an input model for the Spin model checker. At the end, an example for the Zune30 bug is presented.

executable specification; reactive component; software model checking; model transformation

nije evidentirano