Formal Verification Of Software Requirements Based On Variable Relationship Model And Research

In recent years,the development of Chinese civil aircraft and systems has progressed rapidly.With the rapid growth of aircraft functions and system complexity,the design and analysis methods of avionics systems and software that are closely related to the safety of aircraft systems have become hot topics in the field..In the system engineering / software engineering process defined in the civil aircraft development standards such as ARP4754 and DO-178 C,there is a strong emphasis on constructing complete,consistent,and well-organized system / software requirements at the beginning of the software product life cycle,and the introduction of model-based System Engineering(Model Based System Engineering,MBSE)method.At the same time,the rigorous mathematical models and automated analysis algorithms of formal methods make the aviation field begin to pay attention to and apply related formal models and tools(such as Nu XMV,etc.).Therefore,how to use formal methods to model,analyze,and verify avionics system requirements to achieve the airworthiness requirement DO-178 C has become an important challenge in the current avionics software research field.In this thesis,a formal requirement description model-Variable Relationship Model(VRM)oriented to the avionics software application field is established,and a formal verification method based on Nu XMV tools is designed based on the VRM model.And verification activities can meet the objectives of DO-178 C airworthiness standards.It includes the following aspects:1)The BNF definition form of the variable relationship model VRM is constructed,which is used for the strict text model description of the requirement specification.Model elements such as "vocabulary elements","declarations and types",and "expressions" are defined in VRM;where "vocabulary elements" represent the atomic components of the VRM model language;"declarations and types" provide the combination of lexical elements into subsystems,Constants,types,variables,logical structures,and functional requirement declaration rules;"Expressions" define rules for combining operators and operation arrays into constraint expressions and relational expressions.2)Analyze the VRM model elements and XMV modeling language features,and design the mapping rules for converting from VRM language to verifiable model detection language XMV from three aspects: variable type,variable and expression.The mathematical formula was used to prove the correctness of the rules for converting from VRM model language to XMV language.3)The conversion from VRM model to XMV modeling language is realized.The parser ANTLR was used to parse the VRM language to generate a parse tree.The implementation of the conversion tool is accomplished through the designed variable conversion algorithm,logical structure conversion algorithm,and functional requirements conversion algorithm.4)Designed a prototype tool software for avionics system requirement analysis and verification.The main functions of the prototype tool software include: requirements check function,test vector generation function and requirements verification function.The requirements check function completes the check for the correctness,completeness,and consistency of the requirements;the test vector generation function completes the check for the requirements function;and the requirements verification function completes the check for the security attributes ofthe requirements.5)An example of a flight mode management system in a flight navigation system is analyzed.Including: Using the certification goals given in the DO-178 C / DO-333 standard as a guide,constructing a VRM model of the flight mode management system's required behavior,using prototype tool software to perform model conversion,and using Nu XMV to verify the flight mode management system requirements Some of the required security attributes,and determine how these modeling analysis and verification activities meet DO-178C's verification goals.