La spécification et la construction vérifiée de systèmes informatisés Jean-Raymond Abrial, De LTR, Ada, Socrate, Z à B, Event-B et la plateforme Rodin
Collecté par Henri Habrias
JS 2025, Journées Scientifiques de l'université de Nantes
27 mai 2025
" [...] les mathématiques sont une science où l'on ne sait jamais de
quoi on parle ni si ce que l'on dit est vrai" Bertrand Russell (1818)
" [...] les mathématiques sont la seule science où l'on sait toujours
de quoi l'on parle et où l'on est certain que ce que l'on dit est vrai "
Emile Borel , après avoir cité B. Russell in Les grands courants de
la pensée mathématique, dir. par Le Lionnais F. ,Hermann, 1997
1 Introduction, autour de la conférence de J.R.
Abrial au Collège de France
Le 1 avril 2015, Jean-Raymond Abrial, invité par Gérard Berry [1] dans le
cadre du Séminaire : Prouver les programmes : pourquoi, quand, comment ?
au Collège de France, a prononcé une conférence intitulée : Spéci cation,
construction et véri fication de programmes : le parcours d'une pensée
scienti fique sur une quarantaine d'années
Il existe une version antérieure (2013) en anglais de cette conférence [2].
Nous fournissons des extraits de cette conférence dont la vidéo est disponible
sur le site du Collège de France. Nous la complétons par des textes faits principalement
de citations et de références bibliographiques, fournis dans l'ordre
chronologique.
2 Avant 2015
2.1 1938
Naissance le 6 novembre 1938, à Versailles.
2.2 Etudes
Il fut, si ma mémoire est bonne, élève du Prytanée National Militaire de La
Flèche dans la Sarthe. Il fut donc un Brution
2.3 1958
Ecole Polytechnique, sorti en 1960, Ingénieur du Génie Maritime
"Il semble que vous n'avez jamais fait de thèse Pourquoi ? Réponse :
Pas intéressé 1 Vous avez travaillé deux ans au Centre de Programmation
de la Marine. Vous avez fait des publications dans ce cadre.
[3]
Vous êtes connu pour des travaux sur les langages, en particulier
avec le LTR-Langage Temps Réel développé pour le compte de la
Marine Nationale. Vous êtes en lien avec ECA Automation qui a un
contrat avec la Marine pour le projet SENIT de suivi temps réel des
navires.
Réponse : C'est bien ça"
Le système d'exploitation navale des informations tactiques ou SENIT
est un système informatique de traitement des données développé par la Marine nationale. Les premiers navires de combat à être
équipés furent les frégates antiaériennes Sufren employant alors des
ordinateurs Univac et des consoles Hughes Aircraft
2.4 1963-1964
Université Standford aux États-Unis
"Jean-Raymond Abrial : il travaillait pour le Centre de Programmation
de la Marine. C'est comme boursier du gouvernement fran-
çais, que durant deux années, de 1963 à 1965, il suit des cours de
Master à l'université de Stanford ; il y acquiert une vue globale et
systématique sur l'informatique. A cette époque le Gouvernement
français octroie, à de jeunes Français, environ 200 bourses par an
pour descours d'enseignement supérieur aux Etats-Unis, y incluant
le payement des frais de scolarité particulièrement élevés dans les
universités américaines
[4]
2.5 1966
J.R. Abrial, J. Bourgne , P. Yvon,(Centre de Programmation de la Marine,
Paris), La programmation modulaire appliquée à un système militaire en temps
réel, 1966
La suite est sur Research Gate et sur
Comments
Post a Comment