Research On Software Runtime Verification Method Based On LTL Three-valued Semantics

With the increasing complexity of the software system,it is imminent to promote its reliability,which leads immeasurable losses to the national security and economy in the most serious situation.However,in the aspect of improving the software reliability,the traditional model detection is prone to "state space explosion" and testing technology always appears imperfectness situation of test case,which can not guarantee the correct operation of the program.Based on the linear time series logic(LTL)run-time verification technology,through the the combination of actual operation of the system and formal verification,runtime verification monitor is constructed to achieve the program monitoring to ensure that program runs correctly.However,the traditional supervisor is constructed based on the LTL binary semantics,which has problems in semantic consistency.Therefore,the paper will construct the runtime verification monitor based on LTL ternary semantics(LTL3).Firstly,as the LTL only has a single temporal timing operator,the description of the nature specification in many cases is not concise and natural.Therefore,on the basis of the LTL,the paper integrates the timing operators that represent the past time.Unlike the PLTL(LTL with past modalites),the operators of the two tenses are redefined with the concept of moving time so that they can converge with each other and have a unified semantic basis to obtain linear time series logic LTL-P based on moving time,the description of the statute will be more natural,more concise.Secondly,LTL-P has two kinds of timing logic operators,which can not turn into the Büchi automaton directly,while the construction of LTL-P monitor needs to use the Büchi automaton as a transition.This study will convert LTL-P semantics into the two-way exchange automaton for the first step,then convert LTL-P semantics into Büchi automaton.In addition,the Büchi automaton is optimized by MCS algorithm and RRS algorithm,which effectively reduces the size of the final monitor.Finally,the paper carries out the run-time verification experiment based on LTL-P monitor.In the experiment,the transformation of various automation between LTL-P formula and two-way alternating exchange automation and the construction of the LTL-P runtime verification monitor are realized according to the LTL-P supervisor construction method in Chapter 3.The basic framework of runtime verification is designed,which realizes the transformation of LTL-P formula to automaton,the construction of monitor,the weaving of the monitor,and the verification of the four processes of the target program.At the same time,according to this framework,an operable prototyping tool is developed to complete the LTL-P monitor based on the run-time verification experiments.In addition,the tool JavaMOP is extended by adding the LTL ternary semantic logic library so that the generated runtime verification monitor can verifies the target program based on the LTL ternary semantics.