Contact information

  • e-mail Herve.Marchand@inria.fr
  • Address INRIA, centre Rennes - Bretagne Atlantique

    Campus Universitaire de Beaulieu, 35042 Rennes cedex - France
  • 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

Since October 2009, I'm Associate Editor of the IEEE Transactions on Automatic Control, 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 de systèmes réactifs). I have served in the program committee of several conferences : IFAC World Congress'11, DCDS'11 (3rd International Workshop on Dependable Control of Discrete Systems) Vecos'08 (International Workshop on Verification and Evaluation of Computer and Communication Systems), ICINCO'07, ICINCO'08 ICINCO'09, INCINCO'10, INCINCO'11 (International Conference on Informatics in Control, Automation and Robotics), Wodes'06, Wodes'08, Wodes'10, Wodes 2012 (International Workshop on Discrete Event Systems), MSR'05, MSR'07, MSR'09, MSR'11 (Modélisation de systèmes réactifs) and SCODES'01 (symposium on the Supervisory Control of Discrete Event Systems 2001).

Some publications

can be found here sorted by category. The full list, sorted by type, is available here.

Background and Position

I received a Ph.D degree in computer science from "Université de Rennes 1" in 1997 under the supervision of Michel Le Borgne and Paul Le Guernic. 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.

Since 1998, I am an INRIA research scientist (Chargé de recherche) at INRIA, centre Rennes - Bretagne Atlantique. I am a member of the VerTeCs project.

Software

  • 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.

  • 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 Espresso and Vertecs. It is now also integrated in the compiler of the synchronous BZR language. (more details).