×

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.)
Software:
Uppaal2k; VerICS
PDF BibTeX XML Cite