HUAWEI Technologies France SASU (2020-2023) : Formal methods for the synthesis of multi-core embedded real-time OS.
Renault (2015-2018) : Design and Validation for cross-system for autonomous cars.
BA Systemes (2012-2015): Real Time Control of AGV (Automated Guided Vehicle).
SeeForSys (2011-2014): Formal modeling and synthesis of drivers for embedded systems.
Sodius (2006-2009): Study of problems of simulation and model-checking of eFFBD via Time Petri Nets.
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
ANR PRC BisoUS
(2023-2026):Better Synthesis for Underspecified quantitative Systems (BisoUS) : LS2N (Nantes), IRISA (Rennes), LMF (Paris-Saclay) et LIPN (Paris 13).
ANR PRCI (France-Singapor) ProMiS (2020-2024): Provable Mitigation of Side Channel through Parametric Verification (ProMiS) : LORIA (Nancy), LS2N (Nantes), SMU (Singapor) and SUTD (Singapor).
CominLabs Project EPOC (2013-2016) : Energy proportional and opportunistic Computing systems), aims at focusing on energy-aware task execution from the hardware to application's components in the context of a mono-site data center (all resources are in the same physical location) which is connected to the regular electric Grid and to renewable energy sources (such as windmills or solar cells). Partners : LINA (Nantes), IRCCyN (Nantes), Telecom-Bretagne, Lab-STICC (Brest).
FUI FREENIVI (2013-2017): Open Source Software for Embedded Systems dedicated to automotive. Partners : OPEN WIDE, ESG Automotive, IRT SystemX, IRCCyN (Ecole Centrale Nantes), LIAFA (Paris Diderot).
Paris scientifiques régionaux AFSEC PDL (2013-2017) : Approche Formelle des Systèmes Embarqués Communicants en Pays de la Loire. Partners : LINA, IRCCyN.
ANR IMPRO (2011-2014): Implementability and Robustness of Timed Systems. Partners : IRCCyN (Nantes), IRISA (Rennes), LIP6 (Paris), LSV (Cachan), LIAFA (Paris) and LIF (Marseille).
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.
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.