Romeo: A Tool for Analyzing Time Petri Nets

14 years 4 months ago

Download www.irccyn.ec-nantes.fr

In this paper, we present the features of Romeo, a Time Petri Net (TPN) analyzer. The tool Romeo allows state space computation of TPN and on-the-ﬂy model-checking of reachability properties. It performs translations from TPNs to Timed Automata (TAs) that preserve the behavioural semantics (timed bisimilarity) of the TPNs. Besides, our tool also deals with an extension of Time Petri Nets (SchedulingTPNs) modeling preemption. Key words: Time Petri nets, model-checking, state-space, DBM, polyhedron, scheduling, stopwatch.

Guillaume Gardey, Didier Lime, Morgan Magnin, Oliv

Real-time Traffic

CAV 2005 | Formal Methods | Romeo Allows State | Time Petri Nets | Timed Automata |

claim paper

» QPME 20 A Tool for Stochastic Modeling and Analysis Using Queueing Petri Nets

» An Efficient Translation of TimedArc Petri Nets to Networks of Timed Automata

» Modeling and Analyzing SMIL Documents in SAM

» Simulating Biological Pathways with a Continuous Petri Net Using RungeKutta Methods

» Cluster Grid based Responsetime analysis module for the PIPE Tool

» TAPAAL Editor Simulator and Verifier of TimedArc Petri Nets

» ITPNPerfBound A Performance Bound Tool for Interval Time Petri Nets

» HYPENS A Matlab Tool for Timed Discrete Continuous and Hybrid Petri Nets

Post Info
More Details (n/a)

Added	26 Jun 2010
Updated	26 Jun 2010
Type	Conference
Year	2005
Where	CAV
Authors	Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier H. Roux

Comments (0)

Sciweavers

Romeo: A Tool for Analyzing Time Petri Nets

CAV 2005 | Formal Methods | Romeo Allows State | Time Petri Nets | Timed Automata |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers