Relations industrielles

Certification de logiciel en Aéronautique

Les constructeurs aéronautiques dans le monde explorent des techniques variées de vérification formelle de correction de logiciels. Bien sûr, les méthodes fondées sur l'exploration exhaustive d'espaces finis d'états sont très utilisées, mais les méthodes utilisant des techniques des outils de démonstration fondé sur des logiques puissantes et des principes de récurrences sont également utilisées pour explorer des domaines mathématiques potentiellement infinis. Par exemple, la NASA fait appel à l'outil PVS (un outil similaire à Coq par ses objectifs) pour vérifier des logiciels.

Pour notre part, nous maintenons des contacts fructueux avec Dassault-Aviation autour de l'action de développement Génie II. Les algorithmes étudiés dans cette entreprise comportent, entre autres, un algorithme de BDD et un algorithme faisant intervenir la cinématique du point. Dans ce thème, nos apports sur les environnements de démonstration ont été particulièrement appréciés pour l'augmentation de productivité qu'ils permettent.

Actuellement, Génie fournit les ressources pour le contrat de Pascal Lequang sur le développement de CtCoq et Dassault Aviation celles pour la thèse d'Antonia Balaa. En outre, nous fournissons un conseil pour la vérification formelle du générateur de code Scade de Vérilog effectuée chez Dassault Aviation, en collaboration avec Joëlle Despeyroux.

Dyade, France

Nous maintenons des contacts avec les équipes de Dyade sous deux formes différentes. D'une part, les travaux sur l'affichage de données structurées ont profité de notre collaboration dans l'activité Dyade Koala. Dans le cadre du prolongement de cette action de collaboration, nous espérons étendre ces travaux pour mieux maîtriser l'intégration de nos outils avec ceux du WEB. D'autre part, l'une des actions Dyade, l'action VIP, a fait dans le passé un usage important de Coq. Dans le futur, nous espérons que nos outils seront également utilisés par cette action, avec laquelle nous avons des contacts réguliers.

Vérilog, France

Vérilog développe un environnement pour la spécification, la simulation, le test, et la génération de code pour des applications de contrôle-commande. Le langage utilisé, appelé Scade, est issu de Lustre et les vérifications formelles fournies sont fondées sur des outils de model-checking, qui effectuent automatiquement l'exploration de grands espaces finis d'états. Ces outils sont très efficaces mais ne s'appliquent qu'aux cas particuliers où il est praticable d'explorer tous les états accessibles par un logiciel. Au-delà des vérifications de programmes écrits en Scade, se pose également la question de vérifier le générateur de code du langage Scade. Nous sommes indirectement en contact avec Vérilog sur cette question, par l'intermédiaire de Dassault Aviation (en collaboration avec Joëlle Despeyroux).

Prover Technology, Suède

Durant l'été 98 dans le cadre d'un stage, Pierre Letouzey a certifié une implantation de la méthode de Stålmarck pour la vérification de tautologie booléenne. Ce travail a intéressé les gens de Prover Technology AB qui commercialise un outil fondé sur cette méthode.