Formal Verification for VRM Requirement Models

At the requirements level, formal verification and analysis are the focus of task’s attention which is developing complex systems by formal methods. Model checking is a technique for analysis and automated verification of complex safety-critical software systems. In this paper, a requirement model verification method based on formal technology is proposed to practice the model checking activity into the development process. Firstly, this essay analyzes syntax and semantics of models, which are defined by tabular expressions in VRM (variables relationship model). Then we preprocess the VRM model to classify into events tables, conditions tables and model class tables, and transform the VRM model into the automaton state transfer diagram with the help of semantic complementary work. Finally, we design an automatic model transformation framework from the VRM model to the model verification tool (nuXmv) and implement a translator between the formal specification language VRM and the symbolic model checker nuXmv. In this paper, we discuss our translation and abstraction approach in some depth and illustrate its feasibility with some preliminary examples.