Research On Runtime Vefication Technique Based On LTL Formula Progression

The booming demand and increasing innovation in the software industry, has brought great challenge to software reliability. It is not easy for traditional software testing tech-niques to reveal all subtle bugs which may only be witnessed under specific inputs. It is also impossible for test techniques to prove the system is free of errors. On the other hand, although formal verification techniques can prove some property of interest, but they still face some limitations:Theorem proving involves manual intervention while model checking faces the state-space-explosion problem.Runtime Verification is a combination of formal verification and traditional test-ing, where a monitor is generated from the specification, and inspects the execution of the program at run time to check whether the program conforms to the specifica-tion. One of its challenges is how to generate efficient monitor from high-level behavior specifications. The monitor is usually constructed as a deterministic finite automata, but the construction complexity is double exponential. One improvement technique is to construct the automata dynamically. Such techniques are called formula progression. However, the construction procedure based on formula progression is divergent. A clear upper bound of formula size has not even be specified. How to ensure the convergence of construction procedure is still an open problem.In this thesis, we made the following contributions:1) We propose the convergent formula progression algorithm which integrates the novel fix-point reduction technique. With the convergent formula progression, the formula size is restricted under the bound of 2|Φ|, where |Φ| means the size of input formula Φ. To our knowledge, we are the first to give the formal proof on the convergence.2) We implemented a novel runtime frame-work which support the multi-property verfication with both offline and online verifica-tion modes.3) We implemented a prototype tool and evaluated our framework against two real-world software systems. The results indicate that our approach is effective, and can benefit further research in both academic and industrial fields.