SM2SMV - A Tool for Facilitating Dependable Software Requirements Analysis Using Model Checking
Huigang Li, Andrew J. Kornecki, David P. Gluch, Embry Riddle Aero · 2000
The complexity of dependable software and electronicsystems is growing at a rapid pace. As systems becomemore and more complex, defect detection becomes adifficult problem. One of the available techniques tofacilitate early defect detectionwithin requirements specifications is model checking. The technique is basedon building a finite model of a system and checking if themodel possesses the desired/required properties [1].One of the tools used in model checking is theSymbolic Model Verifier (SMV), developed by K. L.McMillan at Carnegie Mellon University [2]. Using theSMV tool consists of four major phases:(1) creating a finite state machine model for the system;(2) translating the state machine model into SMV inputprogram;(3) creating the expected properties and translating theminto SMV program;(4) running the SMV program and interpreting theresults.Currently, the phase (4) can be completed automaticallyby the available SMV tool. Phase (1) to phase (3) still needmanual work.In the past year, we carried out several experimentsapplying SMV to verify system requirements for a varietyof dependable systems (e.g. a heart pacemaker, militaryavionics, etc). The experience shows that most of the workin phase (2) involves mechanical translation from the statemachine graphical representation to SMV input programwritten in SMV language. The detailed syntax andgrammar for SMV input language can be found in the SMVuser manual [2][4].Since phase (2) is a translation from a state machinediagram to SMV input code, it may be possible to do thiswith a software tool. The potential advantages of agraphically based automated code generator would be thetime saved by an engineer and improved correctness ofthe SMV input program. The work described here is thefirst step in exploring these issues. Recently, a research group in Germany did similarresearch on translating STATEMATE designs into SMIcode. The model checker used in their research is a tooldeveloped by SIEMENS [3].