Model Checking Timed Interval Temporal Logic: Theory, Algorithms And Application

Real-time systems are constituted of software or hardware systems that have real-time constraints. In the safety-critical systems, such as transport control systems, spaceflight and nuclear react control systems, model checking is a vital formal technique for guarantee correctness of real-time systems. The principles of this method are: describe the properties of a system with some real-time logic formulas, construct system models with timed automata, model checking algorithm decides automatically whether the models satisfy the properties. Several real-time logics including timed interval temporal logic (TITL) have been presented for formal verification. As a linear real-time logic, TITL has been used widely due to its advantages. But until now, TITL model checking problem has not been solved due to its absence of verification technique and formal theory. To this end, this paper investigates propositional TITL model checking problem as well as constructs its architecture on theory, method and application.In order to make clear what kind of properties can be described by TITL, whether TITL can be used to model checking or not, and the efficiency of TITL model checking, we study expressive power, decidability and complexity of the logic. We prove the equivalence relation between discrete TITL formulas, discrete timed regular expressions and discrete timed automata. So, all of discrete timed regular language can be described and verified by TITL formulas. We prove its satisfiability is not decidable in the dense time domain, but there exists some subsets of full version of the logic that can be decidable. And we prove full version of the logic can be decided in the discrete time domain. So, TITL model checking problem is decidable. We also prove TITL satisfiability checking is a non-elementary problem. As shown in the analysis, not operation and chop operation are embedded interleaved in the worst case, but the probability is very low. So, non-elementary complexity affects scarcely applications of TITL model checking.For automatic verification, we present a novel computational model named with timed normal form graph (TNFG). The fist step is to translate a TITL formula into a TNFG in order that there exists a one-to-one mapping between models of the formula and paths of the TNFG. The second step is to append accepting conditions to the TNFG in order to obtain the timed automaton modeling the TITL formula. The final step is to compute conduct automaton of two timed automata and decide whether the conduct automaton accept empty language or not. So, we obtain an algorithm for discrete TITL model checking based on TNFG. As shown in the complexity, our new algorithm reaches the lowest bound of inhabit problem complexity. As shown in the simulation results for some sample formulas, compared with the existing approaches, the new algorithm can produce lower state-space. And what's more, we give an algorithm for translating formulas in a subset of discrete duration calculus (DC) into discrete TITL formulas. So, model checking this subset of discrete DC can be solved with TNFG.In order to avoid complicated transformation from logic formulas to automata, we find an approach for unified TITL model checking. The first step is to construct a system model by a TITL formula. The second step is to describe a property with another TITL formula. So, unified TITL model checking problem is deduced to satisfiability checking problem that has been solved in this paper. Compared with common model checking techniques, the unified technique is benefit for refinement of real-time systems.In order to raise the describing power of real-time attacks and concurrent attacks, we present an approach for intrusion detection based on TITL model checking. The first step is to describe attack patterns with TITL formulas. The second step is to construct an audit log by automata. The final step is to verify automatically whether automata satisfy formulas, i.e. the log match the attack patterns, by TITL model checking algorithm. As shown in the simulation results, compared with the existing approaches for intrusion detection based on model checking, our new approach can detect efficiently various telnet attacks and password attacks.