Recent Publications

• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Symbolic Supervisory Control of Infinite Transition Systems under Partial Observation using Abstract Interpretation. Discrete Event Dynamic Systems : Theory and Applications, (To appear), 2012. (Abstract | Bibtex )
  We propose algorithms for the synthesis of state-feedback controllers with partial observation of infinite state discrete event systems modelled by Symbolic Transition Systems. We provide models of safe memoryless controllers both for potentially deadlocking and deadlock free controlled systems. The termination of the algorithms solving these problems is ensured using abstract interpretation techniques which provide an overapproximation of the transitions to disable. We then extend our algorithms to controllers with memory and to online controllers. We also propose improvements in the synthesis of controllers in the finite case which, to our knowledge, provide more permissive solutions than what was previously proposed in the literature. Our tool SMACS gives an empirical validation of our methods by showing their feasibility, usability and efficiency
  @article{deds11a,
      Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
      Title = {Symbolic Supervisory Control of Infinite Transition Systems under Partial Observation using Abstract Interpretation},
      Journal = {Discrete Event Dynamic Systems : Theory and Applications},
      Year = {2011}
  }
• F. Cassez, J. Dubreil, H. Marchand. Synthesis of Opaque Systems with Static and Dynamic Masks. Formal Methods in System Design, 2012. (Abstract | Bibtex )
  Opacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask
  @article{FMSD12,
  Author = {Cassez, F. and Dubreil, J. and Marchand, H.},
  Title = {Synthesis of Opaque Systems with Static and Dynamic Masks},
  Journal = {Formal Methods in System Design},
  Year = {2012}
  }
• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Synthesis of Communicating Controllers for Distributed Systems. In 50th IEEE Conference on Decision and Control and European Control Conference, Pages 1803-1810, Orlando, USA, December 2011. (Abstract | Bibtex )
  We consider the control of distributed systems composed of subsystems communicating asynchronously; the aim is to build local controllers that restrict the behavior of a distributed system in order to satisfy a global state avoidance property. We model our distributed systems as communicating finite state machines with reliable unbounded FIFO queues between subsystems. The local controllers can only observe the behavior of their proper local subsystem and do not see the queue contents. To refine their control policy, they can use the FIFO queues to communicate by piggybacking extra information to the messages sent by the subsystems. We define synthesis algorithms allowing to compute the local controllers. We explain how we can ensure the termination of this control algorithm by using abstract interpretation techniques, to overapproximate queue contents by regular languages. An implementation of our algorithms provides an empirical evaluation of our method
  @InProceedings{CDC2011,
  Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
  Title = {Synthesis of Communicating Controllers for Distributed Systems},
  BookTitle = {50th IEEE Conference on Decision and Control and European Control Conference},
  Pages = {1803--1810},
  Address = {Orlando, USA},
  Month = {December},
  Year = {2011}
  }
• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Decentralized Control of Infinite Systems. Discrete Event Dynamic Systems : Theory and Applications, 21(3):359-393, September 2011. (Abstract | Bibtex )
  We propose algorithms for the synthesis of decentralized state-feedback controllers with partial observation of infinite state systems, which are modeled by Symbolic Transition Systems. We first consider the computation of safe controllers ensuring the avoidance of a set of forbidden states and then extend this result to the deadlock free case. The termination of the algorithms solving these problems is ensured by the use of abstract interpretation techniques, but at the price of overapproximations, in particular, in the computation of the states which must be avoided. We then extend our algorithms to the case where the system to be controlled is given by a collection of subsystems (modules). This structure is exploited to locally compute a controller for each module. Our tool SMACS gives an empirical evaluation of our methods by showing their feasibility, usability and efficiency.
  @article{deds112,
      Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
      Title = {Decentralized Control of Infinite Systems},
      Journal = {Discrete Event Dynamic Systems : Theory and Applications},
      Year = {2011}
  }, Volume = {21},
  Number = {3}
  pages = {359-393}
  Month = {September}
  
• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Global State Estimates for Distributed Systems. In 31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems, FORTE, Reykjavik, Iceland, June 2011. (Abstract | Bibtex )
  We consider distributed systems modeled as communicating finite state machines with reliable unbounded FIFO channels. As an essential sub-routine for control, monitoring and diagnosis applications, we provide an algorithm that computes, during the execution of the system, an estimate of the current global state of the distributed system for each local subsystem. This algorithm does not change the behavior of the system; each subsystem only computes and records a symbolic representation of the state estimates, and piggybacks some extra information to the messages sent to the other subsystems in order to refine their estimates. Our algorithm relies on the computation of reachable states. Since the reachability problem is undecidable in our model, we use abstract interpretation techniques to obtain regular overapproximations of the possible FIFO channel contents, and hence of the possible current global states. An implementation of this algorithm provides an empirical evaluation of our method.
  @InProceedings{forte2011,
      Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
      Title = {Global State Estimates for Distributed Systems},
      BookTitle = {31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems, FORTE},
      Address = {Reykjavik, Iceland},
      Month = {June},
      Year = {2011}
  }
• W. L. Andrade, P. Machado, T. Jéron, H. Marchand. Abstracting Time and Data for Conformance Testing of Real-Time Systems. In 7th Workshop on Advances in Model Based Testing A-MOST 2011, Berlin, Germany, March 2011. (Abstract | Bibtex )
  Current approaches to model-based conformance testing of real-time systems are mostly based either on finite state machines/transition systems or on timed automata. However, most real-time systems manipulate data while being subject to time constraints. The usual solution consists in enumerating data values (in finite domains) while treating time symbolically, thus leading to the classical state explosion problem. This paper proposes a new model of real-time systems as an extension of both symbolic transition systems and timed automata, in order to handle both data and time requirements symbolically. We then adapt the tioco conformance testing theory to deal with this model and describe a test case generation process based on a combination of symbolic execution and constraint solving for the data part and symbolic analysis for timed aspects.x
  @InProceedings{amost,
      Author = {L. Andrade, W. and Machado, P. and Jéron, T. and Marchand, H.},
      Title = {Abstracting Time and Data for Conformance Testing of Real-Time Systems},
      BookTitle = {7th Workshop on Advances in Model Based Testing A-MOST 2011},
      Address = {Berlin, Germany},
      Month = {March},
      Year = {2011}
  }
• Y. Falcone, Fernandez J.-C, T. Jéron, H. Marchand, L. Mounier. More Testable Properties. In 22nd IFIP International Conference on Testing Software and Systems, Natal, Lecture note in Computer Science, Volume 6435, Pages 30-46, Brazil, November 2010. (Abstract | Bibtex ) (Best paper award)
  In this paper, we explore the set of testable properties within the Safety-Progress classification where testability means to establish by testing that a relation, between the tested system and the property under scrutiny, holds. We characterize testable properties wrt. several relations of interest. For each relation, we give a sufficient condition for a property to be testable. Then, we study and delineate, for each Safety-Progress class, the subset of testable properties and their corresponding test oracle producing verdicts for the possible test executions. Furthermore, we address automatic test generation for the proposed framework. Finally, we present a tool implementing the results proposed by this paper
  @InProceedings{ictss-b,
      Author = {Falcone, Y. and J.-C, Fernandez and Jéron, T. and Marchand, H. and Mounier, L.},
      Title = {More Testable Properties},
      BookTitle = {22nd IFIP International Conference on Testing Software and Systems},
      Address = {Natal, Brazil},
      Month = {November},
      Year = {2010}
  }
• Y. Falcone, H. Marchand. Various Notions of Opacity Verified and Enforced at Runtime. Research Report INRIA, No 7349, August 2010. (Abstract| Bibtex )
  In this paper, we are interested in the validation of opacity where 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. More specifically, we study how we can verify and enforce, at system runtime, several levels of opacity. Besides already considered notions of opacity, we also introduce a new one that provides a stronger level of confidentiality
  @TechReport{k-opacity,
      Author = {Falcone, Y. and Marchand, H.},
      Title = {Various Notions of Opacity Verified and Enforced at Runtime},
      Number = {7349},
      Institution = {INRIA},
      Month = {August},
      Year = {2010}
  }
  

• Ph. Darondeau, J. Dubreil, H. Marchand. Supervisory Control for Modal Specifications of Services. Workshop on Discrete Event Systems, WODES'10, Pages 428-435, Berlin, Germany, August 2010. (Abstract| Bibtex )
  In the service oriented architecture framework, a modal specification, as defined by Larsen in \cite{Lar89}, formalises how a service should interact with its environment. More precisely, a modal specification determines the events that the server may or must allow at each stage in an interactive session. Therefore, techniques to enforce a modal specification on a system would be useful for practical applications. In this paper, we investigate the adaptation of the supervisory control theory of Ramadge and Wonham to enforce a modal specification (with final states marking the ends of the sessions) on a system modelled by a finite LTS. We prove that there exists at most one most permissive solution to this control problem. We also prove that this solution is regular and we present an algorithm for the effective computation of the corresponding controller.
  @InProceedings{wodes10-a,
      Author = {Darondeau, Ph. and Dubreil, J. and Marchand, H.},
      Title = {Supervisory Control for Modal Specifications of Services},
      BookTitle = {Workshop on Discrete Event Systems, WODES'10},
      Pages = {428-435},
      Address = {Berlin, Germany},
      Month = {August},
      Year = {2010}
  }
  
• E. Dumitrescu, A. Girault, H. Marchand, E. Rutten. Multicriteria optimal discrete controller synthesis for fault-tolerant real-time tasks. Workshop on Discrete Event Systems, WODES'10, Pages 366-373, Berlin, Germany, August 2010. (Abstract | Bibtex )
  We propose a technique for discrete controller synthesis, with optimal synthesis on bounded paths, in order to model, design, and optimize fault-tolerant distributed systems, taking into account several criteria (e.g., the execution costs of the tasks and their quality of service). Different combinations are explored for multi-criteria optimization
  @InProceedings{wodes10-b,
      Author = {Dumitrescu, E. and Girault, A. and Marchand, H. and Rutten, E.},
      Pages = {366-373},
      Title = {Multicriteria optimal discrete controller synthesis for fault-tolerant real-time tasks},
      BookTitle = {Workshop on Discrete Event Systems, WODES'10},
      Address = {Berlin, Germany},
      Month = {August},
      Year = {2010}
  }
• O. Landry Nguena, H. Marchand, A. Rollet. Automatic Test Generation for Data-Flow Reactive Systems with time constraints (Short paper). In 22nd IFIP International Conference on Testing Software and Systems, Natal, Brazil, November 2010. (Abstract | Bibtex )
  In this paper, we handle the problem of conformance testing for data-flow critical systems with time constraints. We present a formal model (Variable Driven Timed automata) adapted for such systems inspired from timed automata using variables as inputs and outputs, and clocks. In this model, we consider urgency and the possibility to fire several transitions instantaneously. We present a conformance relation for this model and we propose a test generation method using a test purpose approach, based on a region graph transformation of the specification
  @InProceedings{ictss-b,
      Author = {Landry Nguena, O. and Marchand, H. and Rollet, A.},
      Title = {Automatic Test Generation for Data-Flow Reactive Systems with time constraints (Short paper)},
      BookTitle = {22nd IFIP International Conference on Testing Software and Systems},
      Address = {Natal, Brazil},
      Month = {November},
      Year = {2010}
  }
• G. Delaval, H. Marchand and E. Rutten, Contracts for Modular Discrete Controller Synthesis Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2010, Pages 57-66, Stockholm, Sweden April 12-16, 2010. ( Abstract | Bibtex )
  We describe the extension of a reactive programming language with a behavioral contract construct. It is dedicated to the pro- gramming of reactive control of applications in embedded sys- tems, and involves principles of the supervisory control of discrete event systems. Our contribution is in a language approach where modular discrete controller synthesis (DCS) is integrated, and it is concretized in the encapsulation of DCS into a compilation pro- cess. From transition system specifications of possible behaviors, DCS automatically produces controllers that make the controlled system satisfy the property given as objective. Our language fea- tures and compiling technique provide correctness-by-construction in that sense, and enhance reliability and verifiability. Our appli- cation domain is adaptive and reconfigurable systems: closed-loop adaptation mechanisms enable flexible execution of functionalities w.r.t. changing resource and environment conditions. Our language can serve programming such adaption controllers. This paper par- ticularly describes the compilation of the language. We present a method for the modular application of discrete controller synthesis on synchronous programs, and its integration in the BZR language. We consider structured programs, as a composition of nodes, and first apply DCS on particular nodes of the program, in order to re- duce the complexity of the controller computation; then, we allow the abstraction of parts of the program for this computation; and finally, we show how to recompose the different controllers com- puted from different abstractions for their correct co-execution with the initial program. Our work is illustrated with examples, and we present quantitative results about its implementation
  @InProceedings{delaval10a,
      Author = {Delaval, G. and Marchand, H. and Rutten, E.},
      Title = {Contracts for Modular Discrete Controller Synthesis},
      BookTitle = {Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2010},
      Pages = {57--66},
      Address = {Stockholm, Sweden},
      Month = {April},
      Year = {2010}
  }
• J. Dubreil, Ph. Darondeau, H. Marchand, Supervisory Control for Opacity, IEEE Transactions on Automatic Control, Vol 55(5):1089-1100, May 2010. (Abstract | Bibtex)
  In the field of computer security, a problem that received little attention so far is the enforcement of confidentiality properties by supervisory control. Given a critical system G that may leak confidential information, the problem consists in designing a controller C, possibly disabling occurrences of a fixed subset of events of G, so that the closed-loop system G/C does not leak confidential information. We consider this problem in the case where G is a finite transition system with set of events A and an inquisitive user, called the adversary, observes a subset Aa of A. The confidential information is the fact (when it is true) that the trace of the execution of G on A* belongs to a regular set S in A, called the secret. The secret S is said to be opaque w.r.t. G (resp. G/C) and Aa if the adversary cannot safely infer this fact from the trace of the execution of G (resp. G/C) on Aa*. In the converse case, the secret can be disclosed. We present an effective algorithm for computing the most permissive controller C such that S is opaque w.r.t. G/C and Aa. This algorithm subsumes two earlier algorithms working under the strong assumption that the alphabet Aa of the adversary and the set of events that the controller can disable are comparable.
  @article{dubreil09b,
     Author = {Dubreil, J. and Darondeau, Ph. and Marchand, H.},
     Title = {Supervisory Control for Opacity},
     Journal = {IEEE Transactions on Automatic Control},
     Volume = {55},
     Number = {5},
     Pages = {1089-1100},
     Year = {2010}
  }
  
• E. Rutten, H. Marchand, Automatic Generation of Safe Handlers for Multi-Task Systems, Journal of Embedded Computing, 3(4):255-276, 2009. (Abstract | Bibtex )
  We are interested in the programming of real-time control systems, such as in robotic, automotive or avionic systems. They are designed with multiple tasks, each with multiple modes. It is complex to design task handlers that control the switching of activities in order to insure safety properties of the global system. We propose a model of tasks in terms of transition systems, designed especially with the purpose of applying existing discrete controller synthesis techniques. This provides us with a systematic methodology, for the automatic generation of safe task handlers, with the support of synchronous languages and associated tools for compilation and formal computation.
  @article{rutten09,
      Author = {Rutten, Eric and Marchand, Hervé},
      Title = {Automatic generation of safe handlers for multi-task systems},
      Journal = {Journal of Embedded Computing},
      Volume = {3},
      Number = {4},
      Pages = {255--276},
      Year = {2009}
  }
  

• H. Marchand, J. Dubreil, T. Jéron, Automatic Testing of Access Control for Security Properties, in TestCom'09/FATES'09, LNCS Volume 5826, Pages 113-128, Eindhoven, November 2009. (Abstract | Bibtex)
  In this work, we investigate the combination of controller synthesis and test generation techniques for the testing of open, partially observable systems with respect to security policies. We consider two kinds of properties: integrity properties and confidentiality properties. We assume that the behavior of the system is modeled by a labeled transition system and assume the existence of a black-box implementation. We first outline a method allowing to automatically compute an ideal access control ensuring these two kinds of properties. Then, we show how to derive testers that test the conformance of the implementation with respect to its specification, the correctness of the real access control that has been composed with the implementation in order to ensure a security property, and the security property itself.
  @InProceedings{testcom09,
     Author = {Marchand, H. and Dubreil, J. and Jéron, T.},
     Title = {Automatic Testing of Access Control for Security Properties},
     BookTitle = {TestCom'09},
     Volume = {5826},
     Pages = {113--128},
     Series = {LNCS},
     Publisher = {Springer-Verlag},
     Month = {November},
     Year = {2009}
  }
• J. Dubreil, T. Jéron, H. Marchand, Monitoring Confidentiality by Diagnosis Techniques, in European Control Conference, Pages 2584--2590, Budapest, Hungary, August 2009. (Abstract | Bibtex)
  In this paper, we are interested in constructing monitors for the detection of confidential information flow in the context of partially observable discrete event systems. We focus on the case where the secret information is given as a regular language. We first characterize the set of observations allowing an attacker to infer the secret behaviors. We consider the general case where the attacker and the administrator have different partial views of the system. Further, based on the diagnosis of discrete event systems, we provide necessary and sufficient conditions under which detection and prediction of secret information flow can be ensured and a construction of a monitor ensuring this task.
  @InProceedings{dubreil09a,
     Author = {Dubreil, J. and Jéron, T. and Marchand, H.},
     Title = {Monitoring Confidentiality by Diagnosis Techniques},
     BookTitle = {European Control Conference},
     Pages = {2584--2590},
     Address = {Budapest, Hungary},
     Month = {August},
     Year = {2009}
  }
• J. Dubreil, Ph. Darondeau, H. Marchand, Opacity Enforcing Control Synthesis, in Workshop on Discrete Event Systems, WODES'08, Pages 28-35, Gothenburg, Sweden, March 2008. (Abstract | Bibtex)
  Given a finite transition system and a regular predicate, we address the problem of computing a controller enforcing the opacity of the predicate against an attacker (who partially observes the system), supposedly trying to push the system to reveal the predicate. Assuming that the controller can only control a subset of the events it observes (possibly different from the ones of the attacker), we show that an optimal control always exists and provide sufficient conditions under which it is regular and effectively computable. These conditions rely on the inclusion relationships between the controllable alphabet and the observable alphabets of the attacker and of the controller.
  @InProceedings{opacity2,
     Author = {Dubreil, J. and Darondeau, Ph. and Marchand, H.},
     Title = {Opacity Enforcing Control Synthesis},
     BookTitle = {Workshop on Discrete Event Systems, WODES'08},
     Pages = {28--35},
     Address = {Gothenburg, Sweden},
     Month = {March},
     Year = {2008}
  }
• J. Komenda, J. van Schuppen, B. Gaudin, H. Marchand, Supervisory Control of Modular Systems with Global Specification Languages, Automatica, 44:1127-1134, 2008. (Abstract | Bibtex)
  The paper presents sufficient conditions for modular (supervisory) control synthesis to equal global control synthesis. In modular control synthesis a supervisory control is synthesized for each module separately and the supervisory control consists of the parallel composition of the modular supervisory controls. The general case of the specification that is indecomposable and not necessarily contained in the plant language, which is often the case in practice, is considered. The usual assumption that all shared events are controllable is relaxed by introducing two new structural conditions relying on the global mutual controllability condition. The novel concept used as a sufficient structural condition is strong global mutual controllability. The main result uses a weaker condition called global mutual controllability together with local consistency of the specification. An example illustrates the approach.
  @article{komenda-automatica,
     Author = {Komenda, J. and van Schuppen, J. and Gaudin, B. and Marchand, H.},
     Title = {Supervisory Control of Modular Systems with Global Specification Languages},
     Journal = {Automatica},
     Volume = {    44},
     Number = {4},
     Pages = {1127--1134},
     Month = {April},
     Year = {2008}
  }
  

• C. Constant, T. Jéron, H. Marchand, V. Rusu, Integrating formal verification and conformance testing for reactive systems, IEEE Transactions on Software Engineering, 33(8):558-574, August 2007. (Abstract | Bibtex)
  In this paper, we describe a methodology integrating verification and conformance testing. A specification of a system- an extended input-output automaton, which may be infinite-state-and a set of safety properties ("nothing bad ever happens") and possibility properties ("something good may happen") are assumed. The properties are first tentatively verified on the specification using automatic techniques based on approximated state-space exploration, which are sound, but, as a price to pay for automation, are not complete for the given class of properties. Because of this incompleteness and of state-space explosion, the verification may not succeed in proving or disproving the properties. However, even if verification did not succeed, the testing phase can proceed and provide useful information about the implementation. Test cases are automatically and symbolically generated from the specification and the properties and are executed on a black-box implementation of the system. The test execution may detect violations of conformance between implementation and specification; in addition, it may detect violation/satisfaction of the properties by the implementation and by the specification. In this sense, testing completes verification. The approach is illustrated on simple examples and on a Bounded Retransmission Protocol.
  @article{ieee-tse,
     Author = {Constant, C. and Jéron, T. and Marchand, H. and Rusu, V.},
     Title = {Integrating formal verification and conformance testing for reactive systems},
     Journal = {IEEE Transactions on Software Engineering},
     Volume = {    33},
     Number = {8},
     Pages = {558--574},
     Month = {August},
     Year = {2007}
  }
  

Automatic Test Generation

• W. L. Andrade, P. Machado, T. Jéron, H. Marchand. Abstracting Time and Data for Conformance Testing of Real-Time Systems. In 7th Workshop on Advances in Model Based Testing A-MOST 2011, Berlin, Germany, March 2011. (Abstract | Bibtex )
  Current approaches to model-based conformance testing of real-time systems are mostly based either on finite state machines/transition systems or on timed automata. However, most real-time systems manipulate data while being subject to time constraints. The usual solution consists in enumerating data values (in finite domains) while treating time symbolically, thus leading to the classical state explosion problem. This paper proposes a new model of real-time systems as an extension of both symbolic transition systems and timed automata, in order to handle both data and time requirements symbolically. We then adapt the tioco conformance testing theory to deal with this model and describe a test case generation process based on a combination of symbolic execution and constraint solving for the data part and symbolic analysis for timed aspects.x
  @InProceedings{amost,
      Author = {L. Andrade, W. and Machado, P. and Jéron, T. and Marchand, H.},
      Title = {Abstracting Time and Data for Conformance Testing of Real-Time Systems},
      BookTitle = {7th Workshop on Advances in Model Based Testing A-MOST 2011},
      Address = {Berlin, Germany},
      Month = {March},
      Year = {2011}
  }
• Y. Falcone, Fernandez J.-C, T. Jéron, H. Marchand, L. Mounier. More Testable Properties. In 22nd IFIP International Conference on Testing Software and Systems, Lecture note in Computer Science, Volume 6435, Pages 30-46, Natal, Brazil, November 2010. ( Abstract | Bibtex) (Best paper award)
  In this paper, we explore the set of testable properties within the Safety-Progress classification where testability means to establish by testing that a relation, between the tested system and the property under scrutiny, holds. We characterize testable properties wrt. several relations of interest. For each relation, we give a sufficient condition for a property to be testable. Then, we study and delineate, for each Safety-Progress class, the subset of testable properties and their corresponding test oracle producing verdicts for the possible test executions. Furthermore, we address automatic test generation for the proposed framework. Finally, we present a tool implementing the results proposed by this paper
  @InProceedings{ictss-b,
     Author = {Falcone, Y. and J.-C, Fernandez and Jéron, T. and Marchand, H. and Mounier, L.},
     Title = {More Testable Properties},
     BookTitle = {22nd IFIP International Conference on Testing Software and Systems},
     Address = {Natal, Brazil},
     Month = {November},
     Year = {2010}
  }
  

• O. Landry Nguena, H. Marchand, A. Rollet. Automatic Test Generation for Data-Flow Reactive Systems with time constraints (Short paper). In 22nd IFIP International Conference on Testing Software and Systems, Natal, Brazil, November 2010. (Abstract | Bibtex )
  In this paper, we handle the problem of conformance testing for data-flow critical systems with time constraints. We present a formal model (Variable Driven Timed automata) adapted for such systems inspired from timed automata using variables as inputs and outputs, and clocks. In this model, we consider urgency and the possibility to fire several transitions instantaneously. We present a conformance relation for this model and we propose a test generation method using a test purpose approach, based on a region graph transformation of the specification
  @InProceedings{ictss-b,
      Author = {Landry Nguena, O. and Marchand, H. and Rollet, A.},
      Title = {Automatic Test Generation for Data-Flow Reactive Systems with time constraints (Short paper)},
      BookTitle = {22nd IFIP International Conference on Testing Software and Systems},
      Address = {Natal, Brazil},
      Month = {November},
      Year = {2010}
  }
• H. Marchand, J. Dubreil, T. Jéron, Automatic Testing of Access Control for Security Properties, in TestCom'09/FATES'09, LNCS Volume 5826, Pages 113-128, Eindhoven, November 2009. (Abstract | Bibtex)
  In this work, we investigate the combination of controller synthesis and test generation techniques for the testing of open, partially observable systems with respect to security policies. We consider two kinds of properties: integrity properties and confidentiality properties. We assume that the behavior of the system is modeled by a labeled transition system and assume the existence of a black-box implementation. We first outline a method allowing to automatically compute an ideal access control ensuring these two kinds of properties. Then, we show how to derive testers that test the conformance of the implementation with respect to its specification, the correctness of the real access control that has been composed with the implementation in order to ensure a security property, and the security property itself.
  @InProceedings{testcom09,
     Author = {Marchand, H. and Dubreil, J. and Jéron, T.},
     Title = {Automatic Testing of Access Control for Security Properties},
     BookTitle = {TestCom'09},
     Volume = {5826},
     Pages = {113--128},
     Series = {LNCS},
     Publisher = {Springer-Verlag},
     Month = {November},
     Year = {2009}
  }
• C. Constant, T. Jéron, H. Marchand, V. Rusu, Integrating formal verification and conformance testing for reactive systems, IEEE Transactions on Software Engineering, 33(8):558-574, August 2007. (Abstract | Bibtex)
  In this paper, we describe a methodology integrating verification and conformance testing. A specification of a system- an extended input-output automaton, which may be infinite-state-and a set of safety properties ("nothing bad ever happens") and possibility properties ("something good may happen") are assumed. The properties are first tentatively verified on the specification using automatic techniques based on approximated state-space exploration, which are sound, but, as a price to pay for automation, are not complete for the given class of properties. Because of this incompleteness and of state-space explosion, the verification may not succeed in proving or disproving the properties. However, even if verification did not succeed, the testing phase can proceed and provide useful information about the implementation. Test cases are automatically and symbolically generated from the specification and the properties and are executed on a black-box implementation of the system. The test execution may detect violations of conformance between implementation and specification; in addition, it may detect violation/satisfaction of the properties by the implementation and by the specification. In this sense, testing completes verification. The approach is illustrated on simple examples and on a Bounded Retransmission Protocol.
  @article{ieee-tse,
     Author = {Constant, C. and Jéron, T. and Marchand, H. and Rusu, V.},
     Title = {Integrating formal verification and conformance testing for reactive systems},
     Journal = {IEEE Transactions on Software Engineering},
     Volume = {    33},
     Number = {8},
     Pages = {558--574},
     Month = {August},
     Year = {2007}
  }
  

• T. Jéron, H. Marchand, V. Rusu, Symbolic Determinisation of Extended Automata, in 4th IFIP International Conference on Theoretical Computer Science, Stantiago, Chile, August 2006. (See the Research Report IRISA, No 1176, February 2006. (Abstract | Bibtex)
  We define a symbolic determinisation procedure for a class of infinite-state systems, which consists of automata extended with symbolic variables that may be infinite-state. The subclass of extended automata for which the procedure terminates is characterised as bounded lookahead extended automata. It corresponds to automata for which, in any location, the observation of a bounded-length trace is enough to infer the first transition actually taken. We discuss applications of the algorithm to the verification, testing, and diagnosis of infinite-state systems.
  @InProceedings{jeron-marchand-rusu-tcs-deter-06,
     Author = {Jéron, T. and Marchand, H. and Rusu, V.},
     Title = {Symbolic Determinisation of Extended Automata},
     BookTitle = {4th IFIP International Conference on Theoretical Computer Science},
     Pages = {197--212},
     Series = {IFIP book series},
     Publisher = {Springer Science and Business Media},
     Address = {Stantiago, Chile},
     Month = {August},
     Year = {2006}
  }
  

• V. Rusu, H. Marchand, T. Jéron, Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems, in Formal Methods 2005 (FM05), John Fitzgerald, Andrzej Tarlecki, Ian Hayes (eds.), July 2005. (Abstract | Bibtex)
  This paper presents a combination of verification and conformance testing techniques for the formal validation of reactive systems. A formal specification of a system, which may be infinite-state, and a set of safety properties are assumed. Each property is verified on the specification using automatic techniques based on abstract interpretation, which are sound, but, as a price to pay for automation, are not necessarily complete. Next, for each property, a test case is automatically generated from the specification and the property, and is executed on a black-box implementation of the system to detect violations of the property by the implementation and non-conformances between implementation and specification. If the verification step did not conclude, the test execution may also detect violations of the property by the specification.
  @InProceedings{rusu05a,
     Author = {Rusu, Vlad and Marchand, Hervé and Jéron, Thierry},
     Title = {Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems},
     BookTitle = {Formal Methods 2005 (FM05)},
     editor = {Fitzgerald, John and Tarlecki, Andrzej and Hayes, Ian},
     Volume = {    3582},
     Pages = {189--204},
     Series = {LNCS},
     Publisher = {Springer},
     Month = {July},
     Year = {2005}
  }
  

• V. Rusu, H. Marchand, V. Tschaen, T. Jeron, B. Jeannet, From Safety Verification to Safety Testing, in The 16th IFIP International Conference on Testing of Communicating Systems (TestCom04),Oxford, UK, March 2004. (Abstract | Bibtex)
  A methodology that combines verification and conformance testing for validating safety requirements of reactive systems is presented. The requirements are first automatically verifed on the systems specification. Then test cases are automatically derived from the specification and the requirements and executed on a blackbox implementation of the system. The test cases attempt to push the implementation into violating a requirement. We show that an implementation conforms to its specification if and only if it passes all the test cases generated in this way Keywords verification conformance testing safety properties.
  @InProceedings{rusu04b,
     Author = {Rusu, V. and Marchand, H. and Tschaen, V. and Jéron, T. and Jeannet, B.},
     Title = {From Safety Verification to Safety Testing},
     BookTitle = {The 16th IFIP International Conference on Testing of Communicating Systems (TestCom04). Volume 2978 of LNCS},
     Publisher = {Springer-Verlag},
     Address = {Oxford, UK},
     Month = {March},
     Year = {2004}
  }
  

Security

• F. Cassez, J. Dubreil, H. Marchand. Synthesis of Opaque Systems with Static and Dynamic Masks. Formal Methods in System Design, 2012. (Abstract | Bibtex )
  Opacity is a security property formalizing the absence of secret information leakage and we address in this paper the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We choose to control the observability of events by adding a device, called a mask, between the system G and the users. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori by a static mask. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static mask ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time and is chosen by a dynamic mask. We show how to check that a system is opaque w.r.t. to a dynamic mask and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic masks under which S is opaque. Our main result is that the set of such masks can be finitely represented and can be computed in EXPTIME and this is a lower bound. Finally we also address the problem of computing an optimal mask
  @article{FMSD12,
  Author = {Cassez, F. and Dubreil, J. and Marchand, H.},
  Title = {Synthesis of Opaque Systems with Static and Dynamic Masks},
  Journal = {Formal Methods in System Design},
  Year = {2012}
  }
• Y. Falcone, H. Marchand. Various Notions of Opacity Verified and Enforced at Runtime. Research Report INRIA, No 7349, August 2010. (Abstract| Bibtex )
  In this paper, we are interested in the validation of opacity where 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. More specifically, we study how we can verify and enforce, at system runtime, several levels of opacity. Besides already considered notions of opacity, we also introduce a new one that provides a stronger level of confidentiality
  @TechReport{k-opacity,
      Author = {Falcone, Y. and Marchand, H.},
      Title = {Various Notions of Opacity Verified and Enforced at Runtime},
      Number = {7349},
      Institution = {INRIA},
      Month = {August},
      Year = {2010}
  }
  

• Ph. Darondeau, J. Dubreil, H. Marchand. Supervisory Control for Modal Specifications of Services. Workshop on Discrete Event Systems, WODES'10, Pages 428-435, Berlin, Germany, August 2010. ( Abstract | Bibtex )
  In the service oriented architecture framework, a modal specification, as defined by Larsen in \cite{Lar89}, formalises how a service should interact with its environment. More precisely, a modal specification determines the events that the server may or must allow at each stage in an interactive session. Therefore, techniques to enforce a modal specification on a system would be useful for practical applications. In this paper, we investigate the adaptation of the supervisory control theory of Ramadge and Wonham to enforce a modal specification (with final states marking the ends of the sessions) on a system modelled by a finite LTS. We prove that there exists at most one most permissive solution to this control problem. We also prove that this solution is regular and we present an algorithm for the effective computation of the corresponding controller.
  @InProceedings{wodes10-a,
      Author = {Darondeau, Ph. and Dubreil, J. and Marchand, H.},
      Title = {Supervisory Control for Modal Specifications of Services},
      BookTitle = {Workshop on Discrete Event Systems, WODES'10},
      Pages = {428-435},
      Address = {Berlin, Germany},
      Month = {August},
      Year = {2010}
  }
  

• J. Dubreil, Ph. Darondeau, H. Marchand, Supervisory Control for Opacity, IEEE Transactions on Automatic Control, Vol 55(5):1089-1100, May 2010. ( Abstract | Bibtex )
  In the field of computer security, a problem that received little attention so far is the enforcement of confidentiality properties by supervisory control. Given a critical system G that may leak confidential information, the problem consists in designing a controller C, possibly disabling occurrences of a fixed subset of events of G, so that the closed-loop system G/C does not leak confidential information. We consider this problem in the case where G is a finite transition system with set of events A and an inquisitive user, called the adversary, observes a subset Aa of A. The confidential information is the fact (when it is true) that the trace of the execution of G on A* belongs to a regular set S in A, called the secret. The secret S is said to be opaque w.r.t. G (resp. G/C) and Aa if the adversary cannot safely infer this fact from the trace of the execution of G (resp. G/C) on Aa*. In the converse case, the secret can be disclosed. We present an effective algorithm for computing the most permissive controller C such that S is opaque w.r.t. G/C and Aa. This algorithm subsumes two earlier algorithms working under the strong assumption that the alphabet Aa of the adversary and the set of events that the controller can disable are comparable.
  @article{dubreil09b,
     Author = {Dubreil, J. and Darondeau, Ph. and Marchand, H.},
     Title = {Supervisory Control for Opacity},
     Journal = {IEEE Transactions on Automatic Control},
     Volume = {55},
     Number = {5},
     Pages = {1089-1100},
     Year = {2010}
  }
  
• H. Marchand, J. Dubreil, T. Jéron, Automatic Testing of Access Control for Security Properties, in TestCom'09, LNCS Volume 5826, Pages 113-128, Eindhoven, November 2009. ( Abstract | Bibtex )
  In this work, we investigate the combination of controller synthesis and test generation techniques for the testing of open, partially observable systems with respect to security policies. We consider two kinds of properties: integrity properties and confidentiality properties. We assume that the behavior of the system is modeled by a labeled transition system and assume the existence of a black-box implementation. We first outline a method allowing to automatically compute an ideal access control ensuring these two kinds of properties. Then, we show how to derive testers that test the conformance of the implementation with respect to its specification, the correctness of the real access control that has been composed with the implementation in order to ensure a security property, and the security property itself.
  @InProceedings{testcom09,
      Author = {Marchand, H. and Dubreil, J. and Jéron, T.},
      Title = {Automatic Testing of Access Control for Security Properties},
      BookTitle = {TestCom'09},
      Volume = {5826},
      Pages = {113--128},
      Series = {LNCS},
      Publisher = {Springer-Verlag},
      Month = {November},
      Year = {2009}
  }
• J. Dubreil, T. Jéron, H. Marchand, Monitoring Confidentiality by Diagnosis Techniques, in European Control Conference, Pages 2584-2590, Budapest, Hungary, August 2009. ( Abstract | Bibtex )
  In this paper, we are interested in constructing monitors for the detection of confidential information flow in the context of partially observable discrete event systems. We focus on the case where the secret information is given as a regular language. We first characterize the set of observations allowing an attacker to infer the secret behaviors. We consider the general case where the attacker and the administrator have different partial views of the system. Further, based on the diagnosis of discrete event systems, we provide necessary and sufficient conditions under which detection and prediction of secret information flow can be ensured and a construction of a monitor ensuring this task.
  @InProceedings{dubreil09a,
      Author = {Dubreil, J. and Jéron, T. and Marchand, H.},
      Title = {Monitoring Confidentiality by Diagnosis Techniques},
      BookTitle = {European Control Conference},
      Pages = {2584--2590},
      Address = {Budapest, Hungary},
      Month = {August},
      Year = {2009}
  }
• J. Dubreil, Ph. Darondeau, H. Marchand, Opacity Enforcing Control Synthesis, in Workshop on Discrete Event Systems, WODES'08, Pages 28-35, Gothenburg, Sweden, March 2008. ( Abstract | Bibtex )
  Given a finite transition system and a regular predicate, we address the problem of computing a controller enforcing the opacity of the predicate against an attacker (who partially observes the system), supposedly trying to push the system to reveal the predicate. Assuming that the controller can only control a subset of the events it observes (possibly different from the ones of the attacker), we show that an optimal control always exists and provide sufficient conditions under which it is regular and effectively computable. These conditions rely on the inclusion relationships between the controllable alphabet and the observable alphabets of the attacker and of the controller.
  @InProceedings{opacity2,
      Author = {Dubreil, J. and Darondeau, Ph. and Marchand, H.},
      Title = {Opacity Enforcing Control Synthesis},
      BookTitle = {Workshop on Discrete Event Systems, WODES'08},
      Pages = {28--35},
      Address = {Gothenburg, Sweden},
      Month = {March},
      Year = {2008}
  }

Diagnosis of Discrete-Event Systems

• J. Dubreil, T. Jéron, H. Marchand, Monitoring Confidentiality by Diagnosis Techniques, in European Control Conference, Budapest, Hungary, August 2009. (Abstract | Bibtex)
  In this paper, we are interested in constructing monitors for the detection of confidential information flow in the context of partially observable discrete event systems. We focus on the case where the secret information is given as a regular language. We first characterize the set of observations allowing an attacker to infer the secret behaviors. We consider the general case where the attacker and the administrator have different partial views of the system. Further, based on the diagnosis of discrete event systems, we provide necessary and sufficient conditions under which detection and prediction of secret information flow can be ensured and a construction of a monitor ensuring this task.
  @InProceedings{dubreil09a,
     Author = {Dubreil, J. and Jéron, T. and Marchand, H.},
     Title = {Monitoring Confidentiality by Diagnosis Techniques},
     BookTitle = {European Control Conference},
     Pages = {2584--2590},
     Address = {Budapest, Hungary},
     Month = {August},
     Year = {2009}
  }
• T. Jéron, H. Marchand, S. Genc, S. Lafortune, Predictability of Sequence Patterns in Discrete Event Systems, in IFAC World Congress, Seoul, Korea, July 2008. (Abstract | Bibtex)
  The problem of predicting the occurrences of a pattern in a partially-observed discrete-event system is studied. The system is modeled by a labeled transition system. The pattern is a set of event sequences modeled by a finite-state automaton. The occurrences of the pattern are predictable if it is possible to infer about any occurrence of the pattern before the pattern is completely executed by the system. An off-line algorithm to verify the property of predictability is presented. The verification is polynomial in the number of states of the system. An on-line algorithm to track the execution of the pattern during the operation of the system is also presented. This algorithm is based on the use of a diagnoser automaton. The results are illustrated using an example from computer systems.
  @InProceedings{ifac2008,
     Author = {Jéron, T. and Marchand, H. and Genc, S. and Lafortune, S.},
     Title = {Predictability of Sequence Patterns in Discrete Event Systems},
     BookTitle = {IFAC World Congress},
     Pages = {537--453},
     Address = {Seoul, Korea},
     Month = {July},
     Year = {2008}
  }
  

• T. Jéron, H. Marchand, S. Pinchinat, M-O. Cordier, Supervision Patterns in Discrete Event Systems Diagnosis, in Workshop on Discrete Event Systems, WODES'06, July 2006. (Abstract | Bibtex)
  In this paper, we are interested in the diagnosis of discrete event systems modeled by finite transition systems. We propose a model of supervision patterns general enough to capture past occurrences of particular trajectories of the system. Modeling the diagnosis objective by a supervision pattern allows us to generalize the properties to be diagnosed and to render them independent of the description of the system. We first formally define the diagnosis problem in this context. We then derive techniques for the construction of a diagnoser and for the verification of the diagnosticability based on standard operations on transition systems. We show that these techniques are general enough to express and solve in a unified way a broad class of diagnosis problems found in the literature, e.g. diagnosing permanent faults, multiple faults, fault sequences and some problems of intermittent faults.
  @InProceedings{wodes-jeron-marchand-pinchinat-cordier-06,
     Author = {Jéron, T. and Marchand, H. and Pinchinat, S. and Cordier, M-O.},
     Title = {Supervision Patterns in Discrete Event Systems Diagnosis},
     BookTitle = {Workshop on Discrete Event Systems, WODES'06},
     Address = {Ann-Arbor (MI, USA)},
     Month = {July},
     Year = {2006}
  }
  

• H. Marchand, L. Rozé, Diagnostic de pannes sur des systèmes à événements discrets : une approche à base de modèles symboliques, in 13ème Congrès Francophone AFRIF-AFIA de Reconnaissance des Formes et Intelligence Artificielle, Pages 191-200, Angers, France, January 2002. (Abstract | Bibtex) (In French)
  Nous présentons une technique de supervision s'appuyant sur une représentation symbolique du modèle du système à superviser et de l'outil utilisé pour effectuer le diagnostic (le diagnostiqueur). Basé sur une approche polynomiale, nous utilisons pour représenter le modèle un automate de Moore symbolique qui permet de représenter des systèmes de grandes tailles. La partie combinatoire la plus importante de ce travail se situe au niveau de l'algorithme de construction du diagnostiqueur et a été diminuée par l'introduction d'une réduction symbolique du modèle (modèle quotient par rapport à une relation d'équivalence s'appuyant sur l'histoire du système). L'intérêt de cette réduction symbolique est grande puisqu'elle permet d'effectuer les calculs de la fonction de transition hors ligne lors d'un prétraitement, réduisant ainsi considérablement le travail devant être effectué en ligne.
  @InProceedings{marchand02a,
     Author = {Marchand, H. and Rozé, L.},
     Title = {Diagnostic de pannes sur des systèmes à événements discrets : une approche à base de modèles symboliques},
     BookTitle = {13ème Congrès Francophone AFRIF-AFIA de Reconnaissance des Formes et Intelligence Artificielle},
     Pages = {191--200},
     Address = {Angers, France},
     Month = {January},
     Year = {2002}
  }
  

Control of Infinite Symbolic Systems handling data

• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Synthesis of Communicating Controllers for Distributed Systems. In 50th IEEE Conference on Decision and Control and European Control Conference, Pages 1803-1810, Orlando, USA, December 2011. (Abstract | Bibtex )
  We consider the control of distributed systems composed of subsystems communicating asynchronously; the aim is to build local controllers that restrict the behavior of a distributed system in order to satisfy a global state avoidance property. We model our distributed systems as communicating finite state machines with reliable unbounded FIFO queues between subsystems. The local controllers can only observe the behavior of their proper local subsystem and do not see the queue contents. To refine their control policy, they can use the FIFO queues to communicate by piggybacking extra information to the messages sent by the subsystems. We define synthesis algorithms allowing to compute the local controllers. We explain how we can ensure the termination of this control algorithm by using abstract interpretation techniques, to overapproximate queue contents by regular languages. An implementation of our algorithms provides an empirical evaluation of our method
  @InProceedings{CDC2011,
  Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
  Title = {Synthesis of Communicating Controllers for Distributed Systems},
  BookTitle = {50th IEEE Conference on Decision and Control and European Control Conference},
  Pages = {1803--1810},
  Address = {Orlando, USA},
  Month = {December},
  Year = {2011}
  }
• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Decentralized Control of Infinite Systems. Discrete Event Dynamic Systems : Theory and Applications, 21(3):359-393, September 2011. (Abstract | Bibtex )
  We propose algorithms for the synthesis of decentralized state-feedback controllers with partial observation of infinite state systems, which are modeled by Symbolic Transition Systems. We first consider the computation of safe controllers ensuring the avoidance of a set of forbidden states and then extend this result to the deadlock free case. The termination of the algorithms solving these problems is ensured by the use of abstract interpretation techniques, but at the price of overapproximations, in particular, in the computation of the states which must be avoided. We then extend our algorithms to the case where the system to be controlled is given by a collection of subsystems (modules). This structure is exploited to locally compute a controller for each module. Our tool SMACS gives an empirical evaluation of our methods by showing their feasibility, usability and efficiency.
  @article{deds112,
      Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
      Title = {Decentralized Control of Infinite Systems},
      Volume = {21},
  Number = {3}
  pages = {359-393}
  Month = {September},
  Journal = {Discrete Event Dynamic Systems : Theory and Applications},
      Year = {2011}
  }
• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Global State Estimates for Distributed Systems. In 31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems, FORTE, Reykjavik, Iceland, June 2011. (Abstract | Bibtex )
  We consider distributed systems modeled as communicating finite state machines with reliable unbounded FIFO channels. As an essential sub-routine for control, monitoring and diagnosis applications, we provide an algorithm that computes, during the execution of the system, an estimate of the current global state of the distributed system for each local subsystem. This algorithm does not change the behavior of the system; each subsystem only computes and records a symbolic representation of the state estimates, and piggybacks some extra information to the messages sent to the other subsystems in order to refine their estimates. Our algorithm relies on the computation of reachable states. Since the reachability problem is undecidable in our model, we use abstract interpretation techniques to obtain regular overapproximations of the possible FIFO channel contents, and hence of the possible current global states. An implementation of this algorithm provides an empirical evaluation of our method.
  @InProceedings{forte2011,
      Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
      Title = {Global State Estimates for Distributed Systems},
      BookTitle = {31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems, FORTE},
      Address = {Reykjavik, Iceland},
      Month = {June},
      Year = {2011}
  }
• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Symbolic Supervisory Control of Infinite Transition Systems under Partial Observation using Abstract Interpretation. Discrete Event Dynamic Systems : Theory and Applications, (To appear), 2011. (Abstract | Bibtex )
  We propose algorithms for the synthesis of state-feedback controllers with partial observation of infinite state discrete event systems modelled by Symbolic Transition Systems. We provide models of safe memoryless controllers both for potentially deadlocking and deadlock free controlled systems. The termination of the algorithms solving these problems is ensured using abstract interpretation techniques which provide an overapproximation of the transitions to disable. We then extend our algorithms to controllers with memory and to online controllers. We also propose improvements in the synthesis of controllers in the finite case which, to our knowledge, provide more permissive solutions than what was previously proposed in the literature. Our tool SMACS gives an empirical validation of our methods by showing their feasibility, usability and efficiency
  @article{deds11a,
      Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
      Title = {Symbolic Supervisory Control of Infinite Transition Systems under Partial Observation using Abstract Interpretation},
      Journal = {Discrete Event Dynamic Systems : Theory and Applications},
      Year = {2011}
  }
• G. Kalyon, Le Gall T, H. Marchand, T. Massart, Control of Infinite Symbolic Transition Systems under Partial Observation, in European Control Conference, Pages 1456-1462, Budapest, Hungary, August 2009. (Abstract | Bibtex)
  We provide models of safe controllers both for potentially blocking and non blocking controlled systems. To obtain algorithms for these problems, we make the use of abstract interpretation techniques which provide over-approximations of the transitions set to be disabled. To our knowledge, with the hypotheses taken, the improved version of our algorithm provides a better solution than what was previously proposed in the literature. Our tool SMACS allowed us to make an empirical validation of our methods to show their feasibility and usability.
  @InProceedings{kalyon09a,
     Author = {Kalyon, G. and Gall T, Le and Marchand, H. and Massart, T.},
     Title = {Control of Infinite Symbolic Transition Systems under Partial Observation},
     BookTitle = {European Control Conference},
     Pages = {1456--1462},
     Address = {Budapest, Hungary},
     Month = {August},
     Year = {2009}
  }
• T. Le Gall, B. Jeannet, H. Marchand, Contrôle de systèmes symboliques, discrets ou hybrides, Technique et Science Informatiques (TSI), 25:293-319, 2006. (Abstract | Bibtex )
  Nous abordons le problème de la synthèse de contrôleurs à travers différents modèles allant des systèmes de transitions finis aux systèmes hybrides en nous intéressant à des propriétés de sûreté. Dans ce cadre, nous nous intéressons principalement au problème de synthèse pour un modèle intermédiaire : les systèmes de transitions symboliques. L'analyse des besoins de modélisation nous amène à redéfinir la notion de contrôlabilité en faisant porter le caractère de contrôlabilité non plus sur les événements mais sur les gardes des transitions, puis à définir des algorithmes de synthèse permettant l'usage d'approximations et d'assurer la terminaison des calculs. Nous généralisons par la suite notre méthodologie au contrôle de systèmes hybrides, ce qui donne un cadre unifié du problème de la synthèse pour un ensemble consistant de modèles.
  @article{tsi-legall-jeannet-marchand-06,
     Author = {Le Gall, T. and Jeannet, B. and Marchand, H.},
     Title = {Contrôle de systèmes symboliques, discrets ou hybrides},
     Journal = {Technique et Science Informatiques (TSI)},
     Volume = {25},
     Pages = {293--319},
     Year = {2006}
  }
  

• T. Le Gall, B. Jeannet, H. Marchand, Supervisory Control of Infinite Symbolic Systems using Abstract Interpretation, in 44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Pages 31-35, Seville (Spain), December 2005. (Abstract | Bibtex)
  Nous abordons le problème de la synthèse de contrôleurs à travers différents modèles allant des systèmes de transitions finis aux systèmes hybrides en nous intéressant à des propriétés de sûreté. Dans ce cadre, nous nous intéressons principalement au problème de synthèse pour un modèle intermédiaire : les systèmes de transitions symboliques. L'analyse des besoins de modélisation nous amène à redéfinir la notion de contrôlabilité en faisant porter le caractère de contrôlabilité non plus sur les événements mais sur les gardes des transitions, puis à définir des algorithmes de synthèse permettant l'usage d'approximations et d'assurer la terminaison des calculs. Nous généralisons par la suite notre méthodologie au contrôle de systèmes hybrides, ce qui donne un cadre unifié du problème de la synthèse pour un ensemble consistant de modèles.
  @InProceedings{legall05b,
     Author = {Le Gall, T. and Jeannet, B. and Marchand, H.},
     Title = {Supervisory Control of Infinite Symbolic Systems using Abstract Interpretation},
     BookTitle = {44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005},
     Pages = {31--35},
     Address = {Seville (Spain)},
     Month = {December},
     Year = {2005}
  }
  

Control of Structured Discrete Event Systems

Control of Concurrent/distributed systems

• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Synthesis of Communicating Controllers for Distributed Systems. In 50th IEEE Conference on Decision and Control and European Control Conference, Pages 1803-1810, Orlando, USA, December 2011. (Abstract | Bibtex )
  We consider the control of distributed systems composed of subsystems communicating asynchronously; the aim is to build local controllers that restrict the behavior of a distributed system in order to satisfy a global state avoidance property. We model our distributed systems as communicating finite state machines with reliable unbounded FIFO queues between subsystems. The local controllers can only observe the behavior of their proper local subsystem and do not see the queue contents. To refine their control policy, they can use the FIFO queues to communicate by piggybacking extra information to the messages sent by the subsystems. We define synthesis algorithms allowing to compute the local controllers. We explain how we can ensure the termination of this control algorithm by using abstract interpretation techniques, to overapproximate queue contents by regular languages. An implementation of our algorithms provides an empirical evaluation of our method
  @InProceedings{CDC2011,
  Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
  Title = {Synthesis of Communicating Controllers for Distributed Systems},
  BookTitle = {50th IEEE Conference on Decision and Control and European Control Conference},
  Pages = {1803--1810},
  Address = {Orlando, USA},
  Month = {December},
  Year = {2011}
  }
• G. Kalyon, T. Le Gall, H. Marchand, T. Massart. Global State Estimates for Distributed Systems. In 31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems, FORTE, Reykjavik, Iceland, June 2011. (Abstract | Bibtex )
  We consider distributed systems modeled as communicating finite state machines with reliable unbounded FIFO channels. As an essential sub-routine for control, monitoring and diagnosis applications, we provide an algorithm that computes, during the execution of the system, an estimate of the current global state of the distributed system for each local subsystem. This algorithm does not change the behavior of the system; each subsystem only computes and records a symbolic representation of the state estimates, and piggybacks some extra information to the messages sent to the other subsystems in order to refine their estimates. Our algorithm relies on the computation of reachable states. Since the reachability problem is undecidable in our model, we use abstract interpretation techniques to obtain regular overapproximations of the possible FIFO channel contents, and hence of the possible current global states. An implementation of this algorithm provides an empirical evaluation of our method.
  @InProceedings{forte2011,
      Author = {Kalyon, G. and Le Gall, T. and Marchand, H. and Massart, T.},
      Title = {Global State Estimates for Distributed Systems},
      BookTitle = {31th IFIP International Conference on FORmal TEchniques for Networked and Distributed Systems, FORTE},
      Address = {Reykjavik, Iceland},
      Month = {June},
      Year = {2011}
  }
• J. Komenda, J. van Schuppen, B. Gaudin, H. Marchand, Supervisory Control of Modular Systems with Global Specification Languages, Automatica, 44:1127-1134, 2008. (Abstract | Bibtex)
  The paper presents sufficient conditions for modular (supervisory) control synthesis to equal global control synthesis. In modular control synthesis a supervisory control is synthesized for each module separately and the supervisory control consists of the parallel composition of the modular supervisory controls. The general case of the specification that is indecomposable and not necessarily contained in the plant language, which is often the case in practice, is considered. The usual assumption that all shared events are controllable is relaxed by introducing two new structural conditions relying on the global mutual controllability condition. The novel concept used as a sufficient structural condition is strong global mutual controllability. The main result uses a weaker condition called global mutual controllability together with local consistency of the specification. An example illustrates the approach.
  @article{komenda-automatica,
     Author = {Komenda, J. and van Schuppen, J. and Gaudin, B. and Marchand, H.},
     Title = {Supervisory Control of Modular Systems with Global Specification Languages},
     Journal = {Automatica},
     Volume = {    44},
     Number = {4},
     Pages = {1127--1134},
     Month = {April},
     Year = {2008}
  }
  

• B. Gaudin, H. marchand, An Efficient Modular Method for the Control of Concurrent Discrete Event Systems: A Language-Based Approach, Discrete Event Dynamic System, 17(2):179-209, 2007.(Abstract | Bibtex)
  In this paper, we are interested in the control of a particular class of Concurrent Discrete Event Systems defined by a collection of components that interact with each other. We investigate the computation of the supremal controllable language contained in the language of the specification. We do not adopt the decentralized approach. Instead, we have chosen to use a modular centralized approach and to perform the control on some approximations of the plant derived from the behavior of each component. The behavior of these approximations is restricted so that they respect a new language property for discrete event systems called partial controllability condition that depends on the specification. It is shown that, under some assumptions, the intersection of these ``controlled approximations'' corresponds to the supremal controllable language contained in the specification with respect to the plant. This computation is performed without having to build the whole plant, hence avoiding the state space explosion induced by the concurrent nature of the plant. It is finally shown that the class of specifications on which our method can be applied strictly subsumes the class of separable specifications.
  @article{deds-gaudin-marchand-07,
     Author = {Gaudin, B. and marchand, H.},
     Title = {An Efficient Modular Method for the Control of Concurrent Discrete Event Systems: A Language-Based Approach},
     Journal = {Discrete Event Dynamic System},
     Volume = {    17},
     Number = {2},
     Pages = {179--209},
     Year = {2007}
  }
  

• K. Schmidt, H. Marchand, G. Gaudin, Modular and Decentralized Supervisory Control of Concurrent Discrete Event Systems Using Reduced System Models, in Workshop on Discrete Event Systems, WODES'06, July 2006. (Abstract | Bibtex)
  This work investigates the supervisor synthesis for concurrent systems based on reduced system models with the intention of complexity reduction. It is assumed that the expected behavior (specification) is given on a subset of the system alphabet, and the system behavior is reduced to this alphabet. Supervisors are computed for each reduced subsystem employing a modular decentralized approach. Depending on the chosen architecture, we provide sufficient conditions for the consistent implementation of the reduced supervisors for the original system.
  @InProceedings{wodes-schmidt-marchand-gaudin-06,
     Author = {Schmidt, K. and Marchand, H. and Gaudin, B.},
     Title = {Modular and Decentralized Supervisory Control of Concurrent Discrete Event Systems Using Reduced System Models},
     BookTitle = {Workshop on Discrete Event Systems, WODES'06},
     Pages = {149--154},
     Address = {Ann-Arbor (MI, USA)},
     Month = {July},
     Year = {2006}
  }
  

• J. Komenda, H. Marchand, S. Pinchinat, A constructive approach to decentralized supervisory Control problems, in 3rd IFAC Workshop on Discrete-Event System Design, 2006. (Abstract | Bibtex)
  We plunge decentralized control problems into modular ones to benefit from the know-how of modular control theory: any decentralized control problem is associated to a natural modular control problem, which over-approximates it. Then, we discuss how a solution of the latter problem delivers a solution of the former.
  @InProceedings{komenda06a,
     Author = {Komenda, J. and Marchand, H. and Pinchinat, S.},
     Title = {A constructive approach to decentralized supervisory Control problems},
     BookTitle = {3rd IFAC Workshop on Discrete-Event System Design},
     Year = {2006}
  }
  

• B. Gaudin, H. Marchand, Supervisory Control and Deadlock Avoidance Control Problem for Concurrent Discrete Event Systems, in 44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Pages 2763-2768, Seville (Spain), December 2005. (Abstract | Bibtex)
  In this paper, we tackle the Supervisory Control Problem control for Concurrent Discrete Event Systems. These are systems that are defined by a collection of components that interact with each other. In this study, we first outline the method allowing to solve the state avoidance control problem on concurrent system, without having to compute the whole system. We then present results offering an efficient method to detect deadlock states in the controlled system due either to the composition or to the control that is performed on the system.
  @InProceedings{gaudin05d,
     Author = {Gaudin, B. and Marchand, H.},
     Title = {Supervisory Control and Deadlock Avoidance Control Problem for Concurrent Discrete Event Systems},
     BookTitle = {44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005},
     Pages = {2763--2768},
     Address = {Seville (Spain)},
     Month = {December},
     Year = {2005}
  }
  

• B. Gaudin, H. Marchand, Efficient Computation of supervisors for loosely synchronous Discrete Event Systems: A State-Based Approach, in 6th IFAC World Congress, Prague, Czech Republic, July 2005. (Abstract | Bibtex)
  In this paper, we are interested in the control of a particular class of Concurrent Discrete Event Systems defined by a collection of components that interact with each other. We here consider the state avoidance control problem. We provide algorithms that, based on a particular decomposition of the set of forbidden states, locally solve the control problem (i.e. on each component without computing the whole system) and produce a global supervisor, that can be efficiently evaluated on the fly.
  @InProceedings{gaudin05d,
     Author = {Gaudin, B. and Marchand, H.},
     Title = {Supervisory Control and Deadlock Avoidance Control Problem for Concurrent Discrete Event Systems},
     BookTitle = {44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005},
     Pages = {2763--2768},
     Address = {Seville (Spain)},
     Month = {December},
     Year = {2005}
  }
  

• J. Komenda, J. H. van Schuppen, B. Gaudin, H. Marchand, Modular supervisory control with general indecomposable specification languages, in 44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005, Pages 3474-3479, Seville (Spain), December 2005. (Abstract | Bibtex)
  Modular supervisory control of discrete-event systems (DES), where the global DES is composed of local components that run concurrently, is considered. For supervisory control of large-scale modular DES the possibility of performing control-related computations locally (in components) is of utmost importance to computational complexity. Recently we have treated the case, where the specification language is decomposable into local specification languages and is included in the (global) plant language. In this paper the case of general specification languages that are neither necessarily decomposable nor contained in the global plant language is studied. Sufficient conditions are found under which any manipulation with the global plant is avoided for the computation of supremal controllable sublanguages of (global) indecomposable specification languages.
  @InProceedings{komenda05a,
     Author = {Komenda, J. and H. van Schuppen, J. and Gaudin, B. and Marchand, H.},
     Title = {Modular supervisory control with general indecomposable specification languages},
     BookTitle = {44nd IEEE Conference on Decision and Control (CDC'05) and Control and European Control Conference ECC 2005},
     Pages = {3474--3479},
     Address = {Seville (Spain)},
     Month = {December},
     Year = {2005}
  }
  

• B. Gaudin, H. Marchand, Modular Supervisory Control of a class of Concurrent Discrete Event Systems, in Workshop on Discrete Event Systems, WODES'04, Septembre 2004. (Abstract | Bibtex)
  In this paper, we are interested in the control of a particular class of Concurrent Discrete Event Systems defined by a collection of components that interact with each other. We investigate the computation of the supremal controllable language contained in the one of the specification. We do not adopt the decentralized approach. Instead, we have chosen to perform the control on some approximations of the plant derived from the behavior of each component. The behavior of these approximations is restricted so that they respect a new language property for discrete event systems called partial controllability condition that depends on the specification. It is shown that, under some assumptions, the intersection of these ``controlled approximations'' corresponds to the supremal controllable language contained in the specification with respect to the plant. This computation is performed without having to build the whole plant, hence avoiding the state space explosion induced by the concurrent nature of the plant.
  @InProceedings{gaudin04c,
     Author = {Gaudin, B. and Marchand, H.},
     Title = {Modular Supervisory Control of a class of Concurrent Discrete Event Systems},
     BookTitle = {Workshop on Discrete Event Systems, WODES'04},
     Pages = {181--186},
     Month = {September},
     Year = {2004}
  }
  

Control of Hierarchical systems

• B. Gaudin, H. Marchand, Safety Control of Hierarchical Synchronous Discrete Event Systems: A State-Based Approach, in 13th Mediterranean Conference on Control and Automation, Pages 889-895, Limassol, Cyprus, June 2005. (Abstract | Bibtex)
  In this paper, we discuss the control of a particular class of Hierarchical Discrete Event Systems and the state avoidance control problem is considered. A methodology is provided that locally computes on each component of the system the set of bad states (these are the states that may lead to the forbidden states via an uncontrollable trajectory). This is performed without computing the whole system. At this point, the supervisor is evaluated on the fly w.r.t. the bad states and thus requires an on-line evaluation in order to determine the set of events that has to be disabled by control. It is performed in such a way that the global partial transition function does not need to be built.
  @InProceedings{gaudin05b,
     Author = {Gaudin, B. and Marchand, H.},
     Title = {Safety Control of Hierarchical Synchronous Discrete Event Systems: A State-Based Approach},
     BookTitle = {13th Mediterranean Conference on Control and Automation},
     Pages = {889--895},
     Address = {Limassol, Cyprus},
     Month = {June},
     Year = {2005}
  }
  

• B. Gaudin, H Marchand, Supervisory Control of Product and Hierarchical Discrete Event Systems, European Journal of Control, 10(2), 2004. (Abstract | Bibtex)
  In this paper, the supervisory control of a class of Discrete Event Systems is investigated. Discrete event systems are modeled either by a collection of Finite State Machines that behave asynchronously or by a Hierarchical Finite State Machine. The basic problem of interest is to ensure the invariance of a set of particular configurations in the system. When the system is modeled as asynchronous FSMs, we provide algorithms that, based on a particular decomposition of the set of forbidden configurations, solve the control problem locally (i.e. on each component without computing the whole system) and produce a global supervisor ensuring the desired property. We then provide sufficient conditions under which the obtained controlled system is non-blocking. This kind of objectives may be useful to perform dynamic interactions between different parts of a system. Finally, we apply these results to the case of Hierarchical Finite State Machines.
  @article{gaudin04b,
     Author = {Gaudin, B. and Marchand, H},
     Title = {Supervisory Control of Product and Hierarchical Discrete Event Systems},
     Journal = {European Journal of Control},
     Volume = {10},
     Number = {2},
     Year = {2004}
  }
  

• H. Marchand, B. Gaudin, Supervisory Control Problems of Hierarchical Finite State Machines, in 41th IEEE Conference on Decision and Control, Las Vegas, USA, December 2002. (Abstract | Bibtex)
  In this paper, the supervisory control of a class of Discrete Event Systems is investigated. Discrete event systems are modeled either by a collection of Finite State Machines that behave asynchronously or by a Hierarchical Finite State Machine. The basic problem of interest is to ensure the invariance of a set of particular configurations in the system. When the system is modeled as asynchronous FSMs, we provide algorithms that, based on a particular decomposition of the set of forbidden configurations, solve the control problem locally (i.e. on each component without computing the whole system) and produce a global supervisor ensuring the desired property. We then provide sufficient conditions under which the obtained controlled system is non-blocking. This kind of objectives may be useful to perform dynamic interactions between different parts of a system. Finally, we apply these results to the case of Hierarchical Finite State Machines.
  @InProceedings{marchand02e,
     Author = {Marchand, H. and Gaudin, B.},
     Title = {Supervisory Control Problems of Hierarchical Finite State Machines},
     BookTitle = {41th IEEE Conference on Decision and Control},
     Address = {Las Vegas, USA},
     Month = {December},
     Year = {2002}
  }
  

Optimal Control of Discrete Event Systems

• E. Dumitrescu, A. Girault, H. Marchand, E. Rutten. Multicriteria optimal discrete controller synthesis for fault-tolerant real-time tasks. Workshop on Discrete Event Systems, WODES'10, Pages 366-373, Berlin, Germany, August 2010. ( Abstract | Bibtex )
  We propose a technique for discrete controller synthesis, with optimal synthesis on bounded paths, in order to model, design, and optimize fault-tolerant distributed systems, taking into account several criteria (e.g., the execution costs of the tasks and their quality of service). Different combinations are explored for multi-criteria optimization
  @InProceedings{wodes10-b,
      Author = {Dumitrescu, E. and Girault, A. and Marchand, H. and Rutten, E.},
      Title = {Multicriteria optimal discrete controller synthesis for fault-tolerant real-time tasks},
      BookTitle = {Workshop on Discrete Event Systems, WODES'10},
      Pages = {366-373},
      Address = {Berlin, Germany},
      Month = {August},
      Year = {2010}
  }
  

• E. Dumitrescu, A. Girault, H. Marchand, E. Rutten, Optimal discrete controller synthesis for the modeling of fault-tolerant distributed systems, in First IFAC Workshop on Dependable Control of Discrete Systems (DCDS'07), Paris, France, June 2007. (Abstract | Bibtex). See the Research Report 6137:
  Embedded systems require safe design methods based on formal methods, as well as safe execution based on fault-tolerance techniques. We propose a safe design method for safe execution systems: it uses optimal discrete controller synthesis (DCS) to generate a correct recon guring fault-tolerant system. The properties enforced concern consistent execution, functionality ful llment (whatever the faults, under some failure hypothesis), and several optimizations, particularly on the execution time when going through checkpoints. We propose an algorithm for optimal DCS on bounded paths. We propose model patterns for a set of periodic tasks with checkpoints, a set of distributed, heterogeneous and fail-silent processors, and an environment model that expresses the potential fault patterns. We use synchronous models, the Sigali symbolic DCS tool and Mode Automata.
  @InProceedings{Dumitrescu07b,
     Author = {Dumitrescu, E. and Girault, A. and Marchand, H. and Rutten, E.},
     Title = {Optimal discrete controller synthesis for the modeling of fault-tolerant distributed systems},
     BookTitle = {First IFAC Workshop on Dependable Control of Discrete Systems (DCDS'07)},
     Address = {Paris, France},
     Month = {June},
     Year = {2007}
  }
  

• H. Marchand, O. Boivineau, S. Lafortune. On Optimal Control of a class of partially-Observed Discrete Event Systems.  Automatica, 38(11):1935-1943, October 2002. (Abstract | Bibtex)
  We are interested in a new class of optimal control problems for Discrete Event Systems (DES). We adopt the formalism of supervisory control theory [Ramadge89] and model the system as a finite state machine (FSM). Our control problem is characterized by the presence of uncontrollable as well as unobservable events, the notion of occurrence and control costs for events and a worst-case objective function. We first derive an observer for the partially unobservable FSM, which allows us to construct an approximation of the unobservable trajectory costs. We then define the performance measure on this observer rather than on the original FSM itself. We then use the algorithm presented in [sengupta98] to synthesize an optimal submachine of the C-observer. This submachine leads to the desired supervisor for the system.
  @article{marchand02c,
     Author = {Marchand, H. and Boivineau, O. and Lafortune, S.},
     Title = {On Optimal Control of a class of partially-Observed Discrete Event Systems},
     Journal = {Automatica},
     Volume = {38},
     Number = {11},
     Pages = {1935--1943},
     Month = {October},
     Year = {2002}
  }
  

• H Marchand, O. Boivineau, S. Lafortune, On the Synthesis of Optimal Schedulers in Discrete Event Control Problems with Multiple Goals, SIAM Journal on Control and Optimization, 39(2):512-532, 2000. (Abstract | Bibtex)
  This paper deals with a new type of optimal control for Discrete Event Systems. Our control problem extends the theory of [sengupta98], that is characterized by the presence of uncontrollable events, the notion of occurrence and control costs for events, and a worst-case objective function. A significant difference with [sengupta98] is that our aim is to make the system evolve through a set of multiple goals, one by one, with no order necessarily pre-specified, whereas the previous theory only deals with a single goal. Our solution approach is divided into two steps. In the first step, we use the optimal control theory in [sengupta98] to synthesize individual controllers for each goal. In the second step, we develop the solution of another optimal control problem, namely, how to modify if necessary and piece together, or schedule, all of the controllers built in the first step in order to visit each of the goals with least total cost. We solve this problem by defining the notion of a scheduler and then by mapping the problem of finding an optimal scheduler to an instance of the well-known Traveling Salesman Problem (TSP). We finally suggest various strategies to reduce the complexity of the TSP resolution while still preserving global optimality.
  @article{marchand00b,
     Author = {Marchand, H and Boivineau, O. and Lafortune, S.},
     Title = {On the Synthesis of Optimal Schedulers in Discrete Event Control Problems with Multiple Goals},
     Journal = {SIAM Journal on Control and Optimization},
     Volume = {39},
     Number = {2},
     Pages = {512--532},
     Year = {2000}
  }
  

• H. Marchand, M. Le Borgne, On the Optimal Control of Polynomial Dynamical Systems over Z/pZ, in 4th IEE International Workshop on Discrete Event Systems, Pages 385-390, Cagliari, Italie, August 1998. (Abstract | Bibtex)
  This paper describes how a polynomial equationnal approach of the theory of logic discrete event systems leads to efficient algorithms for the synthesis of supervisory controllers. Even if traditional control objectives can be considered in our framework (invariance, reachability or attractivity), we address here the synthesis of optimal controller with control objectives specified as a minimization of a given cost function over the states through the trajectories of the system.
  @InProceedings{marchand98b,
     Author = {Marchand, H. and Le Borgne, M.},
     Title = {On the Optimal Control of Polynomial Dynamical Systems over Z/pZ},
     BookTitle = {4th IEE International Workshop on Discrete Event Systems},
     Pages = {385--390},
     Address = {Cagliari, Italie},
     Month = {August},
     Year = {1998}
  }
  

Control of Symbolic Discrete Event Systems (synchronous paradigm)

• G. Delaval, H. Marchand and E. Rutten, Contracts for Modular Discrete Controller Synthesis Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2010, Pages 57-66, Stockholm, Sweden, April 2010.( Abstract | Bibtex)
  We describe the extension of a reactive programming language with a behavioral contract construct. It is dedicated to the programming of reactive control of applications in embedded systems, and involves principles of the supervisory control of discrete event systems. Our contribution is in a language approach where modular discrete controller synthesis (DCS) is integrated, and it is concretized in the encapsulation of DCS into a compilation process. From transition system specifications of possible behaviors, DCS automatically produces controllers that make the controlled system satisfy the property given as objective. Our language features and compiling technique provide correctness-by-construction in that sense, and enhance reliability and verifiability. Our application domain is adaptive and reconfigurable systems: closed-loop adaptation mechanisms enable flexible execution of functionalities w.r.t. changing resource and environment conditions. Our language can serve programming such adaption controllers. This paper particularly describes the compilation of the language. We present a method for the modular application of discrete controller synthesis on synchronous programs, and its integration in the BZR language. We consider structured programs, as a composition of nodes, and first apply DCS on particular nodes of the program, in order to reduce the complexity of the controller computation; then, we allow the abstraction of parts of the program for this computation; and finally, we show how to recompose the different controllers computed from different abstractions for their correct co-execution with the initial program. Our work is illustrated with examples, and we present quantitative results about its implementation.
  @InProceedings{delaval10a,
     Author = {Delaval, G. and Marchand, H. and Rutten, E.},
     Title = {Contracts for Modular Discrete Controller Synthesis},
     BookTitle = {Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2010},
     Pages = {57--66},
     Address = {Stockholm, Sweden},
     Month = {April},
     Year = {2010}
  }
• H. Marchand, P. Bournai, M. Le Borgne, P. Le Guernic, Synthesis of Discrete-Event Controllers based on the Signal Environment, Discrete Event Dynamic System: Theory and Applications, 10(4):325-346, October 2000. (Abstract | Bibtex)
  In this paper, we present the integration of controller synthesis techniques in the Signal environment through the description of a tool dedicated to the incremental construction of reactive controllers. The plant is specified in Signal and the control synthesis is performed on a logical abstraction of this program, named polynomial dynamical system (PDS) over Z/3Z= {-1,0,+1}. The control of the plant is performed by restricting the controllable input values with respect to the control objectives. These restrictions are obtained by incorporating new algebraic equations into the initial system. This theory sets the basis for the verification and the controller synthesis tool, Sigali. Moreover, we present a tool developed around the Signal environment allowing the visualization of the synthesized controller by an interactive simulation of the controlled system. In a first stage, the user specifies in Signal both the physical model and the control objectives to be ensured. A second stage is performed by the Signal compiler which translates the initial Signal program into a PDS, and the control objectives in terms of polynomial relations/operations. The controller is then synthesized using Sigali. The result is a controller coded by a polynomial and then by a Ternary Decision Diagram (TDD). Finally, in a third stage, the obtained controller and some simulation processes are automatically included in the initial Signal program. It is then sufficient for the user to compile the resulting Signal program which generates executable code ready for simulation. Different academic examples are used to illustrate the application of the tool.
  @article{marchand00c,
     Author = {Marchand, H. and Bournai, P. and Le Borgne, M. and Le Guernic, P.},
     Title = {Synthesis of Discrete-Event Controllers based on the Signal Environment},
     Journal = {Discrete Event Dynamic System: Theory and Applications},
     Volume = {10},
     Number = {4},
     Pages = {325--346},
     Month = {October},
     Year = {2000}
  }
  

• H. Marchand, M. Samaan, Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology, IEEE Transaction on Software Engineering, 26(8):729-741, August 2000. (Abstract | Bibtex)
  In this paper, we describe the incremental specification of a power transformer station controller using a controller synthesis methodology. We specify the main requirements as simple properties, named control objectives, that the controlled plant has to satisfy. Then, using algebraic techniques, the controller is automatically derived from these set of control objectives. In our case, the plant is specified at a high level, using the data-flow synchronous Signal language and then by its logical abstraction, named polynomial dynamical system. The control objectives are specified as invariance, reachability, ... properties, as well as partial order relations to be checked by the plant. The control objectives equations are synthesized using algebraic transformations.
  @article{marchand00d,
     Author = {Marchand, H. and Samaan, M.},
     Title = {Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology},
     Journal = {IEEE Transaction on Software Engineering},
     Volume = {26},
     Number = {8},
     Pages = {729--741},
     Month = {August},
     Year = {2000}
  }
  

• H. Marchand, M. Le Borgne, The Supervisory Control Problem of Discrete Event Systems using polynomial Methods, Research Report Irisa, No 1271, October 1999. (Abstract | Bibtex)
  This paper regroups various studies achieved around polynomial dynamical system theory. It presents the basic algebraic tools for the study of this particular class of discrete event systems. The polynomial dynamical systems are defined by polynomial equations over Z/3Z. Their study relies on concept borrowed from elementary algebraic geometry: varieties, ideals and morphisms. They are the basic tools that allow us to translate properties or specifications from a geometric description to suitable polynomial computations. In this paper, we more precisely describe the controller synthesis methodology. We specify the main requirements as simple properties, named control objectives, that the controlled plant has to satisfy.The plant is specified as a polynomial dynamical system over Z/3Z. The control of the plant is performed by restricting the controllable input values to values suitable with respect to the control objectives. This restriction is obtained by incorporating new algebraic equations into the initial polynomial dynamical system, which specifies the plant. Various kind of control objectives are considered, such as ensuring the invariance or the reachability of a given set of states, as well as partial order relation to be checked by the controlled plant.
  @TechReport{marchand99b,
     Author = {Marchand, H. and Le Borgne, M.},
     Title = {The Supervisory Control Problem of Discrete Event Systems using polynomial Methods},
     Number = {1271},
     Institution = {Irisa},
     Month = {October},
     Year = {1999}
  }
  

• H. Marchand, S. Pinchinat, Supervisory Control Problem using Symbolic Bisimulation Techniques, in 2000 American Control Conference, Pages 4067-4071, Chicago, Illinois, USA, June 2000. (Abstract | Bibtex)
  In this paper, we present methods for solving the basic Supervisory Control Problem (SCP) using algorithms based on bisimulation techniques. Barrett and Lafortune first presented the relations between bisimulation and controllability and provided algorithms for solving the SCP. We efficiently solve the same problem using Intensional Labeled Transition System (ILTS), an implicit representation of automaton, relying on algebraic methods.
  @InProceedings{marchand00a,
      Author = {Marchand, H. and Pinchinat, S.},
      Title = {Supervisory Control Problem using Symbolic Bisimulation Techniques},
      BookTitle = {2000 American Control Conference},
      Pages = {4067--4071},
      Address = {Chicago, Illinois, USA},
      Month = {June},
      Year = {2000}
  }
  

Discrete control synthesis applied to control systems programming

• E. Rutten, H. Marchand, Automatic Generation of Safe Handlers for Multi-Task Systems, Journal of Embedded Computing, 3(4):255-276, 2009. ( Abstract | Bibtex )
  We are interested in the programming of real-time control systems, such as in robotic, automotive or avionic systems. They are designed with multiple tasks, each with multiple modes. It is complex to design task handlers that control the switching of activities in order to insure safety properties of the global system. We propose a model of tasks in terms of transition systems, designed especially with the purpose of applying existing discrete controller synthesis techniques. This provides us with a systematic methodology, for the automatic generation of safe task handlers, with the support of synchronous languages and associated tools for compilation and formal computation.
  @article{rutten09,
      Author = {Rutten, Eric and Marchand, Hervé},
      Title = {Automatic generation of safe handlers for multi-task systems},
      Journal = {Journal of Embedded Computing},
      Volume = {3},
      Number = {4},
      Pages = {255--276},
      Year = {2009}
  }
  

• H. Marchand, E. Rutten, Managing multi-mode tasks with time cost and quality levels using optimal discrete control synthesis, in 14th Euromicro Conference on Real-Time Systems (ECRTS'02), June 2002. (Abstract | Bibtex)
  Real-time control systems are complex to design, and automation support is important. We are interested in systems with multiple tasks, each with multiple modes, implementing a functionality with different levels of quality (e.g., computation approximation), and cost (e.g., computation time, energy). It is complex to control the switching of modes in order to insure properties like bounding cost while maximizing quality. We outline a technique for the automatic generation of such controllers involving an automaton-based formal model, and using optimal discrete control synthesis.
  @InProceedings{marchand02b,
     Author = {Marchand, H. and Rutten, E.},
     Title = {Managing multi-mode tasks with time cost and quality levels using optimal discrete control synthesis},
     BookTitle = {14th Euromicro Conference on Real-Time Systems (ECRTS'02)},
     Month = {June},
     Year = {2002}
  }
  

• H. Marchand, M. Samaan, Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology, IEEE Transaction on Software Engineering, 26(8):729-741, August 2000. (Abstract | Bibtex )
  In this paper, we describe the incremental specification of a power transformer station controller using a controller synthesis methodology. We specify the main requirements as simple properties, named control objectives, that the controlled plant has to satisfy. Then, using algebraic techniques, the controller is automatically derived from these set of control objectives. In our case, the plant is specified at a high level, using the data-flow synchronous Signal language and then by its logical abstraction, named polynomial dynamical system. The control objectives are specified as invariance, reachability, ... properties, as well as partial order relations to be checked by the plant. The control objectives equations are synthesized using algebraic transformations.
  @article{marchand00d,
     Author = {Marchand, H. and Samaan, M.},
     Title = {Incremental Design of a Power Transformer Station Controller using Controller Synthesis Methodology},
     Journal = {IEEE Transaction on Software Engineering},
     Volume = {26},
     Number = {8},
     Pages = {729--741},
     Month = {August},
     Year = {2000}
  }
  

Verification and Bisimulation Techniques (synchronous paradigm)

• H. Marchand, E. Rutten, M. Le Borgne, M. Samaan, Formal Verification of programs specified with SIGNAL : Application to a Power Transformer Station Controller, Science of Computer Programming, 41(1):85-104, August 2001. ( Abstract | Bibtex ) (see also AMAST'96 )
  We present a formal specification and verification of the automatic circuit-breaking behavior of an electric power transformer station, using the synchronous approach to reactive real-time systems implemented by the data-flow language Signal. Synchronous languages have a mathematical model that supports the various phases of the development of a control system: specification, verification, simulation, code generation, and implementation. The complex hierarchical, state-based and preemptive behavior of the power station controller is specified in Signalgti, an extension of Signal with notions of time intervals and preemptive tasks. To validate the specification, a graphical simulator is generated using Signal's execution environment, and the required behaviour is proven to be satisfied, using its proof method.
  @article{marchand01a,
      Author = {Marchand, H. and Rutten, E. and Le Borgne, M. and Samaan, M.},
      Title = {Formal Verification of programs specified with SIGNAL : Application to a Power Transformer Station Controller},
      Journal = {Science of Computer Programming},
      Volume = {41},
     Number = {1},
      Pages = {85--104},
      Month = {August},
      Year = {2001}
  }
  

• E. Marchand, E. Rutten, H. Marchand, F. Chaumette, Specifying and verifying active vision-based robotic systems with the Signal environment, Int. Journal of Robotics Research, 17(4):418-432, April 1998. ( Abstract | Bibtex )
Active vision-based robot design involves a variety of techniques and formalisms, from kinematics to control theory, signal processing and computer science. The programming of such systems therefore requires environments with many different functionalities, in a very integrated fashion in order to ensure consistency of the different parts. In significant applications, the correct specification of the global controller is not simple to achieve, as it mixes different levels of behavior, and must respect properties. In this paper we want to advocate the use of a strongly integrated environment able to deal with the design of such systems from the specification of both continuous and discrete parts down to the verification of dynamic behavior. The synchronous language signal is used here as a candidate integrated environment for the design of active vision systems. Our experiments show that signal, while not being an environment devoted to for robotics (but more generally dedicated to control theory and signal processing), presents functionalities and a degree of integration that are relevant to the safe design of active vision-based robotics system
@article{Marchand98c,
    Author = {Marchand, E. and Rutten, E. and Marchand, H. and Chaumette, F.},
    Title = {Specifying and verifying active vision-based robotic systems with the Signal environment},
    Journal = {Int. Journal of Robotics Research},
    Volume = {17},
    Number = {4},
    Pages = {418--432},
    Publisher = {SAGE},
    Month = {April},
    Year = {1998}
}


• A. Benveniste, P. Caspi, P. Le Guernic, H. Marchand, J.P. Talpin, S. Tripakis, A Protocol for Loosely Time-Triggered Architectures, in Embedded Software Conference (EMSOFT '02), LNCS, Volume 2491, Pages 252-265, Grenoble, France, October 2002. ( Abstract | Bibtex )
  A distributed real-time control system has a time-triggered nature, just because the physical system for control is bound to physics. Loosely Time-Triggered Architectures (ltta) are a weaker form of the strictly synchronous Time-Triggered Architecture proposed by Kopetz, in which the different periodic clocks are not synchronized, and thus may suffer from relative offset or jitter. We propose a protocol that ensures a coherent system of logical clocks on the top of ltta, and we provide several proofs for it, both manual and automatic, based on synchronous languages and associated model checkers. We briefly discuss how this can be used for correct deployment of synchronous designs on an ltta.
  @InProceedings{benveniste02a,
      Author = {Benveniste, A. and Caspi, P. and Le Guernic, P. and Marchand, H. and Talpin, J.P. and Tripakis, S.},
      Title = {A Protocol for Loosely Time-Triggered Architectures},
      BookTitle = {Embedded Software Conference (EMSOFT '02)},
      Volume = {2491},
      Pages = {252--265},
      Series = {LNCS},
      Address = {Grenoble, France},
      Month = {October},
      Year = {2002}
  }
  

• S. Pinchinat, H. Marchand, Symbolic Abstractions of Automata, in Proc of 5th Workshop on Discrete Event Systems, WODES 2000, Pages 39-48, Ghent, Belgium, August 2000. ( Abstract | Bibtex )
  We describe the design of abstraction methods based on symbolic techniques: classical abstraction by state fusion has been considered. We present a general method to abstract automata on the basis of a state fusion criterion, derived from e.g. equivalence relations (such as bisimulation), partitions, ... We also introduce other kinds of abstraction, falling into the category of abstraction by restriction: in particular, we study the use of the controller synthesis methodology to achieve the restriction synthesis.
  @InProceedings{pinchinat00a,
      Author = {Pinchinat, S. and Marchand, H.},
      Title = {Symbolic Abstractions of Automata},
      BookTitle = {Proc of 5th Workshop on Discrete Event Systems, WODES 2000},
      Pages = {39--48},
      Address = {Ghent, Belgium},
      Month = {August},
      Year = {2000}
  }