Les méthodes semi-formelles et formelles sont toutes les méthodes se basant sur des preuves mathématiques. En gros, tu vas effectuer une spécification à haut niveau dans un langage mathématiques (en général dérivant du lambda-calcul et/ou de la théorie des ensembles), puis tu vas construire ton logiciel en prouvant mathématiquement qu'il est équivalent à la spécification. Résultat : ton logiciel n'a pas de bug.
Bon, ça c'est la théorie, en pratique la complexité est telle qu'on ne peut généralement pas appliquer une méthodologie pure de A à Z. On doit donc faire des consessions, mais globalement les logiciels créés ainsi ne contiennent presque pas de bug. Il faut aussi que la spécification initiale soit bonne, et c'est là aussi un gros chalenge.
En France, notre recherche est plutôt bien positionnée sur le domaine au niveau mondial, avec en particulier des outils : d'une part, la méthode B et son atelier[1], d'autre part l'assistant à la preuve Coq[2].
Pour ce qui est de la méthode B, c'est une méthode de spécification qui marche par pallier en ce basant sur la théorie des ensembles : on comence par modéliser grossièrement, en posant les propriétés qui doivent être vérifiées, puis on raffine, c'est à dire qu'on devient de plus en plus précis, en prouvant l'équivalence entre chaque niveau. Au final, après un certains nombre de pallier la spécification est tellement précise qu'elle peut être exporter dans un langage (Ada par exemple). Cette méthode a été utilisée par Matra pour construire le SI de météor, la ligne 14 automatique du métro parisien (qui n'a à ce jour jamais eu de problèmes informatique).
Pour ce qui est de Coq, c'est un assistant à la preuve, c'est à dire que c'est un logiciel qui permet de spécifier des propriétés puis de prouver qu'elles sont vrai das un contexte donné. Il se fonde sur un lambda-calcul amélioré, qu'on appelle le Calcul des Constructions Inductives : c'est une Lambda-calcul typé + constructeurs de types + types dépendants / polymorphisme + types inductifs. Avec ça, on dispose d'une expressivité consécante.
Avec Coq, on procéde donc à la spécification du logiciel et de ses propriétés que l'on prouve dans l'assistant. Une fois que les preuves sont faite, on peux réaliser l'extraction du logiciel prouvé. Ceci est quelque chose de très nouveau et Coq est le seul logiciel le proposant pour l'instant : à partir de la preuve, on génére automatiquement le code source du logiciel dans un langage cible (en général, OCaml). On obtient alors le logiciel et on a la preuve qu'il vérifie la spécification et ses propriétés. Bref, c'est beau. Aujourd'hui, Coq et l'extraction de programmes sont utilisés dans une grosse action[3] du CÉDRIC et de l'INRIA afin de certifier un compilateur pour C.
[^] # Re: Des certifications CC-EALx
Posté par Fanf . En réponse à la dépêche Mandrakesoft retenue pour le développement d'un système d'exploitation ouvert de haute sécurité. Évalué à 10.
Bon, ça c'est la théorie, en pratique la complexité est telle qu'on ne peut généralement pas appliquer une méthodologie pure de A à Z. On doit donc faire des consessions, mais globalement les logiciels créés ainsi ne contiennent presque pas de bug. Il faut aussi que la spécification initiale soit bonne, et c'est là aussi un gros chalenge.
En France, notre recherche est plutôt bien positionnée sur le domaine au niveau mondial, avec en particulier des outils : d'une part, la méthode B et son atelier[1], d'autre part l'assistant à la preuve Coq[2].
Pour ce qui est de la méthode B, c'est une méthode de spécification qui marche par pallier en ce basant sur la théorie des ensembles : on comence par modéliser grossièrement, en posant les propriétés qui doivent être vérifiées, puis on raffine, c'est à dire qu'on devient de plus en plus précis, en prouvant l'équivalence entre chaque niveau. Au final, après un certains nombre de pallier la spécification est tellement précise qu'elle peut être exporter dans un langage (Ada par exemple). Cette méthode a été utilisée par Matra pour construire le SI de météor, la ligne 14 automatique du métro parisien (qui n'a à ce jour jamais eu de problèmes informatique).
Pour ce qui est de Coq, c'est un assistant à la preuve, c'est à dire que c'est un logiciel qui permet de spécifier des propriétés puis de prouver qu'elles sont vrai das un contexte donné. Il se fonde sur un lambda-calcul amélioré, qu'on appelle le Calcul des Constructions Inductives : c'est une Lambda-calcul typé + constructeurs de types + types dépendants / polymorphisme + types inductifs. Avec ça, on dispose d'une expressivité consécante.
Avec Coq, on procéde donc à la spécification du logiciel et de ses propriétés que l'on prouve dans l'assistant. Une fois que les preuves sont faite, on peux réaliser l'extraction du logiciel prouvé. Ceci est quelque chose de très nouveau et Coq est le seul logiciel le proposant pour l'instant : à partir de la preuve, on génére automatiquement le code source du logiciel dans un langage cible (en général, OCaml). On obtient alors le logiciel et on a la preuve qu'il vérifie la spécification et ses propriétés. Bref, c'est beau. Aujourd'hui, Coq et l'extraction de programmes sont utilisés dans une grosse action[3] du CÉDRIC et de l'INRIA afin de certifier un compilateur pour C.
Bon, c'était un peu long, désolé...
[1] http://www.atelierb.societe.com/(...)
[2] http://coq.inria.fr/(...)
[3] http://www-sop.inria.fr/lemme/concert/(...)