Parcoursup est un logiciel critique, c’est à dire un logiciel dont le dysfonctionnement peut avoir un coût très élevé en termes humains ou financiers. Par exemple, un erreur de calcul dans les ordres d’appel pourrait nécessiter un redémarrage de toute ou une partie de la procédure d’admission. Ceci fait que des mesures de sûreté logicielle renforcées soient nécessaires pour garantir un fonctionnement optimal, tout en respectant les exigences légales.
Une spécification désigne les propriétés qu'un algorithme est tenu de respecter. Elles peuvent être exprimées informellement (par exemple, sous forme de cahier des charges rédigé en langage naturelle); formellement, en un langage de spécification logicielle ou de façon semi-formelle.
Le terme algorithme désigne un principe de calcul, qui peut être écrit en langue naturelle, pseudo-code ou langage mathématique.
Finalement, l'implémentation désigne la traduction de l'algorithme en un langage de programmation, exécutable par ordinateur.
Dans Parcoursup, on retrouve chacune de ces composantes:
La spécification plus informelle correspond aux critères posés par la loi (taux boursiers et résidents, nombre de vœux), qui sont concrétisés en une notation semi-formelle dans le cahier de charges de Parcoursup.
L’ algorithme, le principe de calcul utilisé pour établir l’ordre d’appel des candidats se trouve dans le document de présentation des algorithmes de Parcoursup.
Finalement, l’implémentation est le code informatique qui résulte de la transformation des dispositions légales en un logiciel. Le code source de Parcoursup est consultable sur le dépôt dédié.
La conformité algorithmique, dans ce cas-ci peut être comprise à deux niveaux: le premier, est la conformité de l’algorithme aux dispositions légales. Le deuxième, est la conformité de l’implémentation avec l’algorithme, sa spécification et son cahier des charges. En d’autres mots, l’implémentation doit refléter correctement l’algorithme qui doit lui-même refléter correctement la loi.
Méthodes formelles: aide à une conformité algorithmique
Les méthodes formelles sont un ensemble de techniques permettant de garantir qu’un algorithme satisfait son spécification. Ces méthodes peuvent être appliquées à des algorithmes, pour confirmer qu’ils respectent les spécifications, mais aussi à l’implémentation de ces algorithmes dans un langage de programmation.
Preuve mathématique des propriétés des algorithmes
La preuve mathématique peut être consultée aux sections 2.1 et 3.1 du document de Vérification de l’algorithme de calcul des ordres d’appel dans Parcoursup. La preuve complète est consultable en suivant ce lien. La preuve établit mathématiquement la conformite de l’algorithme aux spécifications contenues dans le document de présentation des algorithmes de Parcoursup. La preuve établit également d’autres propriétés de l’algorithme appelées invariants. Ce niveau de détail est essentiel pour la preuve formelle, qui nécessite des objets mathématiques bien définis pour pouvoir être élaboré.
Vérification formelle de l’implémentation en Why3
Why3 est une plateforme de preuve de programme, qui s’appuie sur des prouveurs externes automatiques ou interactifs. Cette plateforme permet de prouver du code écrit en WhyML.
Pour pouvoir mener la preuve à terme, il a fallu traduire l’algorithme implémenté en Java au langage WhyML. Le résultat est assez proche de l’implémentation originale en Java. Un travail en cours permettra prochainement de renforcer le lien entre les deux implémentations, à l’aide de l’outil WhyML2Java.
Une explication de la preuve formelle peut être retrouvée aux sections 2.2 et 3.2 du document de Vérification de l’algorithme de calcul des ordres d’appel dans Parcoursup. En suivant ce lien, on retrouve le code écrit en WhyML de chacune des propriétés prouvées, ainsi que de certaines invariantes nécessaires pour la preuve. L’ exécution de ce code, en partie par des prouveurs automatiques, et d’autre par des prouveurs interactifs, a permis de vérifier formellement les propriétés prouvées mathématiquement.
Le code Why3 des preuves de l’algorithme est directement accessible à l’adresse parcoursup.labri.fr/why3/calcul_ordre_appel.
Les preuves formelles sont accessibles depuis le dépôt:
gitub.u-bordeaux.fr/parcoursup/why3.
Vérification à l’exécution de l’implémentation Java
La vérification à l’exécution (runtime verification) consiste à vérifier chaque exécution d’un programme afin de garantir que cette exécution est conforme à la spécification, ou déclencher une alarme quand ce n’est pas le cas. Cette méthode n’offre pas la même sécurité que la vérification de l’implémentation, mais permet d’augmenter la confiance dans la conformité de l’implémentation, y compris lors des évolutions successives . Les tests implémentant la vérification à l’exécution sont consultables sur le dépôt de Parcoursup.
Source: Vérification de l’algorithme de calcul des ordres d’appel dans Parcoursup, Castéran et al., 2022