Research Of Ada Program Model Checking Based On Program Slicing

With the development of multicore proccessors, Ada concurrent programs has been widelyapplied in modern embedded software system design. How to assure the correctness and reliabilityhas become an important problem. Using model checking to verify concurrent programs has become athrend, and the key problem is modeling which is usually done by hand. But this approach has someweaknesses, for instance, high cost and the artificial models are error-prone. At the same time, modelchecking is also facing the state explosion problem. Therefore, the main work of this paper focuses onusing program slicing technique to reduce state space, and the model extraction technique for Adaprogram to automaticly check Ada programs with the model checking tool SPIN.According to the model extraction technology, this paper designs a method of extractingPROMELA model for Ada program. It can well handle most of Ada language features, such as thecreating types and subtypes, concurrent task mechanism. At the same time, we implements anautomatic model extraction tool AdaToSpin, which contains an analyzer that executes lexical andsyntactic analysis and an translator that performs the translation from Ada to PROMELA.According to the state explosion problem, this paper presents an Ada concurrent program slicingmethod based on the properties of LTL. It divides into three steps: Firstly, analysis all kinds ofdependencies between statements, and construct concurrent program dependence graph of Adaprogram; Secondly, extract the slice criterion according to LTL formula for the nuture of the system tobe verified; Finally, use program slicing algorithm to compute the slice according to the dependenciesand slice criterion. At the same time, we implements an Ada concurrent program slicing systemAda_ProgramSlice. Using program slicing technique can effectively reduce state space.At last, according to the research results of this paper, we validate the technique of Ada programmodel checking is effective for extracting the model automaticly and solving the state explosionproblem through experiments.