Dassault Système
Dassault Systèmes (DS) est un éditeur de logiciel spécialisé dans les outils de conception
assistée par ordinateur. La gamme de produits de la société est étendue et comprend 7
marques de produits interconnectés pour former une plateforme technique. La société est le
leader de son marché.
La marque la plus connue de l'entreprise est la marque CATIA, CATIA est composée de 200
produits logiciels qui ensemble composent la solution leader pour la création de produit en
3D. La société a développé en interne, et suite à l'acquisition de Geensoft, une suite d'outils
pour la conception de l'électronique embarquée qui utilise les principes de Model Based
Engineering dans lesquels différents niveaux de modèles sont réalisés pour définir les
fonctions, puis les solutions techniques avant d'être utilisés pour réaliser le logiciel, les
configurations et enfin les bancs de tests des solutions électroniques embarquées. Un de ces
produits est ControlBuild qui est utilisé dans le transport et l'énergie pour modéliser et
générer le code d'applications à forte contrainte de sûreté de fonctionnement.
Dans le cadre d'autres projets de R&D, en particulier le projet TESTEC et le projet EDONA,
Geensoft a expérimenté des techniques de génération de jeux de test et l'intégration de ces
techniques aux outils de conception ; ces expérimentations ont abouti à l'intégration de
modules spécialisés dans les outils ControlBuild et AutosarBuilder. Les équipes R&D de DS
sur les sujets systèmes sont de 100 personnes environ et en croissance rapide.
EDF
EDF Recherche & Développement a pour mission de préparer ce que sera le monde
énergétique de demain. Résoudre les problèmes quotidiens dans l'exercice de nos métiers,
imaginer l'avenir du paysage énergétique et contribuer à conforter la position du Groupe
EDF sur la place internationale, tels sont les enjeux. Au sein d'EDF R&D, le département
Simulation et Traitement de l'information pour les Procédés industriels a pour mission
d'améliorer la sûreté, la disponibilité et la productivité des moyens de production du Groupe
EDF (centrales nucléaires, hydrauliques, thermiques, renouvelables), de maîtriser leurs coûts
de maintenance et d'accroître leur durée de vie. Le département est organisé en cinq groupes
d'études dont le groupe Contrôle-Commande qui a pour mission d'être une source de
propositions innovantes dans les domaines du contrôle-commande et de l'informatique
industrielle utilisée dans les moyens de production. Il contribue à la maîtrise de la durée de
vie des systèmes de contrôle-commande et à la compétitivité des moyens de production, en
maîtrisant leur sûreté de fonctionnement. Dans le domaine des tests de validation, EDF R&D
possède une expertise forte tant au niveau méthodologique que réalisation. Elle la met en
oeuvre en particulier dans le cadre de nouveaux projets de systèmes de contrôle-commande
(nucléaire N4, EPR, Chine) et lors de projets de rénovation des systèmes existants.
EDF R&D a investigué, à des fins exploratoires, la complémentarité des vérifications
formelles et des générations de test automatisées, notamment par le développement d'un
prototype Testminator pour les systèmes logiques non bouclés. EDF R&D développe par
ailleurs des simulateurs de parties opératives pour la validation fonctionnelle du contrôle-commande et maîtrise les techniques d'analyse statique de codes pour la vérification des
logiciels critiques. EDF R&D participe aussi au projet Usine Logicielle du Pôle de
compétitivité "System@tic", dans le cadre du sous-projet MODRIVAL pour la validation des
systèmes (génération de tests à partir de spécifications en UML) et les outils d'analyse de
logiciels.
I3S
L'I3S a une grande expérience dans la programmation par contraintes et applique ces techniques
depuis plus de 10 ans à la génération de jeux de test logiciels et la vérification de programmes.
Gilles Bernot, qui a rejoint l'I3S récemment, a été un des pionniers dans l'utilisation des
méthodes formelles pour le test et la vérification. Dans la continuité de ces travaux, son équipe
est devenue moteur dans l'application des méthodes formelles aux systèmes biologiques
complexes. L'outil SMBioNet développé dans ce cadre met en oeuvre des techniques
d'énumération parcimonieuse qu'on se propose d'appliquer au logiciel.
Une partie de travaux de l'I3S dans ce domaine a été menée dans le cadre du projet RNTL
DANOCOPS, l'ACI V3F et les projets ANR CAVERN et TESTEC. C'est dans le cadre de ce
dernier projet que nous avons commencé à travailler avec les partenaires du projet qui est
soumis; c'est à dire appris à dialoguer avec des automaticiens et appris à connaître les problèmes
des industriels comme ceux de Geensys et EDF R&D.
Les enseignants‑chercheurs de l'I3S impliqués dans ce projet totalisent une vingtaine de
publications internationales (dont plus de 10 revues) dans des domaines directement liés à leur
contribution dans ce projet.
INRIA Rennes - VerTeCS
L'équipe-projet INRIA VerTeCs possède une grande expertise dans la conception de
techniques et outils pour la vérification, le contrôle et la génération automatique de tests de
conformité pour des systèmes réactifs. Ses recherches se fondent sur des modèles formels et
des techniques de vérification. Ayant une renommée internationale en génération
automatique de tests, l'équipe VerTeCs s'est intéressée depuis plusieurs années à la
génération symbolique de tests de conformité pour des modèles de spécifications de type
automates étendus, en évitant l'énumération des données a priori non bornées. Plus
récemment, elle a étudié la génération automatique de test pour différentes classes
d'automates temporisés, avec ou sans données, et notamment dans le cadre du projet ANR
TESTEC en considérant un modèles d'automates temporisés à flots de données (en
collaboration avec le LaBRI). L'équipe Vertecs possède également des compétences solides
en vérification qualitatives et quantitatives sur les modèles temporisés. Elle mène aussi des
recherches sur la combinaison méthodologique et technique de la vérification et du test.
L'équipe collabore sur ces thèmes avec plusieurs laboratoires en Europe, en particulier dans
le cadre du réseau Artist et dans le cadre d'une équipe associée au Brésil. Les membres de
l'équipe Vertecs intervenant dans le projet VACSIM sont auteurs d'une bonne vingtaine de publications dans des conférences internationales et quelques articles de journaux sur les
thèmes dans lesquels elle se propose d'intervenir dans le cadre de ce projet.
Labri
Au niveau du LaBRI (UMR 5800), les thèmes "modélisation et vérification" et "test de
systèmes informatisés" sont concernés par le projet VACSIM. Les membres de ces thèmes ont
une longue expérience dans la modélisation et la validation de systèmes. Entre autres, ces
travaux s'appliquent dans le cadre de systèmes embarqués, temps-réel ou protocoles de
communication. Ils ont étudié la vérification des systèmes infinis (notamment, les systèmes
communicants d'une part, et les systèmes temporisés d'autre part) et différents types de test
(conformité, interopérabilité, robustesse) dans le cadre de projets nationaux (Calife-RNRT,
Platonis-RNRT, Averroes-RNTL, Persee-ACI, SpaCIFY-ANR, Webmov-ANR, Averiss-ANR,
Dots-ANR, Testec-ANR) et de contrats de recherche avec des industriels (BULL, EDF,
Airbus, RATP, France Telecom R&D, THALES). Les outils McScM et TGSE ont été
développés. Le LaBRI a notamment déjà collaboré avec l'ensemble des partenaires du projet
VACSIM au travers du projet ANR TESTEC. Cette collaboration a permis la mise au point de
modèles et méthodes de test pour systèmes temps-réel à flot de données. En effet, grâce à son
expérience dans le domaine des automates temporisés, l'équipe du LaBRI a contribué avec
l'INRIA Rennes au développement d'algorithmes de génération de tests pour une classe de
systèmes proposés par les partenaires industriels (EDf - Geensoft). La particularité de ces
travaux était de proposer une nouvelle modélisation concise et adaptée pour ce genre de
systèmes, et de prendre en compte l'aspect symbolique du temps pour limiter l'explosion
combinatoire dans la production de tests. Ces travaux ont été publiés dans des conférences
internationales. Ce projet a aussi donné lieu à des travaux sur la complémentarité entre le
test structurel et le test à base de modèles. Ces derniers sont toujours en cours.
Lurpa
La thématique générale des recherches de l'équipe ISA (Ingénierie des Systèmes
Automatisés) du LURPA : Commande sûre des systèmes à événements discrets (Dependable
Control of Discrete event Systems), s'insère bien dans les préoccupations des axes 2 et 4 de
l'AAP Ingénierie Numérique & Sécurité. Cette thématique, qui vise à développer des
méthodes, techniques et outils permettant d'améliorer la conception, l'implantation et
l'exploitation des systèmes de commande majoritairement discrets, afin d'accroître la s&ucric;reté
de fonctionnement, constitue une proposition originale de l'équipe qui a été reconnue par
l'IFAC (International Federation of Automatic Control), notamment sous la forme d'une
série de workshops Dependable Control of Discrete event Systems (DCDS).
Cette équipe a, d'autre part, une longue expérience de la collaboration avec des équipes
relevant de l'informatique ou des mathématiques appliquées, dans le cadre de l'Institut
Farman (FR 3311), où nous avons été partenaires de plusieurs projets de recherche
pluridisciplinaire avec le LSV (UMR 8643) et le CMLA (UMR 8536).
Enfin, un certain nombre des recherches s'effectuent dans le cadre de projets de recherche
coopérative avec les centres de R&D de grandes entreprises (Alstom Power, EADS
Innovation Works, EDF R&D) qui concoivent et/ou exploitent des systèmes très critiques.