Research On Software Requirement Verification Based On Model

With the development of computer technology,the application of software in the aerospace system becomes more and more in-depth.Software plays a crucial role in the success of the mission and becomes one of the key factors in determining the quality of system products.The characteristics of the aerospace control system determine the reliability and real-time requirements of the software system are extremely high.According to authoritative statistics,if the software defects introduced during the requirement phase cannot be discovered in time,then the cost of wastage is enormous.In order to eliminate errors early in R&D,verification of software requirements is necessary,and how to perform model-based requirements verification for control system software with high real-time requirement is an issue that needs to be solved.In this paper,software requirement modeling and formal verification techniques and used to conduct a model-based verification of software requirements real-time verification.In this paper,the traditional Kripke structure,the software modeling language UML(Unified Modeling Language),the software requirement verification tool NuSMV(New Symbolic Model Verifier),etc,are deeply studied,and a complete set of integrated real-time requirement verification solution of real-time embedded software are proposed.This paper expands Kripke structure,forms RTKS(Real-time Kripke Structure)and RTKS'(Real-time Kripke Structure')and improves NuSMV to forms RTSMV tool.At the same time,this paper proposes the conversion of UML model to RTSMV tool language for UML's deficiency in formal verification.The rules improve the efficiency of real-time verification of requirement to facilitate model-based real-time verification of requirements.In order to verify the effectiveness of the proposed solution,the typical sub-function modules related to real-time performance in the space model are selected,and a research on software requirement verification based on model is performed.