zbMATH — the first resource for mathematics

Slicing of timed automata with discrete data. (English) Zbl 1097.68061
Summary: The paper proposes how to use static analysis to extract an abstract model of a system. The method uses techniques of program slicing to examine syntax of a system modeled as a set of timed automata with discrete data, a common input formalism of model checkers dealing with time. The method is property driven. The abstraction is exact with respect to all properties expressed in the temporal logic $$\text{CTL}_{-X^*}$$.
MSC:
 68Q45 Formal languages and automata 68Q60 Specification and verification (program logics, model checking, etc.) 68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Uppaal2k; VerICS