2005 | OriginalPaper | Chapter
Romeo: A Tool for Analyzing Time Petri Nets
Authors : Guillaume Gardey, Didier Lime, Morgan Magnin, Olivier (H. ) Roux
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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-fly 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 (
Scheduling-TPNs
) for which the valuations of transitions may be stopped and resumed, thus allowing the modeling preemption.