Publications of Olivier H. Roux

Journal papers

International Journal papers

[1] 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. Copyright Oxford Press. [ bib | http | .pdf | Abstract ]
[2] Louis-Marie Traonouez, Didier Lime, and Olivier (H.) Roux. Parametric model-checking of stopwatch petri nets. Journal of Universal Computer Science, A publication of Graz University of Technology and Universiti Malaysia Sarawak, 15(17):3273-3304, December 2009. [ bib | http | .pdf | Abstract ]
[3] Morgan Magnin, Pierre Molinaro, and Olivier (H.) Roux. Expressiveness of Petri nets with stopwatches. Dense-time part. Fundamenta Informaticae, 97(1-2):111-138, 2009. [ bib | http ]
[4] Morgan Magnin, Pierre Molinaro, and Olivier (H.) Roux. Expressiveness of Petri nets with stopwatches. Discrete-time part. Fundamenta Informaticae, 97(1-2):139-176, 2009. [ bib | http ]
[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. Copyright Springer. [ bib | http | .pdf | Abstract ]
[6] Charlotte Seidner and Olivier (H.) Roux. Formal Methods for Systems Engineering Behavior models. IEEE Transactions on Industrial Informatics. Special Issue on Formal Methods for Embedded Systems Design, 4(4):280-291, 2008. IEEE Computer Society Press. [ bib | .pdf | Abstract ]
[7] Marc Boyer and Olivier (H.) Roux. On the compared expressiveness of arc, place and transition time Petri nets. Fundamenta Informaticae, 88(3):225-249, 2008. Copyright IOS Press. [ bib | http | .pdf | Abstract ]
[8] Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier (H.) Roux. When are timed automata weakly timed bisimilar to time Petri nets? Theoretical Computer Science, 403(2-3):202-220, 2008. Copyright Elsevier. [ bib | .pdf ]
[9] 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. Copyright Springer. [ bib | .pdf | Abstract ]
[10] 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. Copyright Elsevier. [ bib | .pdf ]
[11] 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. Copyright Springer-Kluwer. [ bib | .pdf ]
[12] 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. Copyright Cambridge Press. [ bib | .pdf | Abstract ]
[13] 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. Copyright Hermes-Science. [ bib | .pdf | Abstract ]
[14] Olivier (H.) Roux and Pierre Molinaro. Deadlock detection and processing in Oreste. European Journal of Automation (RAIRO - APII - JESA), 30(4):519-542, 1996. [ bib ]

National Journal papers

[1] 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. [ bib ]
[2] Bernard Berthomieu, Didier Lime, Olivier (H.) Roux, and Francois Vernadat. Problèmes d'accessibilité et espaces d'états abstraits des réseaux de Petri temporels à chronomètres. Journal européen des systèmes automatisés - Numéro spécial en français sur la Modélisation des Systèmes Réactifs (MSR'05), 39(1-2-3):223-238, 2005. [ bib ]
[3] Olivier (H.) Roux and Pierre Molinaro. Detection en ligne des interblocages dans les systèmes répartis (on line distributed deadlock detection). Technique et Science Informatiques, 16(2):243-263, 1997. [ bib ]

Conference papers (since 2000)

International Conference papers

[1] Gilles Benattar, Béatrice Bérard, Didier Lime, John Mullins, Olivier H. Roux, and Mathieu Sassolas. Channel synthesis for finite transducers. In 13th International Conference, on Automata and Formal Languages (AFL'11), Debrecen, Hungary, August 2011. [ bib ]
[2] Y. Thierry-Mieg, B. Bérard, F. Kordon, D. Lime, and O. H. Roux. Compositional Analysis of Discrete Time Petri nets. In 1st workshop on Petri Nets Compositions (CompoNet 2011), volume 726, pages 17-31, Newcastle, UK, June 2011. CEUR. [ bib ]
[3] Louis-Marie Traonouez, Bartosz Grabiec, Claude Jard, Didier Lime, and Olivier H. Roux. Symbolic unfolding of parametric stopwatch petri nets. In Ahmed Bouajjani and Wei-Ngan Chin, editors, 8th International Symposium on Automated Technology for Verification and Analysis (ATVA 2010), volume 6252 of Lecture Notes in Computer Science, pages 291-305, Singapore, September 2010. Springer. [ bib ]
[4] Bartosz Grabiec, Louis-Marie Traonouez, Claude Jard, Didier Lime, and Olivier H. Roux. Diagnosis using unfoldings of parametric time petri nets. In Krishnendu Chatterjee and Thomas A. Henzinger, editors, 8th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 2010), volume 6246 of Lecture Notes in Computer Science, pages 137-151, Vienna, Austria, September 2010. Springer. [ bib ]
[5] Charlotte Seidner, Jean-Philippe Lerat, and Olivier H. Roux. Simulation and verification of dys]functional behavior models: Model checking for SE. In 20th International Symposium of the INCOSE, Chicago, IL, USA, July 2010. International Council on Systems Engineering. [ bib ]
[6] Gilles Benattar, Franck Cassez, Didier Lime, and Olivier H. Roux. Synthesis of Non-Interferent Timed Systems. In Proc. of the 7th Int. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS'09), volume 5813 of Lecture Notes in Computer Science, pages 28-42, Budapest, Hungary, September 2009. Copyright Springer. [ bib | Abstract ]
[7] Hanifa Boucheneb, Hind Rakay, and Olivier (H.) Roux. Time arc Petri nets and their analysis. In 9th Int. Conf. on Application of Concurrency to System Design (ACSD'09), Augsburg, Germany, July 2009. [ bib ]
[8] Didier Lime, Olivier H. Roux, Charlotte Seidner, and Louis-Marie Traonouez. Romeo: A parametric model-checker for Petri nets with stopwatches. In Stefan Kowalewski and Anna Philippou, editors, 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2009), volume 5505 of Lecture Notes in Computer Science, pages 54-57, York, United Kingdom, March 2009. Springer. [ bib ]
[9] 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 ]
[10] Morgan Magnin, Didier Lime, and Olivier (H.) Roux. Symbolic state space of stopwatch Petri nets with discrete-time semantics. In The 29th International Conference on Application and Theory of Petri Nets and other models of concurrency (ICATPN 2008), volume 5062 of Lecture Notes in Computer Science, pages 307-326, Xi'an, China, June 2008. Springer. [ bib | .pdf ]
[11] Charlotte Seidner, Jean-Philippe Lerat, and Olivier (H.) Roux. Usability and usefulness of formal verification in a system design process. In 18th International Symposium of the INCOSE, Utrecht, Netherlands, June 2008. International Council on Systems Engineering. [ bib ]
[12] Charlotte Seidner, Jean-Philippe Lerat, and Olivier (H.) Roux. Behavior diagrams model-checking: Formal methods applied to Systems Engineering and design. In 6th Annual Conference on Systems Engineering Research, Los Angeles, CA, USA, April 2008. University of Southern California. [ bib ]
[13] Dominique Bertrand, Anne-Marie Déplanche, Sébastien Faucou, and Olivier (H.) Roux. A study of the AADL mode change protocol. In Proceedings of the IEEE International Conference on Engineering Complex Computer Systems - ICECCS 2008 3rd International UML & AADL Workshop, pages 288-293, Belfast Irlande, 2008. IEEE Computer Society. [ bib ]
[14] Franck Cassez, John Mullins, and Olivier (H.) Roux. Synthesis of non-interferent distributed systems. In 4th Int. Conf. on Mathematical Methods, Models and Architectures for Computer Network Security (MMM-ACNS'07), volume 1 of Communications in Computer and Inform. Science, pages 159-170. Copyright Springer, September 2007. [ bib | .pdf | Abstract ]
[15] Charlotte Seidner, Jean-Philippe Lerat, and Olivier (H.) Roux. Usability of formal verification on EFFBD models: Applying Petri nets to Systems Engineering issues. In 17th International Symposium of the International Council on Systems Engineering (IS2007), San Diego, CA, June 2007. [ bib ]
[16] Marc Boyer and Olivier (H.) Roux. Comparison of the expressiveness of arc, place and transition time Petri nets. In 28th International Conference on Application and Theory of Petri Nets and other models of concurrency (ICATPN'07), volume 4546 of Lecture Notes in Computer Science, pages 63-82, Siedlce, Poland, jun 2007. Springer-Verlag. (See extended version in Fundamenta Informaticae). [ bib ]
[17] Guillaume Gardey, Olivier (F.) Roux, and Olivier (H.) Roux. Safety control synthesis for time Petri nets. In 8th International Workshop on Discrete Event Systems (WODES'06), pages 222-228, Ann Arbor, USA, July 2006. IEEE Computer Society Press. [ bib | .pdf | Abstract ]
[18] 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. [ bib ]
[19] Beatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier (H.) Roux. When are timed automata weakly timed bisimilar to time Petri nets ? In 25th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2005), volume 3821 of Lecture Notes in Computer Science, pages 273-284, Hyderabad, India, December 2005. Springer. [ bib | .pdf ]
[20] Beatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier (H.) Roux. Comparison of different semantics for time Petri nets. In Automated Technology for Verification and Analysis (ATVA'05), volume 3707 of Lecture Notes in Computer Science, pages 293-307, Taiwan, October 2005. Springer. [ bib | .pdf ]
[21] Beatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier (H.) Roux. Comparison of the expressiveness of timed automata and time Petri nets. In 3rd International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS 05), volume 3829 of Lecture Notes in Computer Science, pages 211-225, Uppsala, Sweden, September 2005. Springer. [ bib | .pdf ]
[22] Guillaume Gardey, John Mullins, and Olivier (H.) Roux. Non-interference control synthesis for security timed automata. In 3rd International Workshop on Security Issues in Concurrency (SecCo'05), Electronic Notes in Theoretical Computer Science, San Francisco, USA, August 2005. Elsevier. [ bib | .pdf ]
[23] 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), volume 3576 of Lecture Notes in Computer Science, pages 418-423, Edinburgh, Scotland, UK, July 2005. Springer. [ bib | .pdf ]
[24] 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), volume 144 of Electronic Notes in Theoretical Computer Science, pages 59-77, Edinburgh, Scotland, UK, July 2005. Elsevier. [ bib | .pdf ]
[25] 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. [ bib | .pdf ]
[26] 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. (See extended version in Journal of Systems and Software). [ bib ]
[27] Olivier (H.) Roux and Didier Lime. Time Petri nets with inhibitor hyperarcs. Formal semantics and state space computation. In The 25th International Conference on Application and Theory of Petri Nets, (ICATPN'04), volume 3099 of Lecture Notes in Computer Science, pages 371-390, Bologna, Italy, June 2004. Springer. Copyright Springer-Verlag. [ bib | .pdf ]
[28] 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 press. (See extended version in Journal of Discrete Event Dynamic Systems). [ bib | Abstract ]
[29] 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. [ bib | .pdf | Abstract ]
[30] Gilles Bernot, Franck Cassez, Jean-Paul Comet, Franck Delaplace, Céline Müller, Olivier Roux, and Olivier (H.) Roux. Semantics of Biological Regulatory Networks. In Vincent Danos and Cosimo Laneve, editors, Workshop on Concurrent Models in Molecular Biology (BioConcur 2003), Electronic Notes in Theoretical Computer Science, Marseille (France), September 2003. Elsevier's ENTCS series. Copyright Elsevier. [ bib | .pdf ]
[31] 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. [ bib | .pdf | Abstract ]
[32] Pierre Molinaro, David Delfieu, and Olivier (H.) Roux. Improving the calculus of the marking graph of Petri net with bdd like structure. In 2002 IEEE international conference on systems, man and cybernetics (SMC 02), Hammamet, Tunisia, October 2002. [ bib ]
[33] Olivier (H.) Roux, David Delfieu, and Pierre Molinaro. Discrete time approach of time Petri net for real-time systems analysis. In ETFA2001, pages 197-204, Nice, France, October 2001. IEEE Computer Society Press, Catalog number : 01TH8597 Volume 2. [ bib ]
[34] David Delfieu, Pierre Molinaro, and Olivier (H.) Roux. Analyzing temporal constraints with binary decision diagrams. In 25th IFAC Workshop on Real-Time Programming (WRTP'00), pages 131-136, Palma, Spain, 2000. [ bib ]
[35] David Delfieu, Pierre Molinaro, and Olivier (H.) Roux. Coupling binary decision diagrams with time Petri net. In 8th international conference on Real-Time and Embedded Systems, pages 122-135, 2000. [ bib ]

National Conference papers

[1] Didier Lime, Claude Martinez, and Olivier (H.) Roux. Coercition temporelle de réseau de petri. 8ieme Colloque sur la Modélisation des Systèmes Réactifs, (MSR'11), Journal européen des systèmes automatisés (JESA), 45(1-2-3):13-28, 2011. [ bib ]
[2] Hanifa Boucheneb, Hind Rakay, and Olivier (H.) Roux. Réseaux de Petri à arcs temporels généralisés aux sémantiques faible et forte. In 6ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'07), Lyon, France, October 2007. [ bib ]
[3] Louis-Maire Traonouez, David Delfieu, and Olivier (H.) Roux. Synthèse de contraintes de conception à partir de réseaux de Petri temporels paramétrés. In 6ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'07), Lyon, France, October 2007. [ bib ]
[4] Charlotte Seidner, Jean-Philippe Lerat, Olivier (H.) Roux, and Morgan Magnin. Vérification dynamique et formelle d'un système décrit par son architecture fonctionnelle à l'aide de réseaux de Petri temporels : promesses et perspectives. In 4th AFIS National Conference, Toulouse, France, May 2006. [ bib ]
[5] Bernard Berthomieu, Didier Lime, Olivier (H.) Roux, and Francois Vernadat. Problèmes d'accessibilité et espaces d'états abstraits des réseaux de Petri temporels à chronomètres. In 5ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'05), Grenoble, France, October 2005. [ bib ]
[6] 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. [ bib | Abstract ]
[7] Olivier (H.) Roux and Anne-Marie Déplanche. Extension des réseaux de Petri t-temporels pour la modélisation de l'ordonnancement de tâches temps-réel. In 3ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'01), pages 327-342, Toulouse, France, October 2001. Hermes Science. Copyright Hermes-Science. [ bib ]

International conferences and workshops without proceedings

[1] Gilles Benattar, Béatrice Bérard, Didier Lime, John Mullins, Olivier (H.) Roux, and Mathieu Sassolas. Covert Channels with Transducers. In the LICS Workshop on Foundations of Computer Security (FCS'09), Los Angeles, California, USA, August 2009. [ bib ]

Books and Special Issue (as co-Editor)

Books

[1] Claude Jard and Olivier (H.) Roux, editors. Communicating Embedded Systems - Software and Design. ISTE Publishing / John Wiley, October 2009. ISBN:978-1-8482-1143-8. [ bib ]
[2] Claude Jard and Olivier (H.) Roux, editors. Approches formelles des systèmes embarqués communicants. Traité IC2. Hermes Lavoisier, 2008. ISBN: 978-2-7462-1942-7. [ bib | .html ]

Special Issue (as co-Editor)

[1] Claude Martinez and Olivier (H.) Roux, editors. Special issue on Modeling of Reactive Systems, volume 21, number 3 of journal of Discrete Event Dynamic Systems (DEDS). Springer, 2011. [ bib ]

Chapters

[1] Didier Lime, Olivier H. Roux, and Jiří Srba. Models for real-time embedded systems. In Communicating Embedded Systems - Software and Design, pages 1-37. ISTE Publishing / John Wiley, 2009. [ bib ]
[2] Alexandre David, Gerd Behrmann, Peter Bulychev, Joakim Byg, Thomas Chatain, Kim G. Larsen, Paul Pettersson, Jacob I. Rasmussen, Jiří Srba, Wang Yi, Kenneth Y. Joergensen, Didier Lime, Morgan Magnin, Olivier H. Roux, and Louis-Marie Traonouez. Tools for model-checking timed systems. In Communicating Embedded Systems - Software and Design, pages 165-225. ISTE Publishing / John Wiley, 2009. [ bib ]
[3] Franck Cassez and Olivier (H.) Roux. From Time Petri nets to Timed Automata. In Petri Net: Theory and Application. Edited by Vedran Kordic, I-Tech Publishing, Vienna, Austria, 2008. ISBN 978-3-902613-12-7. [ bib ]
[4] Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier H. Roux. Comparison of expressiveness for timed automata and time Petri nets. In Vangelis Th. Paschos, editor, Combinatorial Optimization and Theoretical Computer Science, pages 93-144. ISTE Publishing / John Wiley, January 2008. [ bib ]
[5] Didier Lime and Olivier (H.) Roux. Les modèles pour les systèmes temps réel embarqués. In Approches formelles des systèmes embarqués communicants, pages 45-74. Traité IC2, Hermes Lavoisier, 2008. [ bib ]

Edited Proceedings

[1] Didier Lime and Olivier (H.) Roux, editors. Modélisation des systèmes réactifs, volume 43(7-9) of Journal Européen des Systèmes Automatisés (JESA). Hermes, November 2009. [ bib ]
[2] Andras Horváth and Olivier (H.) Roux, editors. Proceedings of 1st International Workshop on Timing and Stochasticity in Petri nets and other models of concurrency. June 2009. [ bib | .html ]
[3] Sebastien Faucou, Didier Lime, and Olivier (H.) Roux, editors. Proceedings of the Summer School ETR'2007. IRCCyN, Nantes, France, September 2007. [ bib | http | .pdf ]

Misc

[1] Marc Boyer and Olivier (H.) Roux. Comparison of the expressiveness w.r.t. timed bisimilarity of k-bounded arc, place and transition time Petri nets with weak and strong single server semantics. Technical Report IRCCyN number RI2006-15, 2006. [ bib ]
[2] Olivier (H.) Roux. Vérification des réseaux de Petri temporels et à chronomètres. Habilitation à Diriger les Recherches (HDR), IRCCyN, University of Nantes, France, December 2005. [ bib | .pdf ]
[3] Beatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier (H.) Roux. Comparison of the expressiveness of timed automata and time Petri nets. Technical Report IRCCyN number R2005-2, 2005. [ bib ]
[4] Bernard Berthomieu, Didier Lime, Olivier (H.) Roux, and Francois Vernadat. Reachability problems and abstract state spaces for time Petri nets with stopwatches. Technical Report LAAS number 04483, October 2004. Rapport du LAAS. [ bib ]
[5] Didier Lime and Olivier (H.) Roux. Computing the state class time automaton of a transition-time Petri net. Technical Report IRCCyN number 1497 R2003_0, 2003. [ bib ]
[6] Franck Cassez and Olivier (H.) Roux. From time Petri nets to timed automata. Technical Report IRCCyN number 1496 R2003_4, 2003 updated in 2004. [ bib ]
[7] Hanifa Boucheneb, Guillaume Gardey, and Olivier (H.) Roux. TCTL model checking of time Petri nets. Technical Report IRCCyN number RI2006-14, 2006 updated in 2008. [ bib | .pdf ]