Sciweavers

Share
ENTCS
2006

An Efficient Method for Computing Exact State Space of Petri Nets With Stopwatches

11 years 11 months ago
An Efficient Method for Computing Exact State Space of Petri Nets With Stopwatches
In this paper, we address the issue of the formal verification of real-time systems in the context of a preemptive scheduling policy. We propose an algorithm which computes the state-space of the system, modeled as a time Petri net with stopwatches, exactly and efficiently, by the use of Difference Bounds Matrices (DBM) whenever possible and automatically switching to more time and memory consuming general (convex) polyhedra only when required. We propose a necessary and sufficient condition for the need of general polyhedra. We give experimental results comparing our implementation of the method to a full DBM over-approximation and to an exact computation with only general polyhedra. Key words: real-time systems, time Petri nets, polyhedra
Morgan Magnin, Didier Lime, Olivier H. Roux
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Morgan Magnin, Didier Lime, Olivier H. Roux
Comments (0)
books