Research And Improvement Of Runtime Verification Monitor Based On PPTL3

With the development of computer technology,various applications have gradually penetrated into various areas of people's daily life.However,even small errors in application can cause extremely negative impacts on people.For this reason,it is very important to improve the reliability and security of software systems.Runtime verification is proposed as a lightweight verification technology,which makes up for the shortcomings of traditional verification technologies.It uses a formal method to describe the property and converts the property into a corresponding monitor,and then extracts the trace from the verified system and delivers it to the monitor.The monitor will finally judge the property and give feedback and results.Various temporal logics are widely used to describe the property of runtime verification.Propositional projection temporal logic,PPTL,has full regular expression ability.Runtime verification can only obtain the finite trace of the system.Therefore,a runtime monitor construction method based on three-valued PPTL(PPTL3)is proposed.The corresponding tool PMG_PPTL(Property Monitor Generation of PPTL property)is implemented and applied to social network systems for offline and online monitoring,respectively.This thesis researches the runtime verification monitor based on PPTL3,proposes an improvement scheme for the monitor and implements it in PMG_PPTL.Firstly,the correctness of the monitor construction algorithm is directly proved,and the consistency of the monitor generated by the construction algorithm and PPTL3 is guaranteed.Secondly,two key problems to be solved are proposed in the monitor construction algorithm:the emptiness check of the NFA acceptable state during the conversion from SBA(Stutter Buchi Automaton)to NFA and the DFA minimization operation before the construction of the monitor.As a consequence,an emptiness check algorithm based on SCC(Strong Connected Component)and a minimization algorithm for deterministic finite automaton are given.Besides,time and space complexity of the improved algorithm for constructiong PPTL3 monitor are analyzed.Thirdly,the implementation of the two algorithms and other improvements in PMG_PPTL are introduced.The previous monitor and the improved one are compared and the results clearly prove the necessity of improvement.Fourthly,a Propositional Trace Monitoring System(PTMS)and a Data-based Trace Monitoring System(DTMS)based on PMG PPTL are proposed.PTMS,which has no restriction on the language of the target system,only contains a monitor at a time and the trace form of the monitor is the conjunction of atomic propositions.DTMS,where the offline monitoring has no restriction on the target language but the online monitoring must be Java,includes multiple property monitors during a monitoring and the trace is a data object.Finally,PMG_PPTL and other runtime verification monitors are compared,and the availability of PMG PPTL is shown.