A Verification Method of Software Safety Model Based on Model Checker
Hao Chen · Xi'an Jiaotong Daxue xuebao · 2011
In order to improve the analysis and design of software safety,on the basis of current researches on safety model and verification technology,a modeling and checking method is proposed for object-oriented software safety.Establishing non-formal UML models of software safety,safety extended deterministic finite automata and linear temporal logic are used to create the formal models and describe the safety properties separately.Through a model checker,we get the verification result.This approach realizes the combination of software safety model and verification technology.Experimental results show that the method can analyze and verify the safety properties effectively in the early stage of software design.