[1] 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 ]
[2] 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), Lecture Notes in Computer Science, Berlin, Germany, September 2017. Springer. [ bib ]
[3] 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 ]
[4] É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 ]
[5] 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 ]
[6] É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 ]
[7] 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 ]
[8] 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 ]
[9] É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 ]
[10] 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 ]
[11] 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 ]
[12] 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 ]
[13] 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 ]
[14] 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 ]
[15] 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 ]
[16] 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 ]
[17] 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 ]
[18] 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 ]
[19] 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 ]
[20] 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 ]
[21] 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 ]
[22] 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 ]
[23] 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: ]
[24] 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 ]
[25] 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, 2012. [ bib ]
[26] 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 ]
[27] 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 ]
[28] 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 ]
[29] 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 ]
[30] 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 ]
[31] 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 ]
In this paper, we focus on the synthesis of secure timed systems which are given by timed automata. The security property that the system must satisfy is a non-interference property. Various notions of non-interference have been defined in the literature, and in this paper we focus on Strong Non-deterministic Non-Interference (SNNI) and we study the two following problems: (1) check whether it is possible to enforce a system to be SNNI; if yes (2) compute a sub-system which is SNNI.

[32] 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 ]
[33] 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 ]
[34] 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 ]
[35] 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 ]
[36] 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 ]
[37] 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 ]
[38] 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 ]
[39] 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 ]
In this paper, we focus on distributed systems sub ject to security issues. Such systems are usually composed of two entities: a high level user and a low level user that can both do some actions. The security properties we consider are non-interference properties. A system is non-interferent if the low level user cannot deduce any information by playing its low level actions. Various notions of non-interference have been defined in the literature, and in this paper we focus on two of them: one trace-based property (SNNI) and another bisimulation-based property (BSNNI). For these properties we study the problems of synthesis of a high level user so that the system is non-interferent. We prove that a most permissive high level user can be computed when one exists.

[40] 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 ]
[41] 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 ]
[42] 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 ]
We study some control synthesis problems on an extension of Time Petri Nets that model a plant and its environment. The Time Petri Net control model both represents controllable and uncontrollable events, the problem is then to design a function (controller) such that a given property is fulfilled. We focus our analysis on safety properties expressed on the markings of the net and we propose a symbolic method to decide the existence of a controller that ensures these properties. Unlike existing methods on Time Petri Nets, that assume the net is bounded, the method is applicable for any Time Petri Nets. A consequence is that it is possible to decide the existence of a controller that k-bounds the plant. A method is then proposed to build a state-based controller and problems raised by the implementation (Zenoness, sampling) of the control function on the plant are discussed.

[43] 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 ]
[44] 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 ]
[45] 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 ]
[46] 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 ]
[47] 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 ]
[48] 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 ]
[49] 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 ]
[50] 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 ]
[51] 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 ]
[52] 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 ]
[53] 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 ]
In this paper, we propose a method for building the state class graph of a bounded time Petri net (TPN) as a timed automaton (TA). We consider bounded TPN, whose underlying net is not necessarily bounded. We prove that the obtained TA is timed-bisimilar to the initial TPN. The number of clocks of the automaton is much lower than with other methods available. It allows us to check real-time properties on bounded TPN with efficient TA model-checkers. We have implemented the method, and give some experimental results in this paper, illustrating the efficiency of the algorithm in terms of clock number.

[54] 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 ]
The theory of Petri Nets provides a general framework to specify the behaviour of real-time systems and time extensions have been introduced to take also temporal specifications into account. The main method to compute the state space of a Time Petri Net has been introduced by Berthomieu and Diaz. It is known as the “state class method”. We present in this paper a new efficient method to compute the state space of a bounded Time Petri Net as a marking graph, based on the region graph method used for Timed Automaton. Although some limitations induced by Difference Bounded Matrices (DBM) have been recently discovered by Bouyer in computing the state space of a Timed Automaton (overapproximation), we successfully used DBM in our method. The algorithm is proved to be exact with respect to the reachability of a marking and it computes a graph which nodes are exactly the reachable markings of the Time Petri Net. The tool implemented computes faster than Tina, a tool for computing the state space using classes, and allows to test on-the-fly the reachability of a given marking.

[55] 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 ]
[56] 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 ]
The most widely used approach for verifying the schedulability of a real-time system consists of using analytical methods. However, for complex systems with interdependent tasks and variable execution times, they are not well adapted. For those systems, an alternative approach is the formal modelisation of the system and the use of model-checking, which also allows the verification of more varied scheduling properties. In this paper, we show how an extension of time Petri nets : scheduling extended time Petri nets (SETPN), is especially well adapted for the modelisation of real-time systems and particularly embedded systems and we provide a method for computing the state space of SETPN. We first propose an exact computation using a general polyhedron representation of time constraints, then we propose an overapproximatiion of the polyhedra to allow the use of much more efficient data structures, DBMs. We finally describe a particular type of observers, that gives us a numeric result (instead of boolean) for the computation of tasks response times.

[57] 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 ]
[58] 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 ]
[59] 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 ]
[60] 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 ]