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

Cette page est en lecture seule. Vous pouvez afficher le texte source, mais ne pourrez pas le modifier. Contactez votre administrateur si vous pensez qu'il s'agit d'une erreur.
{{ :velo:js2025.png?500 |}}

===== CL1 - J.R. Abrial, un pionnier du développement scientifique des langages informatiques et des méthodes formelles et de leur application à grande échelle dans l’industrie ===== 

Colloque n°1 - Salle N [[https://js.univ-nantes.fr/jassiste-aux-colloques/js25cl1|lien Colloque n°1]]

{{:velo:logo-js-abrial.png?300 |}}
/* __Résumé__ */
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.

===== Programme =====

* [[https://js.univ-nantes.fr/medias/fichier/a2-js-25-cl01-programme-fr_1747379748576-pdf?ID_FICHE=1809291&INLINE=FALSE|Découvrir le programme (version française)]]
* [[https://js.univ-nantes.fr/medias/fichier/a2-js-25-cl01-programme-en_1747379779789-pdf?ID_FICHE=1809291&INLINE=FALSE|Discover the program (english version)]]


===== Actes =====

/* //A venir// */
Sommaire {{ :velo:sommaire_des_actes12-05.pdf |pdf}}


==== Communications du colloque ====

==Partie 1==

[[https://uncloud.univ-nantes.fr/index.php/s/A2FXBY5tbH2RdWG|replay visio zoom partie 1]]

* Accueil {{ :velo:bienvenue_a_nantes.pdf |diapos}}
  * Intro des actes {{ :velo:1-introactesjsenlatex25-05.pdf |pdf}}
  * Citation Montaigne {{ :velo:citation_montaigne.pdf |pdf}}
  * In memoriam {{ :velo:inmemoriam.pdf |pdf}}

* //JR Abrial, un chercheur mono-maniaque de LTR à Event-B en passant par Ada, Z, B, Event-B// {{ :velo:1-cdfenlatex2005.pdf |pdf}} {{ :velo:bio_de_jr.pdf |diapos}}\\
Henri HABRIAS, Professeur émérite, Nantes Université

  * Article //Data Semantics// JRA  [Cargese 1974] {{ :velo:cargese-jra.pdf |pdf}}
  * Article //Extending B without changing it (for Developing Distributed Systems) // JRA [1st B conf Nantes 1996] {{ :velo:articlejra-firstbconf.pdf |pdf}}
  * Mejia histoire de B, copie de livre
  * Souvenirs anciens {{ :velo:souvenirsanciensfinal.pdf |pdf}}
  * Ils en parlent, Abrial à Oxford et ailleurs {{ :velo:abrial_a_oxford.pdf |pdf}}

* //LTR, un langage pour programmer des systèmes concurrents// {{ :velo:2-ltr-habrias.pdf |pdf}} {{ :velo:ltr3.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 {{ :velo:courserii4-ltr.pdf |diapos pdf}}
  * avec l'aimable participation de Patrick De Bondely, Pascal Grojean et Gérard Le Lann

* //A propos de rien// {{ :velo:bill_stoddart.odp |odp}}{{ :velo:rien_.mp3 |mp3}}\\
Bill Stoddart, Teesside University

==Partie 2==

[[https://uncloud.univ-nantes.fr/index.php/s/jCkbgtMqg9nM883|replay visio partie 2 A]]
[[https://uncloud.univ-nantes.fr/index.php/s/LcbMn8mmXS8C5BD|replay visio partie 2 B]]

* //[[https://univ-nantes-fr.zoom.us/j/84132822581?pwd=FzLePpcX9K7UbaPiVX31a8qpFjJjKD.1|(visio)]]//
//JR Abrial et Socrate, genèse de recherche et réalisation grenobloise en conception de BD et SGBD//{{ :velo:3-4--jpgiraudin-js25nantes-jrabrialgrenoblois.pdf |pdf}} {{ :velo:exposejeanpierre-partie1-js25nantes-20mai.zip |ppsx zip}}\\
intervention de Jean-Pierre GIRAUDIN – Professeur émérite – LIG - Grenoble  

* //[[https://univ-nantes-fr.zoom.us/j/84132822581?pwd=FzLePpcX9K7UbaPiVX31a8qpFjJjKD.1|(visio)]]//
//Pédagogie par l’exemple, enseignement de bases de données associant Z0, Z1 et Socrate\\
à la Miage de Grenoble en 1980// {{ :velo:3-4--jpgiraudin-js25nantes-jrabrialgrenoblois.pdf |pdf}} {{ :velo:js25nantes-jpgiraudin-partie2-20mai.zip |ppsx zip}}\\
 Jean-Pierre GIRAUDIN – Professeur émérite - LIG - Grenoble  
  * Notations Z, B etc {{ :velo:notation_z_b_etc.pdf |pdf}}
  * Article //Data Semantics// JRA  [Cargese 1974] {{ :velo:cargese-jra.pdf |pdf}}
  * Ils en parlent, Abrial à Grenoble
  * Livre Meyer-Baudouin 

==Partie 3==

[[https://uncloud.univ-nantes.fr/index.php/s/6mxYeLqtmBxcpb7|replay visio zoom partie 3]]

* //[[https://univ-nantes-fr.zoom.us/j/84132822581?pwd=FzLePpcX9K7UbaPiVX31a8qpFjJjKD.1|(visio)]]// 
//Enseigner les techniques formelles avec Event-B et Rodin// {{ :velo:5-mery-nantes27052025.pdf |pdf}}\\
Dominique MERY – Professeur Telecom Nancy - LORIA 

* //Le développement d’outils logiciels pour B - Systerel// {{ :velo:9-_societesb.pdf |pdf}} {{ :velo:systerel-nantes2025_a.pdf |diapos}}\\
Frédéric DADEAU - Systerel 

* //Le développement d’outils logiciels pour B et en B à Clearsy// {{ :velo:10-lecomte-le_developpements_de_logiciels_avec_b.pdf |pdf}} {{ :velo:2025.05.27_-_dev_log_b_clearsy_-_final.pdf |diapos}}\\
Thierry LECOMTE - Clearsy 

==Partie 4==

[[https://uncloud.univ-nantes.fr/index.php/s/aAWJmwgnP8nWofH|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//  {{ :velo:8-guy_laffitteapplicationbaparis.pdf |pdf}} {{ :velo:propos_de_banc_de_touche.pdf |diapos}}\\
Guy LAFFITTE - ancien ingénieur INSEE

* //Histoire parallèle des méthodes formelles et semi-formelles et des travaux d’Abrial// {{ :velo:6-biblio-25-05-2025.pdf |pdf}} {{ :velo:autour_et_alentours.pdf |diapos}}\\
Henri HABRIAS, Professeur émérite, Nantes Université
  * Notations Z, B etc {{ :velo:notation_z_b_etc.pdf |pdf}}
  * Deux crayons. Ontologie ensembliste {{ :velo:ontologieensembliste2105.pdf |pdf}}

* //Histoire des projets de recherche nationaux et européens autour de B// {{ :velo:7-habrias-projets_de_recherche_b.pdf |pdf}} {{ :velo:les_projets_b.pdf |diapos}}\\
Henri HABRIAS, Professeur émérite, Nantes Université 


==== Compléments au fil de l'eau ====

/* //A venir// 

* Intro des actes {{ :velo:introactesjsenlatex.pdf |pdf}}
* Abrial à Oxford et ailleurs {{ :velo:abrial_a_oxford.pdf |pdf}}
* Article JRA  Cargese {{ :velo:cargese-jra.pdf |pdf}}
* Article JRA (1st B conf ) {{ :velo:articlejra-firstbconf.pdf |pdf}}
* Deux crayons. Ontologie ensembliste {{ :velo:ontologieensembliste2105.pdf |pdf}}
* Much ado about nothing Dunn et al. {{ :velo:much_ado.pdf |pdf}}
* Livres sur Z 
*/
/* * Les 16 cas de relations binaires (papygrammes, NIAM, Merise, UML, Z0, B, notation de E. Codd (schémas
relationnels n-aires)) 
* Notations Z, B etc {{ :velo:notation_z_b_etc.pdf |pdf}}
* Mejia histoire de B, copie de livre
* Sociétés B 
*/
/*
* Livres et videos sur B {{ :velo:livres_et_videos_sur_b.pdf |pdf}}
* Bibliographie JR Abrial {{ :velo:bibliographie_jean-raymond_abrial_-_17_mai_2025.pdf |pdf}}
* In memoriam {{ :velo:inmemoriam.pdf |pdf}}
* Citation Montaigne {{ :velo:citation_montaigne.pdf |pdf}}
* Souvenirs anciens {{ :velo:souvenirsanciensfinal.pdf |pdf}}
* Article //Application d’ontologies formelles au droit // André & Habrias {{ :velo:ontodroithhpa.pdf |pdf}}
*/

* Extrait de Programmation statique avec Z - Baudoin/Meyer {{ :velo:programmation_statique_z_-_bm.pdf |pdf}}
* "Une approche formelle de la construction ds logiciels" JR Abrial, traduite par G. Laffitte, 5 sept. 1989 {{ :velo:abrial-laffite-1998.pdf |pdf}}
* B présent, futur, recherche, enseignements TSI V22 N1 2003 {{ :undefined:tsi-v22n1-2004-bpresent-futur-recherche-ens.pdf |pdf}}
* Histoire de B, Fernando Meija, ancien responsable Méthodes et Outils de Développement logiciel d'Alstom Transport Signalisation {{ :velo:specformelleavecb-avant-propos-mejia.pdf |pdf}}
* //Spécification multi-formalismes : l'exemple de la facturation// Pascal André {{ :velo:rr135.pdf |pdf}}
* Livres sur Z {{ :velo:livres_sur_z.pdf |pdf}}
* Livres et videos sur B {{ :velo:livres_et_videos_sur_b.pdf |pdf}}
* Bibliographie JR Abrial {{ :velo:bibliographie_jean-raymond_abrial_-_17_mai_2025.pdf |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 {{ :velo:groupepi-transmis_par-cartherine-dubois.pdf |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 {{ :velo:lecpm.pdf |pdf}}

===== Visioconférence =====

/* //A venir// */ 

* Accès en visio Zoom - [[https://univ-nantes-fr.zoom.us/j/84132822581?pwd=FzLePpcX9K7UbaPiVX31a8qpFjJjKD.1|(lien)]] //(si besoin >> ID de réunion: 841 3282 2581 Code secret: 610460) //


* [[https://uncloud.univ-nantes.fr/index.php/s/A2FXBY5tbH2RdWG|replay visio zoom partie 1]]
* [[https://uncloud.univ-nantes.fr/index.php/s/jCkbgtMqg9nM883|replay visio partie 2 A]]
* [[https://uncloud.univ-nantes.fr/index.php/s/LcbMn8mmXS8C5BD|replay visio partie 2 B]]
* [[https://uncloud.univ-nantes.fr/index.php/s/6mxYeLqtmBxcpb7|replay visio zoom partie 3]]
* [[https://uncloud.univ-nantes.fr/index.php/s/aAWJmwgnP8nWofH|replay visio zoom partie 4]]


===== Photos=====

[[https://uncloud.univ-nantes.fr/index.php/s/MeKxyRSiwEXD9B3|Photos de la journée]]

===== Les JS2025 se passent à Nantes =====

Ne loupez pas le point de vue du [[https://lefenetrou.blogspot.com/2025/05/bienvenue-js2025-de-nantes-universite.html|fenetrou]]
/* <note tip>En architecture, un fenestron ou fenestrou est une petite fenêtre. </note> */

Organisé par : {{:velo-logo-03.jpg?100|}} {{:velo:logo_ls2n_2025.png?60|}} {{:velo:blank.png?20|}} {{:velo:nantesuniversite.png?110|}}
Velo - Vérification pour l'Environnement et le LOgiciel

Outils pour utilisateurs

Outils du site

Outils de la page
