A Bounded Model Checker for Timed Automata and Its Application to LTL Properties

Model checking with a time aspect is often used in verification on hardware and embedded systems. Timed automata are often used for such models. UPPAAL is a world-wide famous model checking tool for timed automata; however, UPPAAL is a Computational Tree Logic (CTL)-based model checking tool and cannot use Linear Temporal Logic (LTL) properties. Bounded model checking uses LTL (Linear Time Logic) for a checking formula. Bounded model checking specifies a boundary k and obtains counterexamples by searching from the initial state of a system to states reachable by k-steps. There are several studies on bounded model checking. Sorea has proposed a concrete algorithm for a timed automaton. There are, however, no clear details on how to implement bounded model checking tools for timed automata, and study the performance. Another problem is that the timed automaton covered by the method does not support general variables except for clock variables. The objective of this study is to implement a bounded model checking tool using LTL for timed automata. We also improve Sorea's method so that it can handle extended timed automata that handle general variables. This paper also presents some LTL examples from texts on requirement specifications for embedded systems and the results of applying the tool to them.