Reseach On Formal Modeling And Testing For Embedded Software

According to the statistics from the aerospace software evaluation center,almost 80%of the large-scale real-time embedded software failures are caused by interrupt nesting,and the problem of atomic violation caused by the interrupt nesting has not been effectively solved.The reliability of the embedded software executed on multi-core CPUs is challenging to guarantee due to data race problems caused by multi-threaded interleaving and random running results.Hence,it is necessary to use multiple single-core CPUs to avoid data race problems through network communication,which accordingly influence the application of multi-cores in aerospace applications.Besides,when testing these applications,the number of test cases is large,which makes it difficult to evaluate its reliability.To solve the problem of atomic violation caused by interrupt nesting,the State Transition Matrix(STM)model with Re-Engineering Interrupt Processing scheme are proposed to solve the problem of atomic violation caused by interrupt nesting.In our scheme,the shared variables in the interrupt handler are transplanted to the main program STM,and the interrupt handler is only responsible for storing the external interrupt request data in the buffer.The main program STM completes the interrupt processing and interrupt nesting functions,thus effectively solving the problem of the atomic violation.Aiming at the problems of atomic violation and data race problem caused by multithreaded interleaving,an STM-based method of multi-threaded access control and separation is proposed.At first,a multi-thread STM model is established.In order to verify the multithreaded model,an integrated method is usually used for verification.However,it is easy to cause an explosion in the state space.Therefore,a control-access separation method is proposed.In our scheme,the control logic for accessing shared variables in each STM is integrated into an independent STM,and finally,the control and access of shared variables are separated,and only the control STM needs to be verified.With this method,the state space explosion problem of multi-threaded verification can be solved.To solve the embedded software real-time integration test case generation problem,the integration test method with the time constraint and loop constraint of the hierarchical model are proposed.Our scheme utilizes the hierarchical model design of the system to be tested and establishes a real-time testing method for large-scale and complex software systems.By increasing the structural complexity of the test cases,it finally generates a more complex regular expression testing case to find out the hidden software function problems.To address the problem of model division and use-case simplification of the complex software integration testing,a model structure decomposition method and test optimization method are proposed.Through the structural decomposition of the directed graph corresponding to the overall finite state automata(FSM),the function test of the decomposed sub-model is performed first.Then,according to the connected characteristics of the directed graph and the semantic characteristics of the semantic network,test cases are clustered and generated.Finally,the system is tested to find deeper errors.Finally,the above research methods are verified in practical applications in aerospace control systems,effectively solving problems such as data race and atomic violations.In practical applications,such as smart TVs and motor control,integrated testing of real-time of complex structure of large-scale software to find hidden defects.After verification,the verification problem of the several FSMs model and the universal testing model can be found,which will be solved in the future.