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
Issue Date:
2008
Publisher:
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Citation:
Volume: 5160 LNCS, Page : 395-409
Abstract:
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.
