Research On PPTL Specification Mining Based On Pattern Library

Program Specification is an important part of software engineering.The quality and reliability of software lacking program specifications can hardly be guaranteed.In reality,most program specifications are written in natural languages,but natural languages have the problem of ambiguity.Formal languages can accurately describe program specifications,but it is very difficult to generate formal languages from natural languages.Since each correct execution of a program contains program specifications,and the trace of the program is a record of the program execution process,formal specifications can be mined from program traces.Temporal logic is often used to describe program specifications.Propositional Projection Temporal Logic(PPTL)is full regular and decidable.Compared with other temporal logic languages such as LTL and CTL,PPTL can better express program specifications.To this end,this thesis focuses on how to mine PPTL specifications from executable programs.The main tasks are as follows:1.A PPTL pattern library is first constructed for storing program patterns.Then,program patterns from existing programs and related documents are extracted and abstracted.Finally,the PPTL pattern library is organized and summarized.The patterns in the pattern library are divided into Occurrence and Order,and there are 37 patterns in total.As the basis of this article's program specification mining task,PPTL pattern library has the advantages of rich patterns and strong expressive ability compared with existing pattern libraries,and allows users to customize editing and adding patterns.2.A method is proposed to mine PPTL specifications from executable programs.First,use the dynamic invariant detection tool Daikon and the Dtrace Filter tool designed and developed in this thesis to generate the trace of the program.Furthermore,a specification mining algorithm based on the PPTL normal form is designed,using the semantics of the PPTL normal form to check the program execution trace,which can ensure the correctness of the specification mining process and results,and avoid the difficulty of directly using PPTL semantics.3.The PPTL specification mining tool PPTLMiner is designed and developed.According to the function,PPTLMiner includes five modules: Trace Generator,Trace Parser,PPTL Parser,PPTL Pattern Instantiator and PPTL Pattern Checker,and detailed descriptions of the functions and implementation details of each module.On this basis,the C program of the reader-writer problem and the Java program of the producer-consumer are used to test PPTLMiner,and the test results are analyzed.The test results show that PPTLMiner can mine the correct specification of programs.Finally,the validity of PPTLMiner is verified on the philosopher's dining problem model,experiments between PPTLMiner and existing specification mining tools are carried out.The results show that PPTLMiner has the advantages of good versatility and strong expressive ability.