×

zbMATH — the first resource for mathematics

Using forward reachability analysis for verification of timed Petri nets. (English) Zbl 1168.68434
Summary: We consider verification of safety properties for concurrent real-timed systems modelled as timed Petri nets by performing symbolic forward reachability analysis. We introduce a formalism, called region generators, for representing sets of markings of timed Petri nets. Region generators characterize downward closed sets of regions and provide exact abstractions of sets of reachable states with respect to safety properties. We show that the standard operations needed for performing symbolic reachability analysis are computable for region generators. Since forward reachability analysis is necessarily incomplete, we introduce an acceleration technique to make the procedure terminate more often on practical examples. We have implemented a prototype for analyzing timed Petri nets and used it to verify a parameterized version of Fischer’s protocol. Lynch and Shavit’s mutual exclusion protocol and a producer-consumer protocol. We also used the tool to extract finite-state abstractions of these protocols.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
Uppaal; Kronos
PDF BibTeX Cite