1(College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016,China)
2(State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210093,China)
Abstract：In the field of safety critical, software systems analysis and verification has become a very important hotspot in the software engineering research. This paper is based on the Mirror Theory, and give a safety verification method.Specially, the analysis tree is created based on the operation expression,and then the semantic predicate of each node in the tree is generated by the semantic axioms,theorems and some calculated rules. Secondly,the result of programs safety is obtained by verifying the corresponding specification with the logic of Mirror Theory.Finally,a tool and example are given to demonstrate its value, and this approach has been applied in the aerospace and astronautics field.
2014, Vol. 35 
