Runtime Checking Of Real-time Temporal Constraints Using Formula Rewriting And Its Application In Train Control Domain

As a safety critical system, train control system takes the core place in rail signal. In order for the system to achieve the goal of safety running, all possible measures should be taken to make sure the correctness both in design and operation. Runtime Checking(RC)(also called Runtime Verification) is one of those measures that makes a trade-off between model checking and traditional testing, reducing the complexity of verification. Mainly focusing on the runtime behavior of system under investigation, RC checks the violation/satisfaction of system specification by abstract execution traces obtained at runtime. Currently the Linear-time Temporal Logic (LTL) is often used to describe the temporal constraints that refer to the correct order in which certain events happen. However, the execution traces consisting of discrete timepoints and checked by LTL do not take into consideration the real-time specification, thus making it too hard for LTL to describe real-time properties.By the construction of execution traces based on discrete timepoints synchronizing with real time of system, RTLTL has the ability to express real-time temporal constraints of system under investigation, thus overcoming the poor expressiveness of LTL for real-time properties. In this thesis, a rewriting-based monitoring algorithm for RTLTL properties is presented and a general non-interactive monitoring procedure is implemented in Maude. However, this algorithm is lack of flexibility due to its ignoring of traces with increasing size. Besides, the efficiency of non-interactive monitoring drops a lot when faced with long traces. In order to solve these problems, an interactive rewriting based incremental monitoring procedure and its implementation based on IMaude as well as auxiliary software tool framework are presented. The main work of this thesis is (1) to present a rewriting based non-interactive monitoring algorithm for RTLTL properties and corresponding monitoring procedure in Maude;(2) to present an interactive rewriting based incremental monitoring procedure based on IMaude; and (3) to apply our algorithm in two typical scenarios with real-time temporal constraints in train control domain, demonstrating the validity of our approach.