Ecole Centrale de Lille, France, du 16 au 18 novembre 2011
Site menu:
Trois orateurs invités à MSR'11
Emmanuel Arbaretier, APSYS
- Titre de l'exposé : Enjeux Industriels pour le Health Management System
- Résumé de l'exposé : Les industriels sont conscients d’avoir la possibilité d’utiliser leur information de conception pour développer des applicatifs embarqués de :
- gestion des modes opérationnels
- gestion des modes dégradés
- diagnostic intégré
- prognostic intégré
- maintenance conditionnelle
- « health management »
Toutes ces applications « basées sur la modélisation » et bien plus sur l’exploitation en temps réel de ces modèles et de la prise en compte de mesures ou signaux avant coureurs communiqués par des mécanismes de détection ou de transmission d’états physiques ou codes défauts sous forme analogique ou numérique, et actualisés quasiment en temps réel, impliquent la mise en œuvre d’un processus qui adresse de nombreuses difficultés :
- quel est l’effort de modélisation nécessaire et d’actualisation ou gestion de configuration associé ?
- comment transposer la connaissance physique et technologique des industriels en modèles répondant à des règles formelles et sémantiques bien précises ?
- où trouver la totalité des informations physiques ?
- comment rentabiliser la processus de gestion de ces informations et en particulier concernant la gestion de configuration des informations par rapport aux produits et systèmes concernés ?
- quel est le « business model » de l’ingénierie des modèles ? Est-ce un enjeu de niveau de détail ou de granularité ?
- comment se pose la problématique d’optimum économique pour l’instrumentation des produits / systèmes en termes de systèmes de surveillance et détection ?
- comment gérer la sous-traitance, les « COTS » et l’utilisation de modèles en intégrant les informations associées à supposer qu’on puisse y avoir accès ?
Ces problématiques seront illustrées par des cas concrets qui situeront ces questions scientifiques sur le champ des applications industrielles.
- Biographie de l'orateur : Emmanuel Arbaretier est responsable du pôle d'activité logiciels
depuis janvier 2004 chez APSYS, filiale du groupe EADS, spécialisée dans l'expertise et le conseil en management des risques pour des industries de secteurs tels que l'aéronautique et l'espace, le ferroviaire, le maritime, l'automobile, le
nucléaire, l'énergie, la pétrochimie et le Gaz. Auparavant, il a travaillé sur le soutien logistique intégré au
sein de la division Système Défense Contrôle de THOMSON – CS de 1985 à 1987. Ensuite, il a occupé les postes de
Responsable Recherche et Développement puis de Directeur Général Adjoint de la société SOFRETEN. Depuis 26 ans,
il participe à plusieurs projets sur des problématiques de sûreté de fonctionnement, soutien logistique intégré,
bases de données logistiques, diagnostic, ingénierie système et fiabilité logicielle. Il a collaboré avec plusieurs
acteurs industriels parmi lesquels Aerospatiale, Matra Defense, Alcatel, PSA. Il est diplômé de l'Ecole Centrale
de Paris.
- Titre de l'exposé : Modélisation synchrone de systèmes complexes
- Résumé de l'exposé : Le projet intégré européen ASSERT (2004-08) a concerné une
méthodologie de développement d'applications embarquées,
notamment dans le domaine spatial (lanceurs et satellites). Dans
l'approche proposée, l'architecture matérielle et logicielle
d'une application est décrite formellement au moyen d'un
langage de description d'architectures (ADL), et les composants
logiciels sont développés indépendamment de cette architecture.
Ce développement séparé du logiciel et de l'architecture support
pose le problème de la validation précoce du système global.
Dans cet exposé, nous présenterons une solution consistant à
traduire automatiquement l'architecture en un modèle exécutable,
pour permettre la simulation et la validation conjointe avec le
logiciel d'application. Spécifiquement, nous considérons le
cas où l'architecture est décrite dans le langage AADL, et où
les composants logiciels sont développés en Scade. Nous montrons
comment traduire automatiquement la description de l'architecture
en un modèle synchrone indéterministe, auquel les composants
logiciels peuvent être intégrés. On obtient ainsi un modèle
synchrone intégré, qui peut être simulé et validé avec les
outils de la programmation synchrone, avant même que l'architecture
d'implantation soit disponible. Cette approche est illustrée
par une étude de cas extraite d'un système spatial réel.
- Biographie de l'orateur : Nicolas Halbwachs est directeur de recherche au CNRS. Il a
été l'un des fondateurs de la programmation synchrone des
systèmes réactifs. Avec Paul Caspi, il a défini le langage
"flot-de-données" synchrone Lustre, qui est le noyau de l'atelier
industriel Scade, utilisé dans le monde entier pour la conception
des logiciels embarqués. Ce succès leur a valu en 2004 le Prix
Monpetit de l'Académie des Sciences. Nicolas Halbwachs a mené
d'autre part des recherches en analyse statique de programmes
par interprétation abstraite. Il est à l'origine d'une méthode,
devenue classique, de découverte de relations linéaires invariantes
entre les variables numériques d'un programme. Ses travaux les plus
récents concernent l'analyse de programmes manipulant des tableaux.
Depuis 2007, il est directeur du Laboratoire Verimag à Grenoble.
- Titre de l'exposé : Synthèse automatique à partir de spécifications écrites dans une extension temps-réel de LTL
- Résumé de l'exposé : Dans cet exposé, nous montrerons que plusieurs problèmes centraux de la théorie des automates qui, habituellement, exigent la déterminisation d'automates sur mots infinis peuvent être résolus sans cette étape couteuse.
Nous montrerons en particulier comment le problème de la synthèse automatique à partir de spécifications écrites en logique temporelle linéaire (LTL) peut être résolu sans utiliser les automates déterministes avec condition de parité. Cette nouvelle solution repose sur le raffinement des méthodes "Safraless" (qui évitent la construction de Safra) proposées par Vardi, Kupferman et Schewe. Nous montrerons également comment cet algorithme peut être implémenté de manière efficace grâce à une structure de donnée symbolique dédiée et de manière compositionnelle. Ce nouvel algorithme permet de traiter des spécifications de systèmes réactifs d'intérêt pratique de manière complètement automatique.
Ces techniques peuvent également être étendues à des formalismes pour les spécifications temps-réels. Nous montrerons en particulier comment résoudre le problème de la synthèse pour une extension temps-réel de la logique LTL.
- Biographie de l'orateur : Jean-François Raskin a obtenu sa thèse de doctorat en 1999 à l'Université de Namur (Belgique). Il a ensuite effectués des séjours post-doctoraux à l'Université de Californie à Berkeley et au Max-Planck pour l'Informatique à Saarbrücken. Il est actuellement professeur à l'Université Libre de Bruxelles où il dirige un groupe de recherche en vérification et synthèse assistées par ordinateur. Il est l'auteur ou le co-auteur d'environ 90 papiers de recherche dans les domaines de la vérification assistée par ordinateur et de l'informatique théorique. (http://www.ulb.ac.be/di/ssd/jfr)
