Research On Aerospace Embedded Software Model Verification System

With the development of modern aerospace technology,the application of embedded software in the aerospace field is becoming more and more extensive.The scale and complexity of aerospace embedded software and the proportion of its function in the entire aerospace system have risen sharply,showing a comprehensive The development trend leads to higher and higher requirements for the reliability and security of aerospace embedded software.Therefore,how to improve the reliability and security of aerospace embedded software has become an issue of increasing concern.When applying model check technology to verify the system model,the growth of the system size will cause the state space of the model of the system to be tested to grow rapidly,and exhaustive traversal of the growing state space will cause slow calculations and a problem of state space explosion.Due to the complex functions of the aerospace embedded software and the large number of states after modeling,the problem of state space explosion will occur during model checking,affecting the efficiency of verification.In view of the above problems,this thesis focuses on the research of embedded software model check technology and embedded software state space reduction technology,and designs and implements aerospace embedded software model verification system.The state space of the model is reduced and the model to be detected is verified and applied in the aerospace application software to alleviate the state space explosion problem,improve the efficiency of model checking,and lay the technical foundation for the improvement of the safety of the aerospace embedded software.The work done in this article is as follows:1.Design of the overall framework of the embedded software model verification system: Aiming at the lack of the current embedded software security verification system in the aerospace field,this thesis proposes the overall framework of the aerospace embedded software model verification system,which is divided into embedded software model verification based on model check tools,embedded software state space reduction tools based on adjacency matrix.2.Design and implementation of embedded software state space reduction tool: for the complex functions of embedded software in the aerospace field,the large number of states after modeling,and the state space explosion during model checking,this thesis studies the state based on adjacency matrix Space reduction technology,design and implement the embedded software state space reduction tool to alleviate the state space explosion in the process of model check.3.Design and implementation of embedded software model verification tool: In response to the current demand for security verification of embedded software in the aerospace field and the inadequate quality assurance of the pre-design of aerospace embedded software in China,this thesis researches the model check technology based on model-driven architecture,and applies the model check technology to the real-time,safe and critical application of star-loaded embedded,and designs and implements the embedded software model verification tool in the aerospace embedded software design and development process,which guarantees the security of aerospace embedded software,thereby improving the application of embedded software in China's aerospace field,enhancing the overall design capability of domestic aerospace embedded software,improving the security of aerospace embedded software,and solving the technical bottleneck and potential problems that hinder the development of future aerospace embedded software from the top level.