Transformation And Formal Verification Of XX Software Requirement Model Based On NuSMV

In the security critical systems of aerospace,rail transit,national defense and military,the errors caused by software requirements design defects will cause huge economic losses,and even threaten the safety of human life.Therefore,it is of great significance to formally detect the software requirements of the security critical system to ensure the security of the system.The formal detection method aims at computer system,using formal language and mathematical methods to verify software security.XX software,as an important part of security critical system in a certain field,needs to use Simulink tools for requirement modeling.To solve the lack of research in the field of formal verification of software requirements from Simulink model to Nu SMV model,this paper designs and implements a formal verification method of security critical software requirements Simulink model based on Nu SMV to improve software security.The main results are as follows:(1)This paper presents a method of transforming Simulink model into intermediate model.Design the method of extracting the information of Simulink model,analyze and process the semantic and structural information of Simulink model.This paper reconstructs the model by using the method of Simulink model transformation,transforms the Simulink model into the intermediate model,and simplifies the process of establishing the Nu SMV model of software requirements.(2)A set of conversion rules from Simulink model to Nu SMV model is designed.According to the variables,functions,state changes and special keywords in the intermediate model,the corresponding transformation rules are made to realize the transformation of the two models,and the specification is extracted to verify the model.Then,aiming at the problem that Nu SMV tool can not automatically locate the wrong path in the model,a fault path backtracking method is designed to locate the wrong path in the requirement model,which is convenient to correct the defects of software requirement design.(3)The extraction method of model formal verification protocol is proposed.The verification protocol is classified by using the characteristics of the model.The extraction methods of domain-independent protocol and domain-related protocol are designed respectively to realize the extraction of model verification protocol.The problem of incomplete and nonstandard specification extraction in the process of model formal verification is solved.At the same time,using the idea of model abstraction and slicing,the common state set is abstracted as a state,and the irrelevant paths that do not affect the system properties are sliced to compress the model state space and improve the efficiency of formal verification.This paper develops the XX software requirement model formal verification system to realize the automatic conversion and verification of the XX software requirement Simulink model to the Nu SMV model.Experiments show that the system can verify mutually exclusive errors,deadlock errors,and the functional attributes of the demand model,and effectively improve software security.