Research On Runtime Verification Based On PPTL₃

With the vigorous development of computer technology,a variety of application software has become an important part of people's lives.Hence,it is a great challenge in the computer science that how to improve the reliability and safety of the software.As a kind of technology for judging whether a system satisfies its properties,verification is widely used to check the reliability and safety of software.Specifically,testing and model checking have been applied to the verification of software,resulting in successfully overcoming a lot of problems.However there are still some shortcomings as follows.For testing,it can only show that problems exist in the software but cannot prove that the software has no error.Moreover,it is difficult to design appropriate test cases.For model checking,it is difficult to extract models and the abstract model may be inconsistent with the actual system.More importantly,the state space explosion in model checking of any large-scale system is a difficult issue.To solve the problems above,a lightweight automated verification technique is proposed.In the Runtime Verification(RV),a temporal logic formula is used to describe the properties that a system should satisfy.Consequently a monitor is built to monitor the runtime traces of the system and these traces can be caught by online and offline methods which correspond to the code instrumentation and inspection of log files in practice,respectively.Finally,the data obtained by the monitor is used to verify whether the system satisfies the desired property.However,in the application of RV,a definite verification result cannot be given in the case of insufficient data since the system is verified by checking the finite prefix of its trace.Therefore,the traditional binary semantics does not meet the demand and need to be extended to the three-valued semantics.In addition,the expression of language is not powerful enough to describe all properties.In contrast,the Propositional Projection Temporal Logic(PPTL)has powerful expression ability,and the PPTL with star has the full regular expression.On this basis,this thesis presents a RV method based on the three-valued semantics PPTL(PPTL3).For software systems,only the runtime traces instead of the extracted model are needed.For the properties to be verified which are abstracted according to the system requirements,the PPTL3 formula is used to describe the properties and then is transformed into a monitor using the normal form and automata related theories.Based on the theoretical research above,this thesis presents a method for constructing the monitor in PPTL3-based Runtime Verification.Firstly,we abstract the property ? that needs to be verified according to the system requirements.Secondly,? and negation ? are rewritten as an equivalent normal form which is further expressed in the form of normal form graph(NFG)according to the corresponding theories.Thirdly,by adding a finite label to the nodes in the NFG,it is shown that the problem about the formula before the chop operator only exists in an infinite model and the whole formula does not exist in the corresponding model.Fourthly,after the stutter Büchi automaton is obtained by transformation,a nondeterministic finite automaton(NFA)is redefined by changing its set of accepting states and then the equivalent deterministic finite automata are obtained.Finally,the monitor is constructed by the product of the two automata.According to this process,this thesis employs the programming language Java to implement the tool,and illustrates the usability of the algorithm for constructing a monitor by an example related to file operations.