Médecine. Transport aérien. Télécommunications. Nucléaire. Automobile... Les ordinateurs jouent un rôle essentiel et sans cesse croissant dans ces secteurs sensibles. Dans ces activités, où le moindre défaut peut se terminer en catastrophe,  la sécurité est primordiale. Cette exigence de fiabilité absolue a conduit au développement de langages de programmation spécifiques et d'outils de vérification ad hoc.

Vlad Rusu (1) s'intéresse à ces systèmes pour lesquels une série d'événements entraîne une série d'actions en retour. Ces programmes réagissent en permanence à leur environnement. On les appelle des systèmes réactifs.  Ils reposent sur ce qu'on nomme les méthodes formelles, c'est à dire des techniques de spécification, de développement et de vérification des software et hardware, basées sur les mathématiques.

La vérification formelle consiste à “prouver un programme ou un logiciel, par rapport à des propriétés elles aussi définies formellement.” Une première approche vise “à poser la correction comme un théorème et à essayer de le prouver... à la main”. Mais la méthode papier-crayon s'avère “ vite limitée par la taille des programmes actuels à vérifier. D’où l’idée d’utiliser les ordinateurs pour aider, systématiser, mécaniser [ce qu'on appelle] les preuves de correction.”

Selon la façon d’impliquer les ordinateurs dans les démarches de preuve et de correction,  les scientifiques distinguent  les techniques algorithmiques (comme le model checking ou l'interprétation abstraite) et les techniques déductives (dans lesquelles un utilisateur interagit avec un assistant de preuve). Ces approches peuvent elles-mêmes se combiner de nombreuses façons.

Pour augmenter la confiance dans la correction des programmee, le test est une alternative à la vérification. Son objectif est “moins ambitieux. Il s’agit de trouver des erreurs lorsqu’il y en a. Il ne s’agit pas d’assurer l’absence totale d’erreur, au moins par rapport à une propriété donnée (comme en vérification), mais de trouver des erreurs et d’en trouver le maximum..”

Jusqu'à présent, Vlad Rusu a orienté ses recherches dans deux directions principales. Tout d'abord : “associer à la preuve formelle des techniques d'abstraction et de "compositionnalité" pour permettre de passer à l'échelle et de traiter des études de cas réalistes.” Deuxièmement : “combiner la vérification formelle et le test de conformité pour valider des implémentations boite-noire (2) de systèmes réactifs par rapport à leurs spécifications et/ou à d'autres propriétés de haut niveau.”

 “Je pense avoir illustré le fait que la vérification et le test (de conformité ou autre) sont complémentaires, au niveau des opérations, mais aussi dans une méthodologie de validation formelle au niveau des systèmes, en particulier réactifs, explique Vlad Rusu. Je pense que l’avenir, c'est l’intégration d’une méthode, l’intégration de différentes techniques entre elles mais aussi l’intégration de vérifications et tests. Ceci aussi avec d’autres techniques formelles, comme la synthèse de contrôleurs et le diagnostic de faute.” Autant de travaux engagés au sein de l'équipe Vertecs (3).

En l'état de l'art, les preuves de correction assistées par ordinateur demeurent chronophages et donc terriblement onéreuses. Il a ainsi fallu à Vlad Rusu trois mois pour effectuer une étude de cas sur le protocole ATM-SSCOP (4) à l'aide de l'assistant de preuve PVS (5), “un temps relativement raisonnable pour une étude de cas relativement conséquente, mais qui reste loin des délais de rigueur dans le monde industriel”, fait-il remarquer. Ce type de travail long et fastidieux alourdit aussi la facture et limite donc l'emploi des méthodes formelles à des secteurs où leurs avantages compensent le surcoût.

Pour Vlad Rusu, “Les outils ne sont pas encore tout à fait mûrs." Ce problème bloque le développement des applications industrielles à plus grande échelle.  "Il manque souvent des spécifications et des propriétés.” La matière première en quelque sorte. Mais le chercheur entrevoit  “plus qu’un début promoteur dans certaines industries. Par exemple, dans les circuits, le model checking est utilisé couramment pour tester de l’équivalence ou pour prouver de l’équivalence entre  différentes vues de circuits.  En développement logiciel également : un outil comme Slam permet de vérifier certaines propriétés standard de programme C pour un sous-ensemble du langage C, et ce, de manière complètement automatique.”  (6)

Pour  intéresser les industriels à ces techniques, Vlad Rusu estime qu'une façon de faire consiste à “construire des liens avec les méthodes (semi-formelles), les notations qu’ils ont déjà l’habitude d’utiliser, pour faire en sorte qu’ils commencent à utiliser les méthodes formelles même sans s’en rendre compte. John Rushby (7) parle de méthodes formelles invisibles. Elles sont aussi discrètes que par exemple un compilateur ou un éditeur de texte. Et aussi naturelles.”

Alors, est-ce que cela va arriver ? “Je ne sais pas. Par exemple, les protocoles cryptographiques sont une application cible de choix pour le test, de conformité ou autre. Là, le domaine est vierge et il faut l’occuper. La sécurité informatique comporte de tels enjeux que, peut-être, on tirera bénéfices des modèles formels.”

-----

Notes

(1) Membre du projet VERTECS, Vlad Rusu a présenté différents aspects de ses travaux sur la vérification formelle et le test de conformité pour systèmes réactifs durant sa défense de HDR (Habilitation à Diriger des Recherches) en décembre 2006. Voir la vidéo de la HDR (format Real).

(2)  Les notions de Boîtes blanches et boîtes noires sont utilisées pour décrire le point de vue du développeur de test. Boîte noire  signifie qu'on a une vue extérieure de l'objet de test, c'est-à-dire le code exécutable. la boîte noire fait référence à une vue intérieure, c'est-à-dire au code source.

(3)   PVS: Specification and Verification System. PVS est un assistant automatique de preuve. Prototype de recherche open source, il se veut le nec-plus-ultra en matière de méthodes formelles automatisées.

(4)   ATM (Asynchronous Transfer Mode) est un protocole réseau qui encode les données en petites cellules (53 octets) à taille fixe, au lieu des paquets à taille variable (comme le font les protocoles IP ou Ethernet). SSCOP (Service Specific Connection Oriented Protocol)  est une protocole qui appartient à la couche d'adaptation ATM / B-ISDN et dont la fonction est d'assurer une transmission de données fiable. Pour plus de détails sur ces recherches de Vlad Rusu, lire : Verifying an ATM Protocol Using a Combination of Formal Techniques (2004)  and Verifying an ATM Protocol Using a Combination of Formal Techniques dans The Computer Journal. 2006; 49: 710-730.

(5)   VERTECS est un acronyme pour : VERification models and techniques applied to the TEsting and Control of reactive Systems. Cette équipe de recherche de l'Irisa travaille à améliorer la fiabilité des systèmes réactifs en  en fournissant aux ingénieurs logiciel des méthodes et des outils permettant d'automatiser le plus possible la génération des test et la synthèse de contrôleurs à partir de spécifications formelles de tels systèmes.

(6) Le moteur d'analyse Slam constitue le noyau d'un outil de repérage d'erreurs appelé SDV (Static Driver Verifier) qui analyse systématiquement le code source des drivers de Microsoft Windows en utilisant les techniques de model checking.

(7)    Directeur de programme pour les méthodes formelles au Computer Science Laboratory du Stanford Research Institute (SRI), en Californie, John Rushby dirige le groupe qui a développé l'assistant de preuve PVS.

Cet article en format PDF.

Articles précédents : 

Analyse, modélisation et simulation des mouvements humains

IHE : vers une meilleure interopérabilité des systèmes médicaux

Découvrez Peerple à Linux Expo 07

Premiers pas de Kerlabs à Linux Expo 07

Les images piratées repérées plus vite

Coopération avec l'Afrique

L'Irisa à SuperComputing 2006

Diwall sur les rails

L'INRIA dans le groupe d'experts sur la gestion de ressources Java

Reconnaissance d'écriture manuscrite