Automatic Generation Of Concurrent Program Based On Statistical Model Checking

Program synthesis is an important research topic in software development,the main goal of which is to generate executable code that conforms to a given specifica-tion automatically.With the development of computer technology,programs become more and more complicated,and it is more and more difficult to guarantee their cor-rectness,which makes the research of program synthesis get more and more attention.Concurrent programs are extremely error-prone because of their highly complex behav-ior.Therefore,how to synthesize concurrent programs automatically is an important research content in related fields.The traditional methods of concurrent program synthesis mainly carry out code construction by means of proof,derivation,etc.Most of these methods have problems of high complexity,low automation and high time overhead.In recent years,search-based concurrent program synthesis methods represented by a genetic algorithm have been proposed.The basic idea is to randomly generate a large number of code samples and then evaluate each sample.The code samples are transformed and searched by genetic algorithm based on the evaluation values.Existing methods use model checking directly to verify each sample for evaluation,which has significant limitations on performance and availability.Firstly,the time cost for verifying each sample is extremely high,and the performance is low.Secondly,we only gets whether the sample satisfied or not from the verification,and the evaluation granularity is too coarse,which is not conducive to the convergence of the search.To solve these problems,we have carried out systematic research:· Aiming at the problem of large time overhead and coarse granularity of the tradi-tional method,a concurrent program synthesis method based on statistical evalua-tion is proposed in this thesis.The core idea of this method is to evaluate the fitness of a program with the statistics of the results of checking program execution paths.Since with this method we only need to simulate the execution of programs to gen-erate a set of paths and check these paths instead of traversing the state space of a program,the time overhead is greatly reduced.Since the results of checking a set of paths are diverse,this method is fine-grained.· Although there are advantages of low time overhead and smooth fitness scores of the concurrent program synthesis method base on statistical evaluation,it needs different code implementation for the module of path verification while dealing with different problems.To solve this problem,we propose a universal method:a concurrent program synthesis method based on statistical model checking,which translates logic specifications on programs to bounded specifications on paths,uses statistical model checking technology to evaluate the probabilities that a program satisfies these bounded specifications,and finally uses this set of probabilities to calculate the fitness of the program.· The statistical model checking module is called frequently,so we have implemented a localized statistical model checking tool.On this basis,we have developed a concurrent program automatic generation tool PSSMC.We systematically evaluate the performance of PSSMC on some classic problems such as mutual exclusion,round robin,and dining philosopher,etc.Experiments show that compared with the existing methods,the concurrent program synthesis method based on statistical model checking proposed in this thesis has significant advantages in success rate and efficiency.