1997 Volume 12 Issue 3 Pages 448-455
Real-time systems consist of many concurrent processes and behave on strict timing conditions. It is important to verify the timing conditions of real-time systems. In this paper, we propose extended real-time temporal logic and effective real-time model checking as follows. (1) The timing description of extended real-time temporal logic consists of both freeze quantification and branching time structure in dense time model. For this extension, extended real-time temporal logic admits timing constraints between distant contexts. (2) System specification is described by parallel composition of timed automata. Timed Kripke structure is automatically generated from timed automaton. (3) Real time model checking consists of both labelling algorithm and geometric region. This method is shown effective by some example.