Olivier H. Roux

Maître de conférences (HDR) -- Assistant Professor

Address:

IRCCyN - UMR CNRS 6597
1, rue de la Noë
B.P. 92101
44321 Nantes Cedex 3
France

Tel: from abroad: +33 2 40 37 69 76 - from France: 02 40 37 69 76

Fax: from abroad: +33 2 40 37 69 30 - from France: 02 40 37 69 30

Email: no-spam.olivier-h.roux@irccyn.ec-nantes.fr (remove "no-spam.")

Not to be confused with Olivier (F.) Roux (also member of IRCCyN)

Teaching (IUT-GEII - University of Nantes)

Data transmission and processing
Electronics
C Programming
Micro-informatics and Automatisms

Research (IRCCyN)

My work concerns Time Petri Nets and some of their extensions used for the model-checking or the control of real-time systems.

- Expressiveness and decidability of Time Petri Nets

Expressiveness of Arc-Place-Transition Time Petri nets.
Comparison of the expressiveness of Timed Automata and Time Petri Nets wrt timed bisimulation and timed language acceptance.
Study of the decidability of problems on TPN (such as reachability, language inclusion, TCTL ...).

- Model-checking of Time Petri Nets

State space abstractions of Time Petri Nets based on state classes or zones.
TCTL model checking of Time Petri Nets (implemented in the tool Roméo)

- Control of Timed Systems

Control of Time Petri Nets.
Control of timed non-inteference.

- Stopwatch Petri nets

Study of the undecidability of the Reachability problem for Time Petri Nets with stopwatches (even if the net is bounded).
States Space Abstractions (semi algorithm)
Overapproximated States Space Abstractions

- Time Petri nets - discrete time semantics

Study of algorithms and data structures for efficient model-checking of Time Petri Nets and Time Petri Nets with inhibitor arcs (and hyperarcs) with a discrete time approach.

Contracts, projects and research groups

Contracts

Industrial contract : Sodius (2006-2009). Study of problems of simulation and model-checking of eFFBD via Time Petri Nets.
Industrial contract : Dassault Aviation (2005-2006). Starting from an AADL model of an avionics system (with timed constraints), the goal is to translate this model into Time Petri Net in order to extract a set of translation rules.

Projects

I am involved in

ANR DOTS (2007-2010): Distributed Open and Timed Systems. Research topics: Formal Verification, Embedded Systems, Model checking, Control and Non-interference. Partners : IRCCyN (Nantes), IRISA (Rennes), LaBRI (Bordeaux), LAMSADE (Paris), and LSV (Cachan).
ARC INRIA (TP)I (2010-2011): (Timed/Probabilistic) Interfaces. Research topics: complex embedded systems - components and interfaces. Partners: IRISA, Aalborg University, ITI Copenhagen et IRCCyN.
ACI CORTOS (2003-2006) : Control and Observation of Real-Time Open Systems. Research topics: Controller synthesis, Real-time systems, Timed automata, Verification of open systems and Observation. Partners : IRCCyN (Nantes), LSV (Cachan) and VERIMAG (Grenoble).
European project ITEA EAST-EEA (2001-2004). This automotive-project is funded by the European Union and consists of major European automotive manufacturers, first-tier suppliers and research departments.

CNRS research groups

Co-leader of GDR ASR program: High performence embedded systems.
Co-leader of inter GDR program: AFSEC (Formal approaches for communicating embedded systems).
GDR ARP program: STRQDS (Real Time Systems QoS).

Tool

These works on Petri Nets lead to implementations which are integrated in the Roméo software workshop (an experimental version for Linux, Mac OSX and Windows is available on the Roméo Web Site). Roméo consists of a graphic interface written in tcl/tk and a computation module written in C++. TA obtained are provided in the input format of Uppaal or Kronos.

Publications

Some Publications can be found here

Google scholar
DBLP

Upcoming & Past Events

Petri Nets 2010 - PC member
DOTS'10 - PC member
VECoS'10 - PC member
APNOC'10 - PC member
SUMo'10 - PC member
MSR'09 - PC chair and organizer
TiSto'09 - PC co-chair
APNOC'09 - PC member
ETR'09 - PC member
MSR'07 - PC member
ETR'07 - PC member and co-organizer