Research On Formal Verification Of Concurrent Avionics Software Based On Abstract Interpretation

Software testing is one of the important aspects of software quality assurance during the software life cycle.Software testing can be divided into dynamic detection and static detection.Dynamic detection is the correctness of the test case at runtime,while static de-tection is the direct analysis of the source code.Static detection technology makes analysis accurate and efficient through powerful abstract interpretation,and has the characteristics of automation,perfection(full control and data coverage),making a popular method in industrial environments.But with the development of computer technology,concurrent software has been widely used.The development of concurrent software brings new chal-lenges to software testing.The uncertainty of execution path is an important feature of concurrent software.It is also a difficult point of testing.Due to the large concurrent state space,it is not good to directly apply the static detection technology of the sequential program to the interleaved execution of concurrent programs.The thread modular analysis method does not consider thread interleaving and re-lated execution construction instructions,and verify the concurrent program by analyzing each thread separately.The main advantage of the threaded modular analysis approach is that the sequential abstract interpreter can be promoted to a concurrent abstract inter-preter with minimal cost.The core idea of this method is divided into two steps:first,it create a thread,and analyze all threads as a separate sequential program,while collecting the impact of other threads on their variables.Then,it reanalyze all the threads and cal-culate the interference between the threads,saving the new behavior found and the new possible interference.Recursively this process until the interference is stable.However,the traditional thread modular analysis method is based on the non-relational flow insen-sitive semantics of thread interaction.The analysis is easier to process but the result is not accurate.This paper implements the flow sensitivity between threads based on the thread modular analysis method.And propose a constraint based on data flow to make the analysis result more accurate.The main innovations of this paper are as follows:1.We propose a flow-sensitive method for composing thread-modular abstract inter-preters into a more accurate static analysis procedure based on the original modular analysis method.2.We develop a lightweight constraint-based framework using data-flow graphs for checking the feasibility of inter-thread interferences.it improves analysis efficiency and analysis accuracy.3.With the support of the above theoretical research,we developed a prototype of an analysis tool for embedded concurrent programs based on this algorithm.4.To verify the aero-engine control system as an example,the static analysis of the sys-tem was carried out by applying our thread modular analysis method,demonstrating the ability of the algorithm to analyze and verify the embedded concurrent program.