Velo - Vérification pour l'Environnement et le LOgiciel

Colloque n°1 - Salle N lien Colloque n°1

Ce colloque relie les travaux de J.R. Abrial, du langage LTR développé au Centre de programmation de la marine, à Paris, en passant par le SGBD Socrate développé à l’IMAG de Grenoble, sa participation à la définition du langage ADA, l’invention de la notation formelle Z, puis la méthode de spécification formelle B, suivie de Event B et du projet de plateforme logicielle Rodin.

• Découvrir le programme (version française)
• Discover the program (english version)

Sommaire pdf

replay visio zoom partie 1

• Accueil diapos
  • Intro des actes pdf
  • Citation Montaigne pdf
  • In memoriam pdf
• JR Abrial, un chercheur mono-maniaque de LTR à Event-B en passant par Ada, Z, B, Event-B pdf diapos
  Henri HABRIAS, Professeur émérite, Nantes Université
  • Article Data Semantics JRA [Cargese 1974] pdf
  • Article Extending B without changing it (for Developing Distributed Systems) JRA [1st B conf Nantes 1996] pdf
  • Mejia histoire de B, copie de livre
  • Souvenirs anciens pdf
  • Ils en parlent, Abrial à Oxford et ailleurs pdf
• LTR, un langage pour programmer des systèmes concurrents pdf diapos
  David Andreu, Neurinnov, Henri HABRIAS, Professeur émérite, Nantes Université

  • Initiation au TR basée sur le langage LTR (indépendant de tout OS RT) David Andreu, Neurinnov diapos pdf
  • avec l'aimable participation de Patrick De Bondely, Pascal Grojean et Gérard Le Lann
• A propos de rien odp
  Bill Stoddart, Teesside University

replay visio partie 2 A replay visio partie 2 B

• (visio) JR Abrial et Socrate, genèse de recherche et réalisation grenobloise en conception de BD et SGBDpdf ppsx zip
  intervention de Jean-Pierre GIRAUDIN – Professeur émérite – LIG - Grenoble
  
• (visio) Pédagogie par l’exemple, enseignement de bases de données associant Z0, Z1 et Socrate
  à la Miage de Grenoble en 1980 pdf ppsx zip
  Jean-Pierre GIRAUDIN – Professeur émérite - LIG - Grenoble

  • Notations Z, B etc pdf
  • Article Data Semantics JRA [Cargese 1974] pdf
  • Ils en parlent, Abrial à Grenoble
  • Livre Meyer-Baudouin

  Partie 3

replay visio zoom partie 3

• (visio) Enseigner les techniques formelles avec Event-B et Rodin pdf
  Dominique MERY – Professeur Telecom Nancy - LORIA
• Le développement d’outils logiciels pour B - Systerel pdf diapos
  Frédéric DADEAU - Systerel
• Le développement d’outils logiciels pour B et en B à Clearsy pdf diapos
  Thierry LECOMTE - Clearsy

replay visio zoom partie 4

• Application de B à Paris, Nantes et Orléans pour le recensement de la population de 1990,
  Exemples de constructions de programmes en B pdf diapos
  Guy LAFFITTE - ancien ingénieur INSEE
• Histoire parallèle des méthodes formelles et semi-formelles et des travaux d’Abrial pdf diapos
  Henri HABRIAS, Professeur émérite, Nantes Université
  • Notations Z, B etc pdf
  • Deux crayons. Ontologie ensembliste pdf
• Histoire des projets de recherche nationaux et européens autour de B pdf diapos
  Henri HABRIAS, Professeur émérite, Nantes Université

• B présent, futur, recherche, enseignements TSI V22 N1 2003 pdf
• Histoire de B, Fernando Meija, ancien responsable Méthodes et Outils de Développement logiciel d'Alstom Transport Signalisation pdf
• Spécification multi-formalismes : l'exemple de la facturation Pascal André pdf
• Livres sur Z pdf
• Livres et videos sur B pdf
• Bibliographie JR Abrial pdf
• “Z caused a good deal of confusion on the pronunciation stakes. The English and even Scots and some French call it Zed. The Americans call it Zee and get confused when we correct them Zed. But Ib had his own distinctive pronunciation: Zet. ”( Bill Roscoe , In Memoriam Ib Sorensen)
• Groupe PI pdf Ce groupe réunit des chercheurs du LITP et du CEDRIC-CNAM, travaillant sur la spécification et la certification de systèmes informatisés à l'aide de systèmes d'aide à la preuve (B, Coq, PVS). (transmis par Catherine Dubois)
• Le Centre de Programmation de la Marine (CPM) Avec Abrial mentionné dans une chronique de Claude Kaiser 2011 pdf

* Accès en visio Zoom - (lien) (si besoin » ID de réunion: 841 3282 2581 Code secret: 610460)

• replay visio zoom partie 1
• replay visio partie 2 A
• replay visio partie 2 B
• replay visio zoom partie 3
• replay visio zoom partie 4

Photos de la journée

Ne loupez pas le point de vue du fenetrou

Organisé par :