Research On Runtime Verification Of Software Correctness Based On LTL

With the development of computer technology, the applications of software and software system in our life have been more and more widely. Besides the applications of software on the microcomputer,there are also a lot of large scale software applications in industrial manufacturing, transportation and military fields. In large scale software systems, it is crucial to ensure the correctness, security and reliability of software. Many important fields have been increasingly relying on the software systems due to its wide and deep deployment. Since the software security has posed higher requirement of verification technologies, the traditional technologies do not meet the needs which software security ask for, software security needs higher standard verification techniques to solve the problem. As a light weight verification technology, the runtime verification can be applied as the complement of traditional verification technologies. One of the outstanding features of this technology is that its verification process which lays the foundation of the real-time correcting of software errors is carried out during the runtime of the software.This paper first presents the semantics of linear temporal logic based on shifting time(LTL-P) which introduces the temporal operators in past-time linear temporal logic into standard linear temporal logic.The LTL-P semantics are able to describe the events in the past and future,and then improve the expressivity of the semantics. After that,we present a new algorithm to generate two-way alternating automatonfrom LTL-P, which implements the transmission from logic semantics to automaton is presented. Finally,a construction method of runtime verification monitors is described,which translates the formula of LTL-P into runtime verification monitor based on the algorithm of automaton transmission. In order to simplify the process of verification, a runtime verification tool named JRVtool which integrates Java MOP with AspectJ is developed. We construct a runtime verification monitor for typical properties by JRVtool, and monitor a target program with it. The results show that the method is correct and effective.