Linear duration invariants (LDI) are important safety properties of real-time systems. They can be easily formulated in terms of a class of chop-free formulas in the Duration Calculus (DC). Compared to other temporal logics, the specification in DC is simpler, neater and more importantly easier to understand. However, directly model checking them is more difficult than model checking properties formulated in the computation tree logic (CTL). In this paper, we present a technique for the verification of the satisfaction of a LDI by a timed automaton by model checking a CTL property. For this, we construct an untimed automaton G from , and prove that satisfies iff is is satisfied by the set of all paths of G. To Verify that all paths of G satisfy , we construct a CTL formula ψ and simply check if G satisfies ψ. By this, we convert the problem of verification of the LDI to the problem of model checking CTL formula. As a result, the CTL model checking techniques and tools, such as UPPAAL, can be used for verification of LDI specified in the DC. © Springer-Verlag Berlin Heidelberg 2008.

Zhang M., Van Hung D., Liu Z.

451.pdf    Gửi cho bạn bè

Từ khóa : Automata theory; Error analysis; Real time systems; Translation (languages); Computation tree logic; CTL model checking; Directly model; Duration calculus; Linear duration; Safety properties; Timed automaton; Model checking