[1] Toussaint Tigori, Jean-Luc Bechennec, Sebastien Faucou, and Olivier H. Roux. Formal model-based synthesis of application specific static RTOS. ACM Transactions on Embedded Computing Systems, 16(4), 2017. [ bib | http ]
[2] 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 | http ]
[3] 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 | http | .pdf ]
[4] 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 | http | .pdf ]
[5] 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 ]
[6] 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 ]
[7] 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 ]
[8] 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 ]
[9] 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 ]
[10] 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 ]
[11] 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 ]
[12] 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 ]
In this paper, we consider subscript TCTL for Time Petri Nets (TPN-TCTL) for which temporal operators are extended with a time interval, specifying a time constraint on the firing sequences. We prove that the model-checking of a TPN-TCTL formula on a bounded TPN is decidable and is a PSPACE-complete problem. We propose a zone based state space abstraction that preserves marking reachability and traces of the TPN. As for Timed Automata (TA), the abstraction may use an over-approximation operator on zones to enforce the termination. A coarser (and efficient) abstraction is then provided and proved exact w.r.t. marking reachability and traces (LTL properties). Finally, we consider a subset of TPN-TCTL properties for which it is possible to propose efficient on-the-fly model-checking algorithms. Our approach consists in computing and exploring the zone based state space abstraction.

[13] 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 ]
At the border between control and verification, parametric verification can be used to synthesize constraints on the parameters to ensure that a system verifies given specifications. In this paper we propose a new framework for the parametric verification of time Petri nets with stopwatches. We first introduce a parametric extension of time Petri nets with inhibitor arcs (ITPNs) with temporal parameters and we define a symbolic representation of the parametric state-space based on the classical state-class graph method. Then, we propose semi-algorithms for the parametric modelchecking of a subset of parametric TCTL formulae on ITPNs. These results have been implemented in the tool Romeo and we illustrate them in a case-study based on a scheduling problem.

[14] 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 ]
[15] 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 ]
[16] 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 ]
In this paper, we propose a method for the verification of timed properties for real-time systems featuring a preemptive scheduling policy: the system, modeled as a scheduling time Petri net, is first translated into a linear hybrid automaton to which it is time-bisimilar. Timed properties can then be verified using . The efficiency of this approach leans on two major points: first, the translation features a minimization of the number of variables (clocks) of the resulting automaton, which is a critical parameter for the efficiency of the ensuing verification. Second, the translation is performed by an over-approximating algorithm, which is based on Difference Bound Matrix and therefore efficient, that nonetheless produces a time-bisimilar automaton despite the over-approximation. The proposed modeling and verification method are generic enough to account for many scheduling policies. In this paper, we specifically show how to deal with Fixed Priority and Earliest Deadline First policies, with the possibility of using Round-Robin for tasks with the same priority. We have implemented the method and give some experimental results illustrating its efficiency.

[17] 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 ]
Safety analysis in Systems Engineering (SE) processes, as usually implemented, rarely relies on formal methods such as model checking since such techniques, however powerful and mature, are deemed too complex for efficient use. This paper thus aims at improving the verification practice in SE design: considering the widely-used model of EFFBDs (Enhanced Function Flow Block Diagrams), it formally establishes its syntax and behavioral semantics. It also proposes a structural translation of EFFBDs to transition time Petri nets (TPNs); this translation is then proved to preserve the behavioral semantics (i.e. timed bisimilarity). After proving results on the boundedness of the resulting TPNs, it was possible to extend a number of fundamental properties (such as the decidability of liveness, state-access, etc.) from bounded TPNs to so-called bounded EFFBDs. Finally, these results led to implement and integrate an operational formal verification tool within a development platform, used in systems design for defense applications, where the underlying complexity is totally concealed from the end-user.

[18] 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 ]
In this paper, we consider safe Time Petri Nets where time intervals (strict and large) are associated with places (TPPN), arcs (TAPN) or transitions (TTPN). We give the formal strong and weak semantics of these models in terms of Timed Transition Systems. We compare the expressiveness of the six models w.r.t. (weak) timed bisimilarity (behavioral semantics). The main results of the paper are : (i) with strong semantics, TAPN is strictly more expressive than TPPN and TTPN ; (ii) with strong semantics TPPN and TTPN are incomparable ; (iii) TTPN with strong semantics and TTPN with weak semantics are incomparable. Moreover, we give a complete classification by a set of 9 relations explained in a figure.

[19] 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 ]
[20] 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 ]
Several extensions of Time Petri nets (TPNs) have been proposed for modeling suspension and resumption of actions in timed systems. We first introduce a simple class of TPNs extended with stopwatches (SwTPNs), and present a semi-algorithm for building exact representations of the behavior of SwTPNs. Then, we prove that state reachability in SwTPNs and all similar models is undecidable, even when bounded, which solves an open problem. Finally, we discuss overapproximation methods yielding finite abstractions of their behavior for a subclass of bounded SwTPNs, and propose a new one based on a quantization of the polyhedra representing temporal information. By, adjusting a parameter, the exact behavior can be approximated as closely as desired.

[21] 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 ]
[22] 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 ]
[23] 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 ]
We present in this paper a forward zone-based algorithm to compute the state space of a bounded Time Petri Net: the method is different and more efficient than the classical State Class Graph. We prove the algorithm to be exact with respect to the reachability problem. Furthermore, we propose a translation of the computed state space into a Timed Automaton, proved to be timed bisimilar to the original Time Petri Net.

[24] 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 ]
In order to analyze whether timing requirements of a real-time application are met, we propose an extension of the T-time Petri net model which takes into account the scheduling of the software tasks distributed over a multi-processor hardware architecture. The paper is concerned with static priority pre-emptive based scheduling. This extension consists in mapping into the Petri net model the way the different schedulers of the system activate or suspend the tasks. This relies on the introduction of two new attributes for the places (allocation and priority). First we give the formal semantics of this extended model as a timed transition system (TTS). Then we propose a method for its analysis consisting in the computation of the state class graph. Thus the verification of timing properties can be conducted (possibly together with an observator) and comes to analyze the such obtained state class graph.

[25] 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 ]