Specification And Verification Of Safety Critical System Requirements Based On SCR Method

Safety-critical systems are those software systems that can cause serious casualties,environmental damage,and property damage,etc,due to system failures.Avionics system,as a core system on the aircraft,is a typical safety-critical system.Requirements analysis is the most important stage in the process of system development through system research and analysis,understanding of user,system functions and performance requirements,and transforming non-formal requirements descriptions into complete requirements definitions.However,the traditional way of expressing the requirements is easy to make mistakes in requirements due to the ambiguity of the natural language and the inability to verify the requirements of the features,and it is difficult to handle highly complex and large-scale systems.The requirements-based formal analysis process is based on the well-defined semantics and mathematical models to make the representation of the requirements clearer and easier to understand.It improves the accuracy and efficiency of the requirements through automated testing and verification tools that address the requirements.However,the formal methods of requirements are too generic at present,and tools generally lack the verification of security attributes.This thesis is based on the research of SCR(Software Cost Reduction)method,for the problem that traditional method of requirements description is easy to introduce mistakes.We apply SCR method to the aircraft flaps and slats system to solve the over-universal problem of SCR method.From the view of ensuring the safety of the system,we expands the function of the T-VEC inspection tool based on the SCR method,and adds the function of verifying the security attributes.Specific research is as follows:In this thesis,the formal requirements analysis method is applied to the safety critical system avionics system,which use SCR method to describe the requirements documents of the existing flaps and slats control system in the aircraft system.Based on the flap motor speed control module for a detailed case analysis,through the T-VEC tool analysis and verification to determine whether it meets the needs of the consistency,grammatical correctness,completeness and other features.Further propose some SCR techniques in the application of skills.This work will provide the basis for the application of SCR method in airborne software system.In the aspect of the safety verification of the requirement model,this thesis develops the model transformation tool T2 N with the aid of the language parser antlr through the extension of T-VEC tools,designs the language structure transformation rules,and describes the requirements description language T-VEC transform to the symbolic model checking language XMV,in order to verify the extracted system security attributes.Based on the developed model transformation tool T2 N,taking the typical case Light Control System in requirement Engineering as an example,we establish the system requirement model,transform it to NuXMV model using T2 N tools,and further add the system safety attributes in the model.Finally,the transformed model is analyzed in the model detector NuXMV to verify the validity of the T2 N tool and the safety of the requirements model.