×

zbMATH — the first resource for mathematics

Romeo: A tool for analyzing time Petri nets. (English) Zbl 1081.68618
Etessami, Kousha (ed.) et al., Computer aided verification. 17th international conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27231-3/pbk). Lecture Notes in Computer Science 3576, 418-423 (2005).
Summary: 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.
For the entire collection see [Zbl 1078.68004].

MSC:
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:
TINA; Oris; Romeo
PDF BibTeX Cite
Full Text: DOI