Papers

Tool papers

[1] Didier Lime, Olivier H. Roux, Charlotte Seidner and Louis-Marie Traonouez. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), Lecture Notes in Computer Science, March 2009, York, United Kingdom. Springer.

[2] Guillaume Gardey, Didier Lime, Morgan Magnin, and Olivier (H.) Roux. Roméo: A tool for analyzing time Petri nets. In 17th International Conference on Computer Aided Verification (CAV’05), Lecture Notes in Computer Science, Edinburgh, Scotland, UK, July 2005. Springer. [Slides].

Journal papers

[1] Aleksandra Jovanović, Didier Lime, and Olivier (H.) Roux. Integer Parameter Synthesis for Real-Time Systems. IEEE Transactions on Software Engineering (TSE), 41(5):445-461, 2015.

[2] Claude Jard, Didier Lime, and Olivier H. Roux. Blending Timed Formal Models with Clock Transition Systems. Fundamenta Informaticae, 129(1-2):85-100, 2014.

[3] Louis-Marie Traonouez, Didier Lime, and Olivier (H.) Roux. Parametric model-checking of stopwatch Petri nets. Journal of Universal Computer Science, 15(17):3273-3304, December 2009. Graz University of Technology and Universiti Malaysia Sarawak.

[4] Hanifa Boucheneb, Guillaume Gardey, and Olivier (H.) Roux. TCTL model checking of time Petri nets. Journal of Logic and Computation, 19(6):1509-1540, December 2009. Oxford Press.

[5] Didier Lime and Olivier (H.) Roux. Formal verification of real-time systems with preemptive scheduling. Journal of Real-Time Systems, 41(2):118-151, 2009. Springer

[6] Bernard Berthomieu, Didier Lime, Olivier (H.) Roux, and Francois Vernadat. Reachability problems and abstract state spaces for time Petri nets with stopwatches. Journal of Discrete Event Dynamic Systems - Theory and Applications (DEDS), 17(2):133-158, 2007. Springer

[7] Franck Cassez and Olivier (H.) Roux. Structural translation from Time Petri Nets to Timed Automata - Model-Checking Time Petri Nets via Timed Automata. The journal of Systems and Software, 79(10):1456-1468, 2006. Elsevier

[8] Didier Lime and Olivier (H.) Roux. Model checking of time Petri nets using the state class timed automaton. Journal of Discrete Events Dynamic Systems - Theory and Applications (DEDS), 16(2):179-205, 2006. Kluwer-Springer

[9] Guillaume Gardey, Olivier (H.) Roux, and Olivier (F.) Roux. 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, 6(3):301-320, 2006. Cambridge Press.

[10] Didier Lime and Olivier (H.) Roux. Vérification formelle des systèmes temps réel avec ordonnancement préemptif. Technique et Science Informatiques, 25(3):347-375, 2006. Hermès-Science.

[11] Olivier (H.) Roux and Anne-Marie Déplanche. A t-time Petri net extension for real time-task scheduling modeling. European Journal of Automation (JESA), 36(7):973-987, 2002. Hermès-Science.

Conference papers

[1] Étienne André, Didier Lime, and Olivier H. Roux. Almost-complete synthesis for bounded parametric timed automata. In The 9th International Workshop on Reachability Problems, volume 9328 of Lecture Notes in Computer Science, Warsaw, Poland, September 2015

[2] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for timed automata. In Nir Piterman and Scott Smolka, editors, 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), volume 7795 of Lecture Notes in Computer Science, pages 401-415, Roma, Italy, March 2013.

[3] Louis-Marie Traonouez, Didier Lime, and Olivier H. Roux. Parametric model-checking of time Petri nets with stopwatches using the state-class graph. In 6th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2008), volume 5215 of Lecture Notes in Computer Science, pages 280-294, Saint-Malo, France, September 2008. Springer. [ bib | .pdf ]

[4] Morgan Magnin, Pierre Molinaro, and Olivier (H.) Roux. Decidability, expressivity and state-space computation of stopwatch Petri nets with discrete-time semantics. In 8th International Workshop on Discrete Event Systems (WODES’06), pages 33-38, Ann Arbor, USA, July 2006. IEEE Computer Society Press.

[5] Morgan Magnin, Didier Lime, and Olivier (H.) Roux. An efficient method for computing exact state space of Petri nets with stopwatches. In third International Workshop on Software Model-Checking (SoftMC’05), Electronic Notes in Theoretical Computer Science, Edinburgh, Scotland, UK, July 2005. Elsevier.

[6] Didier Lime and Olivier (H.) Roux. A translation based method for the timed analysis of scheduling extended time Petri nets. In The 25th IEEE International Real-Time Systems Symposium, (RTSS’04), pages 187-196, Lisbon, Portugal, December 2004. IEEE Computer Society Press.

[7] Franck Cassez and Olivier (H.) Roux. Structural translation from time Petri nets to timed automata. In Fourth International Workshop on Automated Verification of Critical Systems (AVoCS’04), Electronic Notes in Theoretical Computer Science, London (UK), September 2004. Elsevier.

[8] Franck Cassez and Olivier (H.) Roux. Traduction structurelle des réseaux de Petri temporels vers les automates temporisés. In 4ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR’03), Metz, France, October 2003. Copyright Hermes-Science.

[9] Didier Lime and Olivier (H.) Roux. State class timed automaton of a time Petri net. In The 10th International Workshop on Petri Nets and Performance Models, (PNPM’03), pages 124-133, Urbana, USA, September 2003. IEEE Computer Society. Copyright IEEE Computer Society.

[10] Guillaume Gardey, Olivier (H.) Roux, and Olivier (F.) Roux. A zone-based method for computing the state space of a time Petri net. In In Formal Modeling and Analysis of Timed Systems, (FORMATS’03), volume 2791 of Lecture Notes in Computer Science, pages 246-259, Marseille, France, September 2003. Springer. Copyright Springer-Verlag.

[11] Didier Lime and Olivier (H.) Roux. Expressiveness and analysis of scheduling extended time Petri nets. In 5th IFAC International Conference on Fieldbus Systems and their Applications, (FET’03), pages 193-202, Aveiro, Portugal, July 2003. Elsevier Science. Copyright Elsevier Science.

Technical reports

[1] Hanifa Boucheneb, Guillaume Gardey and Olivier (H.) Roux. TCTL model checking of Time Petri Nets. IRCCyN Technical report number RI2006-14. [pdf]

Powered by WordPress with Pool theme design by Borja Fernandez. Roméo logo design by Jean-Luc Bechennec.
Entries and comments feeds. Valid XHTML and CSS. ^Top^