Conférence de J.-R. Abrial au Collège de France

 https://www.college-de-france.fr/en

 Extrait de https://velo.wiki.ls2n.fr/lib/exe/fetch.php?media=velo:1-cdfenlatex2005.pdf

recopie d'un texte publié en Latex.  

 1e avril. Lors de cette conférence, JRA a 76 ans.

"Cette présentation est celle d'un chercheur vieillissant qui porte un regard
historique sur les quarante dernières années de son travail.
Il y a deux sortes de chercheurs : les prolifiques et les monomaniaques.
Je fais partie de la seconde catégorie, car j'ai toujours pratiqué le
même genre d'investigations, à savoir la spécification et la construc-
tion vérifée de systèmes informatisés.
Ce travail, autant théorique que pratique, s'est concrétisé au cours de toutes
ces années dans trois formalismes voisins : Z, B et Event-B (dont je ne suis pas,
loin de là, le seul contributeur). Je vais tenter d'expliciter comment les idées que
contiennent ces formalismes et les outils correspondants ont lentement émergés
de façon parfois erratique.
Je tenterai aussi de préciser les multiples influences qui ont participé à cette évo-
lution. En particulier, je montrerai comment plusieurs réalisations industrielles
ont permis de progresser dans ce domaine. Mais je soulignerai aussi les échecs et
parfois les rejets de la part de communautés tant universitaires qu'industrielles.
Pour finir, je proposerai quelques réflexions et approches pour le financement
de recherches telles que celle-ci.
Je suis très ému d'être de ce côté ci de amphithéâtre parce qu'il y a 40 ans je
venais écouter dans cet amphithéâtre ou un autre du collège, Roland Barthes,
Roland Barthes qui inaugurait dans ce mai 68 son cours. ll avait fait un cours
dans la chaire de sémiologie, Comment vivre ensemble [12], c'est un titre qui
évoque évoque beaucoup de choses.
Je voudrais juste témoigner de mon parcours scientifique qui s'étend sur une
quarantaine d'années. Maintenant je suis un vieux bonhomme et je peux regar-
der un peu en arrière Il y a deux catégories de chercheurs. Il y a les grands chercheurs qui sont
éclectiques et qui touchent à de nombreux domaines et il y a les petits. Et je fais
partie de cette catégorie. Et je vais parler de cette catégorie. Qui sont monoma-
niaques qui font toujours la même chose et pendant quarante ans j'ai toujours
fait la même chose. Mais vous allez dire qu'est ce que j'ai fait pendant quarante
ans.
Comment savoir si ce qu'on programme est bien ce que l'on voulait entre la
tâche que l'on assigne à la machine et bien savoir ce que l'on veut.
Et pour cela j'ai développé différents formalismes qui s'appellent Z, B et je vou-
drais vous présenter tout simplement l'évolution de quelqu'un qui a toujours
réfléchi au même problème. Alors il se passe trente ans entre la première publi-
cation sur Z puis en 1996 mon livre sur B [8] The B-Book, Assigning programs
to meanings 16
Alors quel sera le plan de ma présentation ? Elle ne sera pas aussi technique
et aussi brillante que celle de Gérard, à la fin mon exposé sera un peu plus
technique mais ne sera pas difficile à comprendre.
Alors, comment tout a commencé ? Tout à commencé parce que dans les
années 70, le gouvernement américain a lancé un projet un langage de pro-
grammation une short liste quatre propositions ont été retenues et je fais partie
de l'équipe, le langage vert et qui était dirigée par le regretté Jean Ischbia .
J'étais dans ce groupe et j'avais quelques problèmes avec les autres membres de
l'équipe parce qu'il étaient très occupés à regarder des petits points de détail
de ce langage et moi je disais, c'est un langage de programmation, il faudrait
peut-être programmer et je suis l'un des premiers programmeurs de Green qui
allait devenir le langage Ada mais je me posais la question, comment savoir si
ces programmes que j'avais écrits étaient corrects ? S'ils faisaient bien ce que je
voulais qu'ils fassent. Alors pour y arriver j'écrivais de petites notes en anglais,
parce que tout le monde parlait anglais dans cette équipe c'était une équipe
internationale. Donc j'avais bien écrit des notes explicatives mais le problème
était  est-ce que ces notes correspondent bien au programme ? Comment com-
parer quelque chose qui est écrit en anglais à quelque chose qui est écrit dans
un langage de programmation ? Donc je pensais qu'il était important d'avoir un
moyen systématique pour faire cette fameuse comparaison.
Voilà les réflexions que je me faisais l'année 74 à peu près à la même époque
où je suivais les cours de Roland Barthes. J'étais à la recherche d'une notation
formelle. Et à cette époque là, j'étais assez intéressé par les fameux traités de
Nicolas Bourbaki [21], une espèce de reconstruction systématique des mathéma-
tiques dont le premier livre s'appelle Théorie des ensembles. Et donc je m'étais
plongé dans ce livre et j'ai eu énormément de difficultés, j'ai mis un temps fou
à lire les 50 premières pages mais au bout d'un certain temps je me suis senti
plus familiarisé et je me suis dit, peut-être que cette notation formelle à laquelle
j'aspire pour ces notes explicatives, ce serait bien d'utiliser la notation de la
théorie de ensembles. Ça a un avantage c'est que tout le monde qui a fait des
études scientifiques connaît et que c'est quelque chose qui est largement utilisé
dans les bouquins de maths 17. En effet ce qui est intéressant dans l'usage des
16. Dans son cours à Nantes, J.R. Abrial a cité comme première source de B, l'article de
Robert Floyd, Assigning meanings to programs [13] et en 2010, Event-B [14].
17. Note personnelle : Quand je suis arrivé un jour à l'IUT de Nantes avec le premier livre
de J.D. Warnier (et Flanagan), heureux d'avoir trouvé une méthode de programmation qui
mathématiques est que l'expression est rigoureuse, ne prête pas à ambiguïté
comme souvent les langages les plus récents de programmation, et surtout les
maths ça sert à écrire des preuves. [. . .] Mais j'ai tout de suite eu des déboires.
On m'avait proposé de faire un cours autour de cette approche dans une école
d'été. Et c'était immédiatement annulé. On m'a dit  ça n'a aucun intérêt pour
ce genre de sujet . Il fallait comprendre que je m'étais trompé mais je suis
quelqu'un d'un petit peu obtus, alors quand j'ai une idée, je vais essayer de la
poursuivre. En fait, les informaticiens n'aiment pas du tout la théorie des en-
sembles. Ils confondent mathématiques et informatique, ils confondent prédicat
et expression booléenne, mais d'un autre côté les mathématiciens ne sont pas
très forts en logique. Si vous regardez des preuves assez classiques sur Wikipedia
ou sur Internet vous verrez des preuves effroyables, des preuves dans lesquelles
précisément il y a pas mal de quantications universelles ou existentielles et ces
preuves ne sont pas complètes ou ce sont des preuves par cas et tous les cas ne
sont pas prévus, etc. Et il semblerait qu'il soit un peu difficile de réconcilier ces
deux communautés. Je me trouvais un peu en porte à faux dans chacune d'elles.
Heureusement j'ai eu la chance à la fin des années 70 d'être invité par Tony
Hoare à Oxford et j'ai pu faire un travail commun avec Bernard Sufrin et Ib Sø-
rensen [15] [16] [7]. Je citerai beaucoup de noms car il est important de montrer
que je n'ai pas fait ses choses là tout seul mais que c'était évidemment avec un
groupe de gens qui m'ont beaucoup aidé et nous avons développé une notation
basée sur la théorie des langages. Nous n'avons pas développé un langage, il
n'y avait pas de raison de développer un langage. Nous avons seulement archi-
tecturée un peu cette notation. Z était né et c'était à peu près n des années
70 [...] J'étais vraiment naïf. On était loin de résoudre le problème initial : la
fameuse comparaison entre les notes explicatives, maintenant formalisées en Z
i.e. en théorie des ensembles et le programme. Quelles preuves pouvait-on faire
pour tenir lieu de cette comparaison. Au début des années 80, après mon séjour
à Oxford pendant deux ans, je suis rentré en France et j'ai eu l'idée de quelques
orientations nouvelles, simplifier Z, structurer Z, mais surtout introduire le raf-
finement. C'est quelque chose qui a été étudié par beaucoup de gens, Back [17],
[18], [?],Hoare, Morgan [20], Jones, et surtout d'automatiser la programmation.
Maintenant faisons un petit détour par d'autres disciplines de l'ingénierie. L'avia-
tion, l'architecture ou par exemple le génie civil. Et bien qu'est ce qu'ils font
ces gens-là ? Est-ce qu'ils utilisent des approches similaires ? Existe-t-il des
approches dans d'autres disciplines consistant à faire quelque chose avant la
construction proprement dite ? Oui les dessins industriels et les plans. Il serait
impossible, aberrant de se précipiter à construire un avion, un pont, un avion,
une maison sans avoir fait des plans ? Et bien, assez souvent, les gens se préci-
pitent sur le terminal et programment directement. J'ai eu encore récemment la
visite d'un amis qui travaille maintenant aux USA qui travaille chez eBay, eBay
c'est la formule américaine du Bon Coin. Il est à Portland dans l'Oregon et il
dirige toute une armée de programmeurs et il me dit que les programmeurs se
précipitent, n'écrivent rien avant. Dans notre discipline on est complétement ar-
riérée par rapport aux autres disciplines. Le dessin industriel remonte au XIXe ;
Il serait impensable de faire quelque chose sans avoir des plans.

me semblait bien applicable aux  applications de gestion  alors qu'aucune n'était enseignée
alors, un collègue qui faisait  calcul numérique-Fortran  m'a dit " Ah des ensembles ! Aucun
intérêt ". J'avais fait un stage chez ICL où était appliqué chez les clients la " méthode Cantor
", mais les ensembles n'y étaient pas utilisés ! Et je l'enseignais.

Qu'est ce que c'est qu'un dessin industriel ? C'est une certaine représentation
de ce que l'on veut construire mais cette représentation n'est pas une maquette.
La base manque : on ne peut pas  conduire  le dessin d'une voiture. Mais
on peut raisonner sur notre futur système durant sa conception, et c'est là que
c'est extrêmement important [...]. Dénir et calculer le fond du système (ce qu'il
doit faire), incorporer les contraintes du système (ce qu'il ne doit pas faire), en
dénir l'architecture. Tout ceci est basé sur des théories scientiques bien éta-
blies, résistance des matériaux, mécanique des fluides, la gravitation, etc. Nous
avons aussi des techniques de raisonnement sur plan, utilisation de conventions
prédénies. Quand vous voyez un plan tout le monde peut le lire. Il y a un pro-
blème de communication qui est très important. Nous pouvons le lire car nous
adhérons à un certain nombre de conventions et des conventions doivent facili-
ter le raisonnement. On peut avoir plusieurs plans, ajouter des détails de plus
en plus précis. On arrive à cette notion de raffinement. Repousser des choix en
élaborant des options. On ne sait pas encore si le toit de la maison sera en tuiles
ou en un autre matériau. Par contre il doit avoir la propriété que l'eau ne rentre
pas dans la maison. Mais on va repousser le choix précis. Décomposer un plan
en plusieurs sous-plans. Réutiliser des vieux plans avec quelques changements
[. . .] Au lieu d'avoir une seule note je vais en avoir une série emboîtées et entre
chacune d'elles il y aura éventuellement des preuves. Entre les notes formelles,
ranement et preuves. Les notes s'appellent maintenant des modèles formels.
Le programmeur est devenu un modélisateur.
Evidemment dans l'industrie il y a un rejet assez profond pour ce type d'ap-
proche, mais pas partout [. . .] Est-ce que ça marche ? Evidemment le programme
qui a été obtenu, on ne doit pas y toucher. Sur l'après le programme on a les
tests, les assertions, l'interprétation abstraite, les preuves. Mais avant le pro-
gramme ? On n'a pas grand-chose. Certes on a UML. Personnellement je n'aime
pas beaucoup parce que je trouve que ce n'est pas tout à fait assez rigoureux.
[. . .] Pendant les années 80, j'ai eu des contacts avec la RATP qui a projeté un
métro semi-automatique sur le RER de la ligne A et qui avait développé un
très important système embarqué mais à la dernière minute les managers ont
eu à prendre la décision nale. Je suis contacté par Claude Hennebert [27] ,
ingénieur de la RATP qui est un individu extrêmement intéressant parce qu'il
était à la RATP et qu'il était ni énarque ni polytechnicien il était bloqué. C'était
quelqu'un qui était assez haut dans la hiérarchie donc assez près des robinets
d'argent mais en même temps qu'il avait gardé un très bon esprit technique,
donc il m'a contacté et il m'a dit  on voudrait faire un audit technique. A duré
trois semaines. J'ai rencontré des gens très intéressants et devais répondre à des
questions. Les moyens mis en œuvre permettent-ils de garantir que le produit
nal correspond bieu à sa spécification initiale ?
Alors je fais mon étude et puis à une grande réunion, il y avait des gens de la
RATP et aussi des industriels qui fabriquaient ce système et j'ai dit , je ne peux
pas répondre parce que j'ai pas vu des spécications, je n'ai pas vu d'avant.
Les gens étaient fous de rage, foux furieux et ils m'ont ditj c'est pas vrai. Mais
montrez le moi ! Et même je n'ai pas vu de document de design, de conception,
i.e. que les gens nalement, avaient programmé. Très bien, je ne portais pas de
jugement sur ce qui avait été fait, mais je ne pouvais pas répondre à la ques-
tion. Finalement le projet a été retardé d'un an, probablement pas uniquement
à cause de ce que j'ai raconté, mais pour la RATP retarder un projet d'un an
était un drame parce que la RATP est considérée comme le meilleur métro du
monde, ce qui est vrai. [. . .] Il n'y avait pas de spécication, alors faites nous un
cours de spécication. Alors là j'était un peu tremblotant parce qu'il a fallu que
je bâtisse un cours de spécication qui a si bien marché qu'à la mi-80 la RATP a
décidé de se lancer dans un métro sans conducteur, vous l'avez tous pris, la ligne
14 et ils ont été convaincus par B pour développer les parties critiques du logiciel
et ils ont aussi mis la main à la pâte et de l'argent pour développer un outil "
Atelier B ", entièrement nancé par la RATP et c'est l'outil qui va permettre de
faire tous les ranements et toutes ses preuves. Et la RATP décide  et là encore
je trouve que ce monsieur Hennebert était vraiment un type extraordinaire. Ils
ont dit, on va supprimer les tests unitaires et supprimer les tests d'intégration,
ce qui est très intéressant parce que les tests pour de tels systèmes embarqués
ça coûte extrêmement cher. Ils ont supprimé de l'après parce que l'avant était
solide et en octobre 98, lancement de la ligne 14. Depuis lors pas de problème.
Initialement Matra Transports était absolument contre l'utilisation de B. Là
encore monsieur Hennebert était absolument incroyable. Il a dit  Vous êtes
contre, d'accord, alors vous allez faire les deux, un avec vos techniques et aussi
la technique avec B et puis on verra. Ils ont ouvert les robinets bien sûr et petit à
petit ont ni par être convaincus et en particulier les ingénieurs se sont très bien
adaptés à cette nouvelle technologie parce qu'il fallait faire les fameuses preuves
et en particulier certaines de ces preuves sont automatiques mais d'autres sont
interactdives i.e. que l'utilisateur doit utiliser l'outil pour aider l'ordinateur a
faire la preuve. [. . .] Pour la ligne 1 ce qui est remarquable c'est que pendant
un certain temps il y avait des métros sans conducteur et derrière vous aviez un
métro avec conducteur. J'avais dit à la RATP que c'était très dangereux d'avoir
ça car vis-à-vis du système automatique, les métros avec conducteur sont des
espèces de bouzins qu'on ne peut pas contrôler et donc c'était très difficile.
Pourquoi plus de succès ? Parce que Matra Transport a développé un outil de
raffinement automatique. L'Atelier B développé par la société Clearsy, un outil
de raffinement développé par Matra Transport. Deux sociétés font du B, Clearsy
et Systerel, et elles marchent très bien." [...]
Ensuite je me suis intéressé aux études systèmes. [...]
Jusqu'à présent B et Event-B étaient utilisés pour modéliser des systèmes dis-
crets. Mais les systèmes hybrides deviennent de plus en plus importants. Qu'est-
ce que c'est qu'un système hybride ? On doit contrôler, au moyen d'interventions
discrètes, une situation externe en évolution continue. [...] Là je suis encore très
intéressé par le travail de Ralph Back , Luigia Petre et Ivan Porres .
 Les parties continues sont dénies à l'aide de fonctions temporelles
 les fonctions temporelle sont souvent dénies par des équations différen-
tielles
 et ces équations sont souvent non résolubles analytiquement.
 Comment alors prouver certaines propriétés de ces fonctions ?
Tout ceci est actuellement du domaine de la recherche.
Un petit exemple [...] Commande d'un train d'atterrissage. [...] Approche
méthodologique du système.
 le cahier des charges
 la stratégie de ranage
 le développement des modèles formels
Quelques développement du cahier des charges sur l'Environnement.
 Le système comprend trois trains (gauche, droite, devant) ENV1
 Chaque train comprend des roues qui peuvent être rétractées, étendues
ou en mouvement ENV2
 Chaque train comprend aussi une porte qui peut être ouverte, fermée ou
en mouvement ENV3
 Les trains (portes et roues) sont mis en mouvement par l'intermédiaire
de pistons hydrauliques ENV4
 Dans le cockpit, il y a, à la disposition du pilote une poignée qui peut
être en position haute ou basse ENV5
a dû faire un atterrissage car le pilote s'est aperçu que deux des circuits hy-
drauliques étaient en panne. Alors il a dû descendre le train manuellement. Ce
qui est gênant dans ces cas là, c'est qu'ensuite on ne donne pas les raisons [...]
Quelques éléments
 Si les trains sont rétractés et que la poignée va de haut en bas, la séquence
d'extension a lieu FUN1
 Séquence d'extension : ouverture des portes, extension des roues, ferme-
ture des portes, idem dans l'autre sens FUN2
 En cours d'extension ou de rétraction, le pilote peut changer la position
de la poignée FUN3
Ces éléments du cahier des charges sont des phrases simples avec un numéro et
un label, ici FUN pour fonction. Et FUN3 complique les choses et en particulier
ça peut provoquer des blocages [...] Il faut prouver que si le pilote ne fait pas
monter, descendre la poignée autant de fois qu'il le veut ou arrête de le faire alors
la train arrivera à descendre ou à remonter [...] Quelques détections d'anomalies
 Circuits non pressurisés 2 secondes après stimulation ANM1
 Portes encore fermées 7 secondes après stimulation ANM2
 Portes encore ouvertes 7 secondes après stimulation ANM3
 Roues non rétractées 10 secondes après stimulation ANM4
 Roues non étendues 10 secondes après stimulation ANM5
On a : 21 ENV, 13 FUN, 7 AMN. A partir de ça je dois faire une stratégie de
raffinement.
 0 Mouvements libres de la poignée et du train "unique" (abstraction)
 1 Synchronisation de la poignée avec le train "unique" Je suppose que
j'ai une connexion directe de la poignée et les différents éléments. Mon
abstraction triche avec la réalité.
 2 Contrôle des portes et des roues par le logiciel
 3 Introduction des électro-valves hydrauliques
 4 Introduction des contraintes temporelles
 8 Introduction des 3 trains qu'il faut synchroniser
Il faut que je vérifie la couverture du cahier des charges, i.e. que tous les
élément du cahier des charges sont bien pris en compte. Le développement
 Construction progessive des modèles (par raffinements successifs)
 Preuves systématiques effectuées à chaque étape :
 conservation d'invariants
 raffinements corrects
 absence de bloquage
 Confrontation à chaque étape avec d'autres approches :
 model checking
 animations
et même les tests. Je ne rejette pas du tout l' "après", mais je le fais à chaque
niveau de raffinement. Les résutats : plus de 2000 preuves (toutes prouvées au-
tomatiquement). J'arrive à la fin.

Z et Event-B essentiellement utilisés dans le milieu universitaire, B essentielle-
ment dans le milieu industriel. D'après moi, ceci est dû à la méthode de finan-
cement.
 Z initialement développé à Oxford
 B financé par le projet industriel de la RATP pour la ligne 14
 Event-B financé par des projets européens
Alors je ferai une suggestion. Pourrait-on généraliser la méthode de financement
de B ? Par un pourcentage systématique d'un grand projet industriel. Ça existe
pour les œuvres d'art érigées devant les hôpitaux, etc. J'en ai parlé mais n'ai eu
aucun succès ; Pourtant ça existe, au Brésil, en Suisse. [...