Romeo: A tool for analyzing time Petri nets. 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.

References in zbMATH (referenced in 21 articles , 1 standard article )

Showing results 1 to 20 of 21.
Sorted by year (citations)

1 2 next

  1. André, Étienne; Benmoussa, Mohamed Mahdi; Choppy, Christine: Formalising concurrent UML state machines using coloured Petri nets (2016)
  2. Byg, Joakim; Jacobsen, Morten; Jacobsen, Lasse; Jørgensen, Kenneth Yrke; Møller, Mikael Harkjær; Srba, Jiří: TCTL-preserving translations from timed-arc Petri nets to networks of timed automata (2014)
  3. Lime, Didier; Martinez, Claude; Roux, Olivier H.: Shrinking of time Petri nets (2013)
  4. Balaguer, Sandie; Chatain, Thomas; Haar, Stefan: A concurrency-preserving translation from time Petri nets to networks of timed automata (2012)
  5. David, Alexandre; Jacobsen, Lasse; Jacobsen, Morten; Jørgensen, Kenneth Yrke; Møller, Mikael H.; Srba, Jiří: TAPAAL 2.0: integrated development environment for timed-arc Petri nets (2012)
  6. Lepri, Daniela; Ábrahám, Erika; Ölveczky, Peter Csaba: Timed CTL model checking in real-time Maude (2012)
  7. de Lara, Juan; Vangheluwe, Hans: Automating the transformation-based analysis of visual languages (2010)
  8. Grabiec, Bartosz; Traonouez, Louis-Marie; Jard, Claude; Lime, Didier; Roux, Olivier H.: Diagnosis using unfoldings of parametric time Petri nets (2010)
  9. Penczek, Wojciech; Pòłrola, Agata; Zbrzezny, Andrzej: SAT-based (parametric) reachability for a class of distributed time Petri nets (2010)
  10. Traonouez, Louis-Marie; Grabiec, Bartosz; Jard, Claude; Lime, Didier; Roux, Olivier H.: Symbolic unfolding of parametric stopwatch Petri nets (2010)
  11. Boucheneb, Hanifa; Gardey, Guillaume; Roux, Olivier H.: TCTL model checking of time Petri nets (2009)
  12. Lime, Didier; Roux, Olivier (H.): Formal verification of real-time systems with preemptive scheduling (2009)
  13. Stöcker, Jan; Lang, Frédéric; Garavel, Hubert: Parallel processes with real-time and data: the ATLANTIF intermediate format (2009)
  14. Abdelli, Abdelkrim; Badache, Nadjib: Towards building the state class graph of the TSPN model (2008)
  15. Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; Roux, O.H.: When are timed automata weakly timed bisimilar to time Petri nets? (2008)
  16. Magnin, Morgan; Lime, Didier; Roux, Olivier H.: Symbolic state space of stopwatch Petri nets with discrete-time semantics (theory paper) (2008)
  17. Srba, Jiří: Comparing the expressiveness of timed automata and timed extensions of Petri nets (2008)
  18. Berthomieu, Bernard; Lime, Didier; Roux, Olivier H.; Vernadat, François: Reachability problems and abstract state spaces for time Petri nets with stopwatches (2007)
  19. Cassez, Franck; Chatain, Thomas; Jard, Claude: Symbolic unfoldings for networks of timed automata (2006)
  20. Bérard, Beatrice; Cassez, Franck; Haddad, Serge; Lime, Didier; Roux, Olivier H.: Comparison of the expressiveness of timed automata and time Petri nets (2005)

1 2 next