Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Roux, O.H., Déplanche, A.M.: A t-time Petri net extension for real time-task scheduling modeling. European Journal of Automation (JESA) 36(7), 973–987 (2002)
Bucci, G., Fedeli, A., Sassoli, L., Vicario, E.: Time state space analysis of real-time preemptive systems. IEEE transactions on software engineering 30, 97–111 (2004)
Cassez, F., Roux, O.H.: Structural translation from time Petri nets to timed automata. In: Cassez, F., Roux, O.H. (eds.) Fourth International Workshop on Automated Verification of Critical Systems (AVoCS 2004), London (UK). ENTCS, Elsevier, Amsterdam (2004)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE trans. on software engineering 17, 259–273 (1991)
Gardey, G., Roux, O.H., Roux, O.F.: State space computation and analysis of time Petri nets. Theory and Practice of Logic Programming (TPLP). Special Issue on Specification Analysis and Verification of Reactive Systems (2005) (to appear)
Lime, D., Roux, O.H.: State class timed automaton of a time Petri net. In: 10th International Workshop on Petri Nets and Performance Models, PNPM 2003 (2003)
Lime, D., Roux, O.H.: A translation based method for the timed analysis of scheduling extended time Petri nets. In: The 25th IEEE RTSS 2004, Lisbon, Portugal (2004)
Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool tina – construction of abstract state spaces for petri nets and time petri nets. International Journal of Production Research 42 (2004), Tool available at http://www.laas.fr/tina/
Bucci, G., Sassoli, L., Vicario, E.: Oris: A tool for state-space analysis of real-time preemptive systems. In: Quantitative Evaluation of Systems, First International Conference on (QEST 2004), pp. 70–79 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gardey, G., Lime, D., Magnin, M., Roux, O.(.). (2005). Romeo: A Tool for Analyzing Time Petri Nets. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_41
Download citation
DOI: https://doi.org/10.1007/11513988_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)