Site menu:



Quatre orateurs invités à MSR2017

Hervé MARCHAND
INRIA Rennes-Bretagne Atlantique, France

Biographie de l'orateur ... Biographie de l'orateur


Hervé Marchand est un ancien étudiant de l’université de rennes 1 en mathématiques. Son doctorat (soutenu en 1997) se concentre sur le contrôle de systèmes synchrones basé sur le langage Signal. Après une année de post-doc auprès de Stéphane Lafortune sur le contrôle des SED avec coûts, il se consacre de manière générale à l’'analyse des SED portant sur le sur le diagnostic, la vérification et le contrôle de ceux-ci. Depuis depuis 1988, il est chercheur Inria dans l ‘équipe Sumo comme chercheur Inria (après un passage par EP-ATR, puis Vertecs), Ces principaux domaines de recherche recouvrent la vérification, le diagnostic et le contrôle des SED avec une emphase ces dernières années sur les systèmes infinis. Actuellement membre du comité de pilotage de MSR depuis 4 ans, Hervé Marchand est membre depuis 6 ans du comité IFAC sur les SED et systèmes hybrides et a été « associate editor » de transaction Automatic and control durant 4 ans.



Contribution to the Analysis of Discrete Event Systems (slides)

Cet exposé remplace celui de Stéphane Lafortune, annulé suite à un empêchement
Mercredi 15 novembre, 9h30 - 10h30


Résumé de l'exposé   : Since the 90's, automatic systems take a growing place into our everyday lives. It might be embedded systems, such as in robotic, automotive or avionic systems, telecommunication or transportation systems or energy services, etc. The presence of such systems offers new possibilities, but the price to pay is the increasing risks of software failures which can have dramatic consequences in terms of human lives or prohibitive costs. Manual validation is expensive, may be impossible for large systems, and is permeable to mistakes. The development of automatic tools serving to analyze or to ensure security/safety has thus become crucial to discover and avoid breaches and mistakes in the development of embedded systems. This talk reports on some of my contributions to formal methods for discrete event systems. More specifically, the following problems are tackled: the diagnosis of discrete event systems for faulty behaviors that can be represented finite automata (these faults can be permanent or transient). A second contribution concerns the automatic control of concurrent systems composed of multiple sub-systems communicating either synchronously or asynchronously by means of fifo channel. In the field of computer security, the third contribution deals with the enforcement and the detection of confidentiality properties (more specifically the notion of opacity) using diagnosis techniques to detect opacity violations or supervisory control theory to restrict the behavior of a system in order to avoid information leakage.

Joseph SIFAKIS
RSD Team, Verimag, France

Biographie de l'orateur ... Biographie de l'orateur


Joseph Sifakis is Emeritus Senior CNRS Researcher at Verimag. His current research interests cover fundamental and applied aspects of embedded systems design. The main focus of his work is on the formalization of system design as a process leading from given requirements to trustworthy, optimized and correct-by-construction implementations. Joseph Sifakis has been a full professor at Ecole Polytechnique Fédérale de Lausanne (EPFL) for the period 2011-2016. He is the founder of the Verimag laboratory in Grenoble, which he directed for 13 years. Verimag is a leading research laboratory in the area of embedded systems, internationally known for the development of the Lustre synchronous language used by the SCADE tool for the design of safety-critical avionics and space applications. In 2007, Joseph Sifakis has received the Turing Award for his contribution to the theory and application of model checking, the most widely used system verification technique today. Joseph Sifakis has had numerous administrative and managerial responsibilities both at French and European level. He has actively worked to reinvigorate European research in embedded systems as the scientific coordinator of the « ARTIST » European Networks of Excellence, for ten years. He has participated in many major industrial projects led by companies such as Airbus, EADS, France Telecom, Astrium, and STMicroelectronics. Joseph Sifakis is a member of the French Academy of Sciences, a member of the French National Academy of Engineering, a member of Academia Europea, a member of the American Academy of Arts and Sciences, and a member of the National Academy of Engineering. He is a Grand Officer of the French National Order of Merit, a Commander of the French Legion of Honor. He has received the Leonardo da Vinci Medal in 2012. Joseph Sifakis has received in 2009 the Award of the Hellenic Parliament Foundation for Parliamentarism and Democracy. He is a commander of the Greek Order of the Phoenix. He has been the President of the Greek Council for Research and Technology for the period February 2014 – April 2016.



Modeling architectures and their properties in BIP

Mercredi 15 novembre, 16h30 - 17h30



Résumé de l'exposé   : Architectures are mechanisms for ensuring global properties characterizing the coordination between components. Using architectures largely accounts for our ability to master complexity and develop systems cost-effectively. In BIP, architectures are generic behavior transformers represented as sets of connectors. They take as arguments typed components and give a composite component. We propose two different ways to describe architectures using respectively imperative and declarative languages. The imperative language, Dynamic BIP uses iterators on component variables and set-of-component variables to describe dynamic architectures. The declarative language is a second order Interaction Logic based on a symbolic representation of connectors. In BIP, architecture properties are architecture styles or patterns that characterize families of architectures sharing common characteristics such as Token-ring and Philter styles. Configuration Logic is a power-set extension of Interaction Logic used to specify architecture styles. We provide theoretical foundations of the above formalisms developed at EPFL and Verimag. We also provide examples illustrating their effective application. We conclude with a discussion on ongoing and future work directions aiming at the implementation and integration of these results in correct-by-construction system design flows.

Serge HADDAD
LSV, ENS Cachan, France

Biographie de l'orateur ... Biographie de l'orateur


Serge Haddad est un ancien élève de l'ENS Cachan en mathématiques. Son doctorat (soutenu en 1987) était consacré à l'analyse des réseaux de Petri de haut-niveau. Depuis il a été successivement maître de conférences de 1988 à 1993 à l'Université Pierre et Marie Curie, puis professeur à l'Université Paris-Dauphine et depuis 2008 à l'ENS Cachan. Ses travaux (qui lui ont valu 5 récompenses en conférence internationale) portent sur la vérification et le contrôle de systèmes à événements discrets présentant des aspects quantitatifs tels que le temps et les probabilités.



Réseaux de Petri discrets et continus : apports réciproques (slides)

Jeudi 16 novembre, 9h00 - 10h00



Résumé de l'exposé   : Dans les années 80, les réseaux de Petri continus (RdPC) ont été introduits d'une part pour remédier à l'explosion combinatoire des réseaux de Petri discrets (RdP) et d'autre part pour modéliser le comportement de systèmes physiques dont l'état est spécifié par des variables continues. Depuis cette époque, différents travaux ont établi que la complexité de la vérification de propriétés comportementales se réduit en passant du modèle discret au modèle continu. Cet exposé consistera en trois parties. Tout d'abord je détaillerai un algorithme polynomial pour l'accessibilité dans les RdPC et survolerai les autres algorithmes polynomiaux pour RdPC. Je montrerai aussi que l'accessibilité est PTIME-complète tandis que l'absence de blocage est coNP-complète. J'étudierai ensuite l'application de ces procédures au problème de couverture des RdP. La couverture est particulièrement appropriée à l'étude de programmes concurrents à mémoire partagée. Cependant sa complexité élevée (EXPSPACE-complète) limite son utilisation pour des problèmes de taille industrielle. Aussi je développerai une nouvelle approche appliquant la couverture des RdPC comme méthode d'élagage d'un algorithme de couverture en arrière. Le point crucial est ici un codage efficace de l'algorithme polynomial en une formule d'un SMT solveur. Finalement je montrerai que ce codage peut aussi être appliqué au problème d'inclusion d'ensembles d'accessibilité de RdPC réduisant ainsi la complexité de EXPTIME à coNP. J'établirai aussi que cette procédure est optimale, i.e. le problème est coNP-complet.

Claudine CHAOUIYA
Instituto Gulbenkian de Ciência, Portugal

Biographie de l'orateur ... Biographie de l'orateur


Claudine Chaouiya a obtenu un Doctorat en Informatique en 1992 à Nice Sophia Antipolis. Après avoir occupé un poste de professeur invité au Brésil puis de Maitre de Conférences en Nouvelle Calédonie, elle a rejoint l'Université d'Aix-Marseille en 1999. C'est à Marseille qu'elle a commencé à s' intéresser aux réseaux biologiques, avec l'idée que ses connaissances de modélisation et analyse de systèmes industriels trouveraient là un champ d' application passionnant. Depuis 2008, elle est en détachement au Portugal, à l'Institut Gulbenkian de Science, où elle dirige sa propre équipe de recherche. Ses travaux sont menés en collaboration étroite avec des biologistes et sont organisés selon deux axes majeurs: la modélisation de processus biologiques et les développements méthodologiques pour une analyse efficaces de ces modèles.



Prolifération, différenciation, mort cellulaire… Comprendre le destin des cellules en modélisant leurs réseaux moléculaires

Vendredi 17 novembre, 9h00 - 10h00


Résumé de l'exposé   : Les processus cellulaires majeurs sont contrôlés par des réseaux d'interactions complexes et hétérogènes, et les dysfonctionnements de ces réseaux sont associés à de nombreuses maladies. Après un bref panorama des approches de modélisation considérées pour aborder ces réseaux, je présenterai le formalisme logique de René Thomas. L'analyse des dynamiques discrètes de ces modèles logiques est particulièrement difficile et pourrait bénéficier des techniques développées par la communauté des automaticiens et informaticiens. Pour illustrer ces défis, je présenterai les travaux de mon équipe sur des méthodes d'analyse qui seront appliquées sur un modèle de la régulation des propriétés adhésives des cellules cancéreuses.

Stéphane LAFORTUNE
Université du Michigan, Ann Arbor, États-Unis

Biographie de l'orateur ... Biographie de l'orateur


Stéphane Lafortune est Professeur au département “Electrical Engineering and Computer Science” à l’université du Michigan, Ann Arbor, EU. Il a obtenu ses diplômes en génie électrique de l’Ecole Polytechnique de Montréal (B.Ing, 1980), l’université McGill (M.Eng, 1982), et l’université de California à Berkeley (PhD, 1986). Lafortune est un “Fellow” de l’IEEE (1999) et de l’IFAC (2017). Ses recherches couvrent tous les aspects des systèmes à événements discrets, incluant la modélisation, le contrôle, le diagnostic et l’optimisation, avec applications aux systèmes d’ordinateurs. Il est co-auteur, avec Christos Cassandras, du livre Introduction to Discrete Event Systems (2e édition, Springer, 2008). Il est Editeur-en-Chef du journal Discrete Event Dynamic Systems: Theory and Applications (Springer).



Contrôle par supervision des systèmes à événements discrets : Rétrospective et Perspectives

Annulé suite à un empêchement


Résumé de l'exposé   : L’année 2017 marque le trentième anniversaire de la publication dans la littérature en automatique des articles de Ramadge et Wonham qui ont introduit la théorie du contrôle par supervision des systèmes à événements discrets modélisés dans le cadre des langages formels et des automates finis. Cette théorie a par la suite été étendue à plusieurs catégories d'architectures de contrôle avec modularité horizontale ou verticale. En parallèle, le domaine des méthodes formelles en informatique a fait des progrès considérables en vérification des systèmes fermés ainsi qu'en synthèse des systèmes réactifs. Récemment, le domaine des méthodes formelles en automatique a pris de l'ampleur, en particulier dans le cadre des systèmes cyber-physiques qui sont abstraits en systèmes discrets soumis à des spécifications en logique temporelle. Nous allons discuter comment ces domaines de recherche sont complémentaires. Nous allons aussi présenter des résultats récents sur la synthèse de contrôleurs et de stratégies d'activation des capteurs pour les systèmes discrets à observation partielle d'événements. Nous allons conclure la présentation avec des perspectives sur les algorithmes pour la synthèse des contrôleurs qui exploitent les méthodes symboliques et les résultats récents dans la technologie des solveurs du problème SAT.