Contact information

  • e-mail Herve.Marchand@inria.fr
  • Address Centre Inria de l'Université de Rennes, Campus Universitaire de Beaulieu, 35042 Rennes cedex - France
  • Member of the LogicA team
  • Tel. +33 (0)2 99 84 75 09
  • Fax +33 (0)2 99 84 71 71

Research Topics

My currents interests are the control synthesis of discrete events systems. I am also interested in automatic test generation as well as in Diagnosis of discrete event systems. Within these areas, I concentrate on
  • the control of discrete event systems
    • control of Modular and hierarchical discrete event systems avoiding state space exploration
    • control under partial observation
    • Control within the synchronous paradigm and its application to the control of fault tolerant systems and multi-task systems
    • control of infinite systems using symbolic approximate techniques
  • the Model-Based Testing:
    • models and theory for conformance testing of reactive systems,
    • automated test case synthesis with enumerated or symbolic approximate techniques.
    • combination between verification and test
  • the diagnosis and prognosis (predictability) of Discrete Event Systems by means of Supervision Patterns
  • the security of information systems: security testing, diagnosis for intrusion detection and automatic synthesis of access-control.
  • model-checking, symbolic bisimulation, reduction model

Responsibilities

  • Steering Committees and Editorial Board. I'm member of the IFAC Technical Committees (TC 1.3 on Discrete Event and Hybrid Systems) since 2005 and member of the steering committee of MSR (Modélisation des Systhèmes Réactifs) since 2011. I became president of the Steering Committee of MSR in 2017. I was Associate Editor of the IEEE Transactions on Automatic Control between 2009 and 2013. Since January 2019, I'm associate editor of the journal Discrete Event Dynamic Systems: Theory and Applications

  • Member of the conference program committees. I have served in the program committee of several conferences : MSR'19: Modélisation des systèmes réeactifs Wodes'18: International Workshop on Discrete Event Systems, MSR'17, DCDS'15: workshop on dependable DES, Wodes'14, MSR'13, DCDS'13, Wodes 2012, MSR'11, IFAC World Congress'11, DCDS'11, INCINCO'11: International Conference on Informatics in Control, Automation and Robotics), Wodes'10, INCINCO'10, MSR'09, ICINCO'09, Wodes'08, Vecos'08: International Workshop on Verification and Evaluation of Computer and Communication Systems, ICINCO'08, MSR'07, ICINCO'07, Wodes'06, MSR'05, ACSD'05: International Conference on Application of Concurrency to system design, SCODES'01: Symposium on the Supervisory Control of Discrete Event Systems.

  • Conference Organisation. I co-organized with Loïc Hélouët MSR'13 in Rennes. I also co-organized ACSD'05 - Tool Demonstration (International Conference on Application of Concurrency to system design), St-Malo, France June 2005

Publications

The full list, sorted by type, is available here.

Background and Position

I received a PhD degree in computer science from "Université de Rennes 1" in 1997 under the supervision of Michel Le Borgne and Paul Le Guernic in the EP-ATR team. I spent one year as a Postdoctoral Associate in the Systems Science and Engineering Division of the Dept. of Electrical Engineering and Computer Science at the University of Michigan under the supervision of S. Lafortune.

Since 1998, I am an INRIA research scientist (Chargé de recherche) at INRIA, centre Rennes - Bretagne Atlantique. I was a member of the EP-ATR team between 1998 and 2000, member of the VerTeCs and Sumo teams between 2001 and 2022. Since January 2023, I am member of the Logica team.

I obtained my Habilitation from "Université de Rennes 1" in June 2017 (Document, Slides)

Software

  • Sigali : a Design Environment for Discrete-Event Controllers Synthesis.

    Sigali is a model-checking tool-based which manipulates ILTS: Implicit Labeled Transition Systems (which can be seen as an equational representation of an automaton) as intermediate models for discrete event systems. It offers functionalities for verification of reactive systems and discrete controller synthesis. It is developed jointly by Tea and Sumo. It is now also integrated in the compiler of the synchronous BZR/Heptagon language. (more details).

  • ReaX is a tool developed by N. Berthier and myself that investigates the control of safety properties for infinite reactive synchronous systems modeled by arithmetic symbolic transition systems (e.g., programs comprising Boolean, real or integer variables). By using abstract interpretation techniques involving disjunctive polyhedral over-approximations, we provide effective symbolic algorithms allowing to solve the deadlock-free safety control problem. As for SIGALI, this tool is connected with the BZR/Heptagon environment. ReaX is distributed under the terms of the GNU General Public License. It is implemented in Ocaml and is a fork of the ReaVer tool originally implemented by Peter Schrammel .

  • TAKOS: Toolbox for Analyzing the K-Opacity of Systems.
    TAKOS is a tool dedicated to the validation of several levels of opacity on systems.

    Opacity means the impossibility for an attacker to retrieve the value of a secret in a system of interest. Roughly speaking, ensuring opacity provides confidentiality of a secret on the system that must not leak to an attacker.
    Besides additional features, with TAKOS the user is able to:
    • to check offline (i.e. model-check) the opacity of a secret on a system,
    • to synthesize a runtime verification monitor in order to check the opacity at system runtime,
    • and to synthesize an enforcement monitor in order to ensure the opacity of a secret at system runtime.