Publications of Olivier H. Roux

Journal papers

International Journal papers

[1] Imane Haur, Jean-Luc Béchennec, and Olivier H. Roux. Model-checking of concurrent real-time software using High-Level Colored Time Petri Nets with stopwatches. Cybernetics and Systems, pages 1-31, September 2023. Taylor & Francis. [ bib | DOI | http ]
[2] Imane Haur, Jean-Luc Béchennec, and Olivier H. Roux. Formal verification process of the compliance of a multicore AUTOSAR OS. Software Quality Journal, 31(2):497-531, June 2023. Springer. [ bib | DOI ]
[3] Rémi Parrot, Mikaël Briday, and Olivier H. Roux. Design and verification of pipelined circuits with timed petri nets. Discrete Event Dynamic Systems - Theory and Applications (DEDS), 33(1):1-24, December 2022. Springer. [ bib | DOI ]
[4] Antoine Bernabeu, Jean-Luc Béchennec, Mikaël Briday, Sébastien Faucou, and Olivier H. Roux. Cost-optimal timed trace synthesis for scheduling of intermittent embedded systems. Discrete Event Dynamic Systems - Theory and Applications (DEDS), 33(1):63-93, December 2022. Springer. [ bib | DOI ]
[5] Étienne André, Didier Lime, and Olivier H. Roux. Reachability and liveness in parametric timed automata. Logical Methods in Computer Science, 18(1):1-31, February 2022. [ bib | .pdf ]
[6] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Control of Real-time Systems with Integer Parameters. IEEE Transactions on Automatic Control, 67(1):75-88, January 2022. [ bib | DOI ]
[7] Didier Lime, Olivier H. Roux, and Charlotte Seidner. Cost problems for parametric time petri nets. Fundamenta Informaticae, 183(1-2):97-123, 2021. [ bib | DOI | .pdf ]
[8] Jean-Luc Bechennec, Didier Lime, and Olivier H. Roux. Logical Time Control of concurrent DES. Discrete Event Dynamic Systems - Theory and Applications (DEDS), 31(2):185-217, 2021. Springer. [ bib | DOI ]
[9] Thomas Chatain, Maurice Comlan, David Delfieu, Loig Jezequel, and Olivier H. Roux. Pomset Bisimulation and Unfolding for Reset Petri Nets. Information and Computation, 283:104674, 2020. issn 0890-5401, Elsevier. [ bib | DOI ]
[10] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. A Game Approach to the Parametric Control of Real-time Systems. International Journal of Control, 92(9):2025-2036, 2019. Taylor and Francis. [ bib | DOI ]
[11] Jean-Luc Béchennec, Matthias Brun, Sébastien Faucou, Louis-Marie Givel, and Olivier H. Roux. Testing Real Time Systems with runtime enforcement. IEEE Design & Test, 35(4):31-37, August 2018. IEEE. [ bib | DOI ]
[12] Toussaint Tigori, Jean-Luc Béchennec, Sébastien Faucou, and Olivier H. Roux. Formal model-based synthesis of application specific static RTOS. ACM Transactions on Embedded Computing Systems, 16(4):97:1-97:25, May 2017. [ bib | DOI ]
[13] Nicolas Beldiceanu, Bárbara Dumas Feris, Philippe Gravey, Sabbir Hasan, Claude Jard, Thomas Ledoux, Yunbo Li, Didier Lime, Gilles Madi-Wamba, Jean-Marc Menaud, Pascal Morel, Michel Morvan, Marie-Laure Moulinard, Anne-Cécile Orgerie, Jean-Louis Pazat, Olivier H. Roux, and Ammar Sharaiha. Towards energy-proportional Clouds partially powered by renewable energy. Computing, 99(1), January 2017. [ bib | DOI ]
[14] Johan Girault, Jean-Jacques Loiseau, and Olivier H. Roux. On-line compositional controller synthesis for AGV. Discrete Event Dynamic Systems - Theory and Applications (DEDS), 26(4):583-610, 2016. Springer. [ bib | DOI | .pdf ]
[15] 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. [ bib | DOI | .pdf ]
[16] Gilles Benattar, Franck Cassez, Didier Lime, and Olivier H. Roux. Control and Synthesis of Non-Interferent Timed Systems. International Journal of Control, 88(2):217-236, 2015. Taylor and Francis. [ bib | http | .pdf ]
[17] Claude Jard, Didier Lime, and Olivier H. Roux. Blending Timed Formal Models with Clock Transition Systems. Fundamenta Informaticae, 129(1-2):85-100, 2014. [ bib | .pdf ]
[18] Cédrick Lelionnais, Matthias Brun, Jérôme Delatour, Olivier H. Roux, and Charlotte Seidner. Formal synthesis of real-time system models in a MDE approach. International Journal on Advances in Systems and Measurement, 7(1-2), 2014. [ bib | http ]
[19] Claude Jard, Didier Lime, Olivier H. Roux, and Louis-Marie Traonouez. Symbolic unfolding of parametric stopwatch Petri nets. Formal Methods in System Design (FMSD), 43(3):493-519, 2013. Springer. [ bib | .pdf ]
[20] Didier Lime, Claude Martinez, and Olivier H. Roux. Shrinking of time Petri nets. Journal of Discrete Event Dynamic Systems - Theory and Applications (DEDS), 23(4):419-438, 2013. Springer. [ bib | .pdf ]
[21] Béatrice Bérard, Franck Cassez, Serge Haddad, Didier Lime, and Olivier H. Roux. The expressive power of time Petri nets. Theoretical Computer Science (TCS), 474:1-20, 2013. Elsevier. [ bib | http | .pdf ]
[22] Gilles Benattar, Béatrice Bérard, Didier Lime, John Mullins, Olivier H. Roux, and Mathieu Sassolas. Channel synthesis for finite transducers. International Journal of Foundations of Computer Science, 23(6):1241-1260, 2012. [ bib | http | .pdf ]
[23] 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 ]
[24] 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 ]
[25] 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 ]
[26] 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 ]
[27] 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 ]
[28] 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 ]
[29] 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 ]
[30] 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 ]
[31] 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 ]
[32] 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 ]
[33] 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 ]
[34] 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 ]
[35] 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 ]
[36] 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] Johan Girault, Jean-Jacques Loiseau, and Olivier H. Roux. Synthèse en ligne de superviseur compositionnel pour flotte de robots mobiles. Journal européen des systèmes automatisés - Numéro spécial en français issu du colloque Modélisation des Systèmes Réactifs (MSR'13), 47(1-3):195-210, 2013. [ bib ]
[2] Didier Lime, Claude Martinez, and Olivier H. Roux. Coercition temporelle de réseaux de Petri. Journal européen des systèmes automatisés - Numéro spécial en français issu du colloque Modélisation des Systèmes Réactifs (MSR'11), 45(1-3):13-28, 2011. [ bib ]
[3] 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 ]
[4] 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 issu du colloque Modélisation des Systèmes Réactifs (MSR'05), 39(1-3):223-238, 2005. [ bib ]
[5] Olivier H. Roux and Pierre Molinaro. Détection 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] Jan Komenda, Sébastien Lahaye, Rémi Parrot, and Olivier H. Roux. Weakly strong semantics of Time Petri Nets for performance evaluations. In 17th IFAC Workshop on Discrete Event Systems (WODES'24), Rio de Janeiro, Brazil, April 2024. IFAC. [ bib ]
[2] Anthony Spriet, Didier Lime, and Olivier H. Roux. Timed non-interference under partial observability and bounded memory. In 21st International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2023), volume 14138 of Lecture Notes in Computer Science, pages 122-137, Antwerp, Belgium, September 2023. Springer. [ bib ]
[3] Loriane Leclercq, Didier Lime, and Olivier H. Roux. A state class based controller synthesis approach for Time Petri Nets. In The 44th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2023), volume 13929 of Lecture Notes in Computer Science, Lisbon, Portugal, June 2023. Springer. [ bib ]
[4] Imane Haur, Jean-Luc Béchennec, and Olivier H. Roux. Formal verification of the inter-core synchronization of a multi-core RTOS kernel. In 23th International Conference on Formal Engineering Methods (ICFEM 2022), volume 13478 of Lecture Notes in Computer Science, Madrid, Spain, October 2022. Springer. [ bib ]
[5] Rémi Parrot, Hanifa Boucheneb, Mikaël Briday, and Olivier H. Roux. Expressiveness and analysis of Timed Petri Nets. In 16th IFAC Workshop on Discrete Event Systems (WODES'22), Prague, Czechia, September 2022. IFAC. [ bib ]
[6] Imane Haur, Jean-Luc Béchennec, and Olivier H. Roux. High-level Colored Time Petri Nets for true concurrency modeling in real-time software. In International Conference on Control, Decision and Information Technologies (CODIT 2022), Istanbul, Turkey, May 2022. [ bib ]
[7] Rémi Parrot, Mikaël Briday, and Olivier H. Roux. Pipeline Optimization using a Cost Extension of Timed Petri Nets. In The 28th IEEE International Symposium on Computer Arithmetic (ARITH 2021). IEEE, June 2021. [ bib ]
[8] Serge Haddad, Didier Lime, and Olivier H. Roux. A Turn-Based Approach for Qualitative Time Concurrent Games. In The 42th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021), volume 12734 of Lecture Notes in Computer Science. Springer, June 2021. [ bib ]
[9] Rémi Parrot, Mikaël Briday, and Olivier H. Roux. Timed Petri Nets with Reset for Pipelined Synchronous Circuit Design. In The 42th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2021), volume 12734 of Lecture Notes in Computer Science. Springer, June 2021. [ bib ]
[10] Imane Haur, Jean-Luc Béchennec, and Olivier H. Roux. Formal schedulability analysis based on multi-core RTOS model. In The 29th International Conference on Real-Time Networks and Systems (RTNS 2021), 2021. [ bib ]
[11] Joumana Lagha, Jean-Luc Béchennec, Sébastien Faucou, and Olivier H. Roux. Toward an Exact Simulation Interval for Multiprocessor Real-Time Systems Validation. In The Twelfth International Conference on Advances in System Testing and Validation Lifecycle (VALID 2020), Porto, Portugal, October 2020. [ bib ]
[12] Joumana Lagha, Jean-Luc Béchennec, Sébastien Faucou, and Olivier H. Roux. Safe Bound on simulation interval for real-time systems for two-phases task model. In 22nd IEEE Real Time Conference (RT2020), Virtual, October 2020. [ bib ]
[13] Didier Lime, Olivier H. Roux, and Charlotte Seidner. Parameter Synthesis for Bounded Cost Reachability in Time Petri Nets. In The 40th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2019), volume 11522 of Lecture Notes in Computer Science, Germany, June 2019. Springer. [ bib ]
[14] Jean-Luc Bechennec, Didier Lime, and Olivier H. Roux. Control of DES with urgency, avoidability and ineluctability. In 19th International Conference on Application of Concurrency to System Design (ACSD'19), Aachen, Germany, June 2019. IEEE. [ bib ]
[15] Yrvann Emzivat, Javier Ibanez Guzman, Philippe Martinet, and Olivier H. Roux. A formal approach for the design of a dependable perception system for autonomous vehicles. In IEEE 21th International Conference on Intelligent Transportation Systems (ITSC 2018), Hawai, USA, November 2018. [ bib ]
[16] Hanifa Boucheneb, Didier Lime, Olivier H. Roux, and Charlotte Seidner. Optimal-cost reachability analysis based on time Petri nets. In 18th International Conference on Application of Concurrency to System Design (ACSD'18), Bratislava, Slovakia, June 2018. [ bib ]
[17] Thomas Chatain, Maurice Comlan, David Delfieu, Loig Jezequel, and Olivier H. Roux. Pomsets and unfolding of reset Petri nets. In 12th International Conference on Language and Automata Theory and Applications (LATA 2018), volume 10792 of Lecture Notes in Computer Science. Springer, April 2018. [ bib ]
[18] Jean-Luc Bechennec, Olivier H. Roux, and Toussaint Tigori. Formal model-based conformance verification of an OSEK/VDX compliant RTOS. In International Conference on Control, Decision and Information Technologies (CODIT 2018), April 2018. [ bib ]
[19] Yrvann Emzivat, Javier Ibanez Guzman, Philippe Martinet, and Olivier H. Roux. Adaptability of an automated driving system facing inherent hazardous areas of the road network. In IEEE 20th International Conference on Intelligent Transportation Systems (ITSC 2017), Yokohama, JAPAN, October 2017. [ bib ]
[20] Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux. Coverability synthesis in parametric Petri nets. In Roland Meyer and Uwe Nestmann, editors, The 28th International Conference on Concurrency Theory (CONCUR 2017), LIPIcs, Berlin, Germany, September 2017. Dagstuhl Publishing. [ bib ]
[21] Hanifa Boucheneb, Didier Lime, Baptiste Parquier, Olivier H. Roux, and Charlotte Seidner. Optimal reachability in cost time Petri nets. In Uwe Nestmann and Katinka Wolter, editors, 15th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2017), volume 10419 of Lecture Notes in Computer Science, pages 58-73, Berlin, Germany, September 2017. Springer. [ bib ]
[22] Yrvann Emzivat, Javier Ibanez Guzman, Philippe Martinet, and Olivier H. Roux. Dynamic driving task fallback for an autonomous vehicle whose perception module has failed. In IEEE Intelligent Vehicles Symposium (IV 2017), Redondo Beach, USA, June 2017. [ bib ]
[23] Étienne André, Didier Lime, and Olivier H. Roux. Decision problems for parametric timed automata. In Kazuhiro Ogata, Mark Lawford, and Shaoying Liu, editors, 18th International Conference on Formal Engineering Methods (ICFEM 2016), volume 10009 of Lecture Notes in Computer Science, pages 400-416, Tokyo, Japan, November 2016. Springer. [ bib ]
[24] Baptiste Parquier, Laurent Rioux, Rafik Henia, Romain Soulat, Olivier H. Roux, Didier Lime, and Étienne André. Applying parametric model-checking techniques for reusing real-time critical systems. In Cyrille Artho and Peter Csaba Ölveczky, editors, 5th International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2016), Communications in Computer and Information Science, Tokyo, Japan, November 2016. Springer. [ bib ]
[25] Étienne André, Didier Lime, and Olivier H. Roux. On the expressiveness of parametric timed automata. In Martin Fränzle and Nicolas Markey, editors, 14th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2016), volume 9984 of Lecture Notes in Computer Science, pages 19-34, Québec City, Canada, August 2016. Springer. [ bib ]
[26] Yrvann Emzivat, Benoît Delahaye, Didier Lime, and Olivier H. Roux. Probabilistic Time Petri Nets. In Fabrice Kordon and Daniel Moldt, editors, The 37th International Conference on Application and Theory of Petri Nets and Concurrency (Petri Nets 2016), volume 9698 of Lecture Notes in Computer Science, pages 261-280, Toruń, Poland, June 2016. Springer. [ bib ]
[27] Louis-Marie Givel, Jean-Luc Béchennec, Matthias Brun, Sébastien Faucou, and Olivier H. Roux. Testing real-time embedded software using runtime enforcement. In 11th IEEE Symposium on Industrial Embedded Systems, SIES 2016, Krakow, Poland, May 23-25, 2016, pages 199-204, May 2016. [ bib ]
[28] Étienne André, Didier Lime, and Olivier H. Roux. Integer-complete synthesis for bounded parametric timed automata. In The 9th International Workshop on Reachability Problems, volume 9328 of Lecture Notes in Computer Science, pages 7-19, Warsaw, Poland, September 2015. Springer. [ bib ]
[29] Kabland Toussaint Gautier Tigori, Jean-Luc Bechennec, , and Olivier H. Roux. Formal synthesis of optimal RTOS. In The 12th IEEE international Conference on Embedded Software and Systems, New York, USA, August 2015. IEEE. [ bib ]
[30] Louis-Marie Givel, Matthias Brun, Camille Constant, Sebastien Faucou, and Olivier H. Roux. Use of runtime enforcement for the test of real-time systems. In The 12th IEEE international Conference on Embedded Software and Systems, New York, USA, August 2015. IEEE. [ bib ]
[31] Nicolas David, Claude Jard, Didier Lime, and Olivier H. Roux. Discrete parameters in Petri nets. In Raymond Devillers and Antti Valmari, editors, The 36th International Conference on Application and Theory of Petri Nets and Concurrency (ICATPN 2015), volume 9115 of Lecture Notes in Computer Science, pages 137-156, Brussels, Belgium, June 2015. Springer. [ bib ]
[32] Johan Girault, Jean-Jacques Loiseau, and Olivier H. Roux. On-line optimal compositional controller synthesis for agv by unfolding. In 5th international Workshop on Dependable Control of Discrete Systems (DCDS 2015), Cancun, Mexico, 2015. [ bib ]
[33] Julien Tanguy, Jean-Luc Béchennec, Mikaël Briday, and Olivier H. Roux. Reactive embedded device driver synthesis using logical timed models. In The 4th International Conference on Simulation and Modeling Methodologies, Technologies and Applications (SIMULTECH 2014), Vienna, Austria, August 2014. Scitepress Digital Library. [ bib ]
[34] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Synthesis of bounded integer parameters for parametric timed reachability games. In Hung Dang-Van and Mizuhito Ogawa, editors, The 11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013), volume 8172 of Lecture Notes in Computer Science, pages 87-101, Hanoi, Vietnam, October 2013. Springer. [ bib | .pdf ]
[35] Hanifa Boucheneb, Didier Lime, and Olivier H. Roux. On Multi-enabledness in Time Petri Nets. In José Manuel Colom and Jörg Desel, editors, The 34th International Conference on Application and Theory of Petri Nets and other models of concurrency (ICATPN 2013), volume 7927 of Lecture Notes in Computer Science, pages 130-149, Milano, Italy, June 2013. Springer. [ bib ]
[36] 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. Springer. (See extended version in IEEE TSE vol 41 issue 5, 2015). [ bib ]
[37] Cédrick Lelionnais, Matthias Brun, Jérôme Delatour, Olivier H. Roux, and Charlotte Seidner. Formal composition based on roles within a model driven engineering approach. In The 5th International Conference on Advances in System Testing and Validation Lifecycle (VALID 2013), Venice, Italy, 2013. [ bib ]
[38] Julien Tanguy, Jean-Luc Béchennec, Mikaël Briday, Olivier H. Roux, and Sébastien Dubé. Device driver synthesis for embedded systems. In The 18th IEEE International Conference on Emerging Technologies &Factory Automation (ETFA 2013), Cagliari, Italy, 2013. IEEE Computer Society. [ bib ]
[39] Aleksandra Jovanović, Sébastien Faucou, Didier Lime, and Olivier H. Roux. Real-Time Control with Parametric Timed Reachability Games. In 11th International Workshop on Discrete Event Systems (WODES'12), pages 323-330, Guadalajara, Mexico, October 2012. IFAC. [ bib | http ]
[40] Hanifa Boucheneb, Adrien Bullich, and Olivier H. Roux. FIFO Time Petri Nets for conflicts handling. In 11th International Workshop on Discrete Event Systems (WODES'12), pages 143-148, Guadalajara, Mexico, October 2012. IFAC. [ bib | http ]
[41] Claude Jard, Didier Lime, and Olivier H Roux. Clock Transition Systems. In 21th international Workshop on Concurrency, Specification and Programming (CS&P 2012), Berlin, Germany, September 2012. Bia University of Technology, ISBN 978-83-62582-42-6. [ bib ]
[42] S Akshay, Loïc Hélouët, Claude Jard, Didier Lime, and Olivier H. Roux. Robustness of Time Petri Nets under architectural constraints. In Marcin Jurdzinski and Dejan Nickovic, editors, 10th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2012), volume 7595 of Lecture Notes in Computer Science, pages 11-26, London, UK, September 2012. Springer. [ bib | www: ]
[43] Adrien Bullich, Hanifa Boucheneb, and Olivier H. Roux. Refinement of time Petri nets semantics in conflict situations. In The 9th International Conference on Cybernetics and Information Technologies, Systems and Applications: CITSA 2012, Orlando, USA, July 2012. [ bib ]
[44] Cedric Lelionnais, Matthias Brun, Jerome Delatour, Olivier H. Roux, and Charlotte Seidner. Formal behavioral modeling of real-time operating systems. In 14th Int. Conf. Ent. Information Systems - Model Driven Development for Information Systems (MDDIS 2012),, Wroclaw, Poland, June 2012. [ bib ]
[45] 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 ]
[46] 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 ]
[47] 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 ]
[48] 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 ]
[49] 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 ]
[50] 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 ]
[51] 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 ]
[52] 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 ]
[53] 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 ]
[54] 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 ]
[55] 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 ]
[56] 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 ]
[57] 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 ]
[58] 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 ]
[59] 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 ]
[60] 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, Jun 2007. [ bib ]
[61] 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 ]
[62] 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 ]
[63] 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 ]
[64] 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 ]
[65] 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 ]
[66] 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 ]
[67] 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 ]
[68] 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 ]
[69] 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 ]
[70] 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 ]
[71] 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 ]
[72] 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 ]
[73] 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 ]
[74] 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 ]
[75] 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 ]
[76] 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 ]
[77] 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 ]
[78] 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 ]
[79] 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] Jean-Luc Bechennec, Didier Lime, and Olivier H. Roux. Contrôle des SED avec urgence, évitabilité et inéluctabilité . In 12ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'19), Angers, France, November 2019. [ bib ]
[2] Toussaint Tigori, Jean-Luc Béchennec, and Olivier H. Roux. Approche formelle pour la spécialisation de systèmes d'exploitation temps réel. In 10ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'15), Nancy, France, November 2015. [ bib ]
[3] Johan Girault, Jean-Jacques Loiseau, and Olivier H. Roux. Synthèse en ligne de superviseur compositionnel pour flotte de robots mobiles. In 9ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'13), Rennes, France, November 2013. [ bib ]
[4] Didier Lime, Claude Martinez, and Olivier H. Roux. Coercition temporelle de réseaux de Petri. In 8ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs, (MSR'11), Lille, France, November 2011. [ bib ]
[5] 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 ]
[6] 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 ]
[7] 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 ]
[8] 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 ]
[9] 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 ]
[10] 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] Toussaint Tigori, Jean-Luc Béchennec, Sébastien Faucou, and Olivier H. Roux. Using formal methods for the development of safe application-specific rtos for automotive systems. In Critical Automotive applications : Robustness and Safety, CARS 2015, 2015. [ bib ]
[2] 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] Victor Khomenko, Jetty Kleijn, Wojciech Penczek, and Olivier H. Roux, editors. Application and Theory of Petri Nets and Concurrency - Special Issue, volume 169, number 1-2 of Fundamenta Informaticae. IOS Press, 2019. [ bib | DOI | http ]
[2] 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] Victor Khomenko and Olivier H. Roux, editors. 39th International Conference on Application and Theory of Petri Nets and Concurrency, PETRI NETS 2018, volume 10877 of Lecture Notes in Computer Science. Springer, 2018. [ bib ]
[2] 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 ]
[3] 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 ]
[4] 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 ]