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 26 articles , 1 standard article )

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

1 2 next

  1. Fahrenberg, Uli; Legay, Axel; Quaas, Karin: Computing branching distances with quantitative games (2020)
  2. Bouyer, Patricia; Fahrenberg, Uli; Larsen, Kim Guldstrand; Markey, Nicolas; Ouaknine, Joël; Worrell, James: Model checking real-time systems (2018)
  3. André, Étienne; Benmoussa, Mohamed Mahdi; Choppy, Christine: Formalising concurrent UML state machines using coloured Petri nets (2016)
  4. Jensen, Peter Gjøl; Larsen, Kim Guldstrand; Srba, Jiří: Real-time strategy synthesis for timed-arc Petri net games via discretization (2016)
  5. Klai, Kais: Timed aggregate graph: a finite graph preserving event- and state-based quantitative properties of time Petri nets (2015)
  6. 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)
  7. Lime, Didier; Martinez, Claude; Roux, Olivier H.: Shrinking of time Petri nets (2013)
  8. Balaguer, Sandie; Chatain, Thomas; Haar, Stefan: A concurrency-preserving translation from time Petri nets to networks of timed automata (2012)
  9. 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)
  10. Lepri, Daniela; Ábrahám, Erika; Ölveczky, Peter Csaba: Timed CTL model checking in Real-Time Maude (2012)
  11. Jacobsen, Lasse; Jacobsen, Morten; Møller, Mikael H.; Srba, Jiří: Verification of timed-arc Petri nets (2011)
  12. de Lara, Juan; Vangheluwe, Hans: Automating the transformation-based analysis of visual languages (2010)
  13. Grabiec, Bartosz; Traonouez, Louis-Marie; Jard, Claude; Lime, Didier; Roux, Olivier H.: Diagnosis using unfoldings of parametric time Petri nets (2010)
  14. Penczek, Wojciech; Pòłrola, Agata; Zbrzezny, Andrzej: SAT-based (parametric) reachability for a class of distributed time Petri nets (2010)
  15. Traonouez, Louis-Marie; Grabiec, Bartosz; Jard, Claude; Lime, Didier; Roux, Olivier H.: Symbolic unfolding of parametric stopwatch Petri nets (2010)
  16. Boucheneb, Hanifa; Gardey, Guillaume; Roux, Olivier H.: TCTL model checking of time Petri nets (2009)
  17. Lime, Didier; Roux, Olivier H.: Formal verification of real-time systems with preemptive scheduling (2009)
  18. Stöcker, Jan; Lang, Frédéric; Garavel, Hubert: Parallel processes with real-time and data: the ATLANTIF intermediate format (2009)
  19. Abdelli, Abdelkrim; Badache, Nadjib: Towards building the state class graph of the TSPN model (2008)
  20. Bérard, B.; Cassez, F.; Haddad, S.; Lime, D.; Roux, O. H.: When are timed automata weakly timed bisimilar to time Petri nets? (2008)

1 2 next