Ce projet rassemble des laboratoires français dont les
équipes sont reconnues dans les domaines des preuves formelles et de
la génération de tests temporisés.
France Télécom R&D coordonnera le projet.
Les partenaires se connaissent bien pour avoir
travaillé ensemble dans le projet RNRT Calife (se terminant
fin 2002), dans une action FORMA (CNRS/MNRT/DGA),
des contrats de recherche bilatéraux avec France Télécom
ainsi que diverses instances académiques françaises
(comme le GDR programmation) ou internationales
(comme les projet européens TYPES et VERIFICARD).
A titre d'exemples concrets,
le modèle des p-automates est issu d'un travail en commun
du LSV, du LaBRI, de FTR&D et du LRI ;
plusieurs applications (ABR, PIM, PGM) ont été traités
de concert par le LRI, FTR&D et le LSV ;
CRIL-Technology a réalisé des interfaces entre un outil graphique
et les outils de vérification des autres partenaires (LSV, LRI, LaBRI),
en collaboration étroite avec ces derniers ;
Le LORIA et le LRI ont réalisé une interface entre les systèmes Coq et Elan,
permettant de démontrer des égalités de manière sûre et efficace ;
le LRI collabore avec FTR&D et avec le LSV pour la mise au point
de nouvelles tactiques ;
et bien entendu le LRI et LogiCal collaborent
de longue date sur le système Coq.
Notons que l'expérience du projet Calife a permis de valider l'idée qu'un
système généraliste puisse être utilisé de manière efficace dans un
domaine d'application spécialisé au moyen de bibliothèques appropriées
et d'interfaces avec des outils spécialisés.
France Télécom R & D
France Télécom R & D (FTR&D),
centre de recherche de France Télécom, a travaillé depuis
une vingtaine d'années sur les techniques formelles
(spécification, preuve et test), tant sur le plan théorique que pratique.
L'une de ses missions est d'apporter à France Télécom
une expertise au meilleur niveau sur les sciences et techniques
susceptibles
d'améliorer la qualité des services offerts
et d'apporter un avantage compétitif.
Sur le plan de l'utilisation des méthodes formelles,
l'intérêt de FTR&D est de
contribuer au développement de techniques pertinentes
par rapport aux problèmes soulevés en pratique
et bénéficier des avancées réalisées dès que possible.
En particulier disposer de bons concepts et outils pour les systèmes où le
temps et l'utilisation des ressources jouent un rôle important
est un enjeu important des prochaines années.
Le laboratoire TAL (Techniques Avancées pour la construction
de Logiciels) au sein de duquel
est lancé le projet comprend 9 chercheurs à temps plein
sur les méthodes formelles (vérification, test)
et 7 doctorants.
Il a des relations suivies avec de nombreux laboratoires
français et étrangers.
CRIL Technology Systèmes Avancés
PME de 400 personnes, CRIL Technology Systèmes Avancés est une société d'ingénierie et
d'études spécialisée en informatique technique et scientifique et en
télécommunications. CRIL Technology affirme sa stratégie de
développement en consacrant une part importante de son chiffre d'affaires (12 %)
à la recherche et à la technologie. Elle s'appuie dans ce cadre sur une veille
technologique constante et a mis en place une dynamique de l'innovation basée sur la
participation à des projets d'études et de recherche de la communauté
européenne, la présence à des colloques, des partenariats avec des
laboratoires, centres de recherche, écoles et universités.
CRIL Technology travaille sur de nombreux projets relatifs au
développement de logiciels temps réél pour des systèmes critiques et
investit, dans ce cadre et depuis plusieurs années, dans les méthodes
de validation formelle. Son implication dans le projet Calife lui a
permis de développer une interface en logiciel libre et source ouvert,
en collaborant avec les laboratoires français spécialistes du domaine.
LaBRI - Bordeaux
Le LaBRI (Laboratoire Bordelais de Recherche en Informatique) est une
Unité Mixte de Recherche du CNRS (UMR 5800), rattachée au Département
des Sciences pour l'Ingénieur, et dépendant à la fois de l'Université
Bordeaux I et de l'ENSEIRB (Ecole Nationale Supérieure d´Electronique,
Informatique et Radiocommunications de Bordeaux).
Ce laboratoire regroupe des chercheurs du CNRS, des enseignants-chercheurs,
doctorants et post-doctorants répartis sur 5 équipes : Combinatoire et
Algorithmique -·Logique - Langages et Applications - Modélisation,
Vérification et Test de systèmes informatisés - Calcul Parallèle et
Distribué - Image et Son.
Les effectifs actuels sont d'environ 85 enseignants-chercheurs permanents
et 50 chercheurs non permanents.
Sa participation dans ce projet concerne l'équipe MVTsi (Modélisation,
Vérification et Test de systèmes informatisés), dirigée par A. Arnold et
R. Castanet. Cette équipe a centré son activité de recherche sur
l'ingénierie de systèmes complexes et critiques : l'objectif est de
pouvoir les modéliser formellement, effectuer des calculs sur les
modèles (vérification de propriétés, simulation, évaluation qualitative
et quantitative, génération de séquences de test, etc.) et exploiter
les résultats des « calculs », et en particulier les interpréter pour
valider la modélisation et la spécification. Les principaux modèles
étudiés et utilisés sont essentiellement des systèmes à événements
discrets : automates d'états finis, réseaux de Petri, algèbre de Boole,
automates temporisés, processus stochastiques, etc.
En ce qui concerne les applications pratiques, les membres de l'équipe
participent à plusieurs projets de recherche finalisée dans le cadre de
coopérations industrielles (FTR&D, Elf-Aquitaine, IsdF, EdF, etc.).
LORIA - Nancy
Le LORIA, Laboratoire Lorrain de Recherche en Informatique et ses
Applications, est une unité Mixte de Recherche - UMR 7503 - commune au
CNRS, à l'Institut National Polytechnique de Lorraine, à L'INRIA, à
l'Université Henri Poincaré et à l'Université de Nancy 2. Le
Laboratoire regroupe 300 chercheurs, enseignants-chercheurs,
doctorants et post-docs. Le projet implique l'équipe Prothéo et des
membres de l'équipe Calligramme. Le projet Protheo (Contraintes,
Déduction Automatique et Preuves de Propriétés de Logiciels), dirigée
par Claude Kirchner se compose de 6 permanents, 6 doctorants et 5
invités et postdoctorants. Cette équipe est reconnue
internationalement en réécriture, mécanisation du raisonnement et
résolution de contraintes. Elle est l'auteur du système Elan, cadre
formel basé sur le calcul de réécriture, et dont le langage permet
d'exprimer règles et stratégies de calcul ou de déduction et de les
exécuter très efficacement.
Le projet Calligramme, dirigé par Philippe de Groote, se compose de
5 permanents et de 2 doctorants.
Cette équipe est reconnu internationalement en complexité implicite.
Ces deux équipes mènent une politique active de coopération
industrielle (contrats avec la Sollac, le FTR&D, le GIHP-Reims,
Xerox) et bénéficient d'un réseau de coopération internationale
important avec entre autres les universités et centre de recherche du
CWI à Amsterdam, de Munich, de Tel-Aviv, d'Urbana-Champaign, de
Bloomington Indiana, et le centre de recherche SRI-CSL à Menlo Park.
Elles sont par ailleurs partenaires du thème Qualité et Sûreté des
Logiciels développé au LORIA.
L'intérêt des résultats attendus tant sur le plan théorique que sur le
plan pratique concerne d'une part la mise en oeuvre du concept de
réécriture comme cadre formel et pratique pour modéliser, étudier et
rendre exécutable la coopération des procédures de décisions avec les
méthodes de preuve automatiques ou assistées dans le prolongement de
nos travaux sur le concept de déduction modulo. D'autre part, il
concerne le
développement et la mise en oeuvre de résultats de complexité
implicite dans le domaine de la réécriture et de l'extraction de
programme à partir de démonstration
pour aller vers la maîtrise des ressources de calcul et d'espace
mémoire.
PCRI - Saclay
Le PCRI (Pôle commun de recherche en informatique) est une structure
nouvellement créée qui regroupe les équipes du LRI
(un des deux laboratoires en informatique de l'université
Paris Sud, UMR CNRS 8623) du LIX (laboratoire d'informatique de l'école
polytechnique, UMR CNRS 7650) et accueille des projets communs avec l'INRIA
(Institut National de Recherche en Informatique et en Automatique,
Établissement Public Scientifique et Technique, placé sous la double
tutelle du Ministère de la Recherche et du Ministère de l'Industrie).
La proposition implique le projet LogiCal commun à l'INRIA et à
l'université Paris Sud, dont le responsable est Gilles Dowek et
l'équipe Démons (Démonstration et Programmation) du LRI, dirigée par
Chistine Paulin. Ces deux équipes regroupent 13 permanents (dont un
membre du LIX), 15 doctorants, 3 chercheurs post-doctoraux et un
ingénieur.
Le projet LogiCal est à l'origine du développement de l'assistant à la
démonstration Coq. Son expertise est donc naturellement centrée
autour des assistants de preuves, (architecture, langage preuves, ...)
et de leurs utilisations dans la preuve de correction de logiciel et
de matériel. En dehors du projet CALIFE, le projet LogiCal est
impliqué dans le projet Européen VERIFICARD de vérification
d'applications JavaCard et a entamé une collaboration avec une équipe
du laboratoire de recherche NASA-Langley dans le domaine de la
modélisation et vérification d'algorithmes de contrôle aérien.
On compte actuellement plus de 200 utilisateurs de Coq
dans le monde.
L'équipe Démons est internationalement reconnue pour son
expertise en démonstration automatique et tout particulièrement en
réécriture et résolution de contraintes.
Elle développe en particulier le système CiME qui
permet d'effectuer automatiquement des preuves de terminaison de
systèmes de réécriture. Des avancées théoriques significatives ont été
réalisées ces trois dernières années dans la compréhension des
systèmes combinant réécriture et ordre supérieur. Ces résultats devraient
permettre à moyen terme de concevoir de nouvelles architectures
d'assistant de preuve améliorant sensiblement les performances et
l'expressivité des systèmes actuellement sur le marché.
Nous collaborons étroitement avec les différents membres du
projet :
avec CRIL Technology, sur la mise au
point de la traduction des p-automates vers des théories Coq ;
avec France Télécom R&D, dans l'étude des
procédés d'automatisation de preuve et modélisation
d'applications ;
avec le LORIA, sur l'interaction entre calcul (en particulier
réécriture) et déduction;
avec le LSV, sur l'adaptation de techniques de model-checking (abstraction, calcul
d'invariants) à un environnement de preuves interactives sûres.
LSV - Cachan
Le LSV (Laboratoire Spécification et Vérification) est le laboratoire
d'Informatique de l'Ecole Normale Supérieure de Cachan et est associé
au CNRS (UMR 8643). Il regroupe une trentaine de chercheurs,
enseignants-chercheurs, doctorants et post-docs autour du double thème
de la spécification et de la vérification. Le LSV comporte des
spécialistes de différentes facettes de ces domaines (spécification
algébrique, démonstration automatique, model-checking, automates
temporisés, cryptographie, ...).
La recherche au LSV
est centrée sur la vérification de logiciels et systèmes critiques,
ainsi que sur la vérification de la sécurité des systèmes
informatiques. Il mène depuis sa création une politique active de
coopérations industrielles, en particulier dans le cadre de la
spécification et de la vérification de la qualité de service (contrats
avec EDF, Alcatel, France Télécom, Trusted Logic, etc.).
Le LSV à l'ENS Cachan a une longue expérience dans
l'utilisation d'environnements de model-checking
(Uppaal, Hytech) et développe ses propres outils de
model-checking
compositionnel (HCMC).
Le présent projet RNTL s'inscrit
donc parfaitement dans les domaines de compétences du laboratoire.
Organisation du partenariat dans le projet
L'implication des partenaires dans les différents lots
assure que chacun a une vision très large voire globale
de l'ensemble.
Les partenaires sont habitués à collaborer sous forme
d'échanges de chercheurs, de suivis de doctorants,
de participation à des communautés scientifiques communes ou voisines,
séminaires communs, etc.
L'administration du projet s'effectuera à travers des réunions formelles
(2 à 3 par an) et des échanges électroniques.
