Modules enseignés à l'UFR Sciences et à l'IUT Polycopiés, documents et diverses références J. C. Attiogbé

Formal Software Engineering (Master2, ALMA 2018-2019) - UFR Sciences (12h) Lesson 1 : Introduction to Formal Software Engineering Introduction to Formal Methods Motivating examples Exercices Réviser Logique du premier ordre, Théorie des ensembles, Automates Lesson 2 : Introduction to B/EventB Method B and Event B Method : Part1 B and  Event B Method : Part2 Exercices Etude de cas 1 + Exos bases Exercices en B Guide Prise en main de l'AtelierB Memento of Software Construction Article à lire et synthétiser File System, SBMF 2009 Formal Software Engineering (Master2, ALMA 2017-2018) - UFR Sciences (12h) Lesson 1 : Introduction to Formal Software Engineering Introduction to Formal Methods Exercices Réviser Logique du premier ordre, Théorie des ensembles, Automates Lesson 2 : Introduction to B/EventB Method Introduction to B Method Introduction to Event B Exercices Exercices en B Guide Prise en main de l'AtelierB Memento of Software Construction Article à lire et synthétiser File System, SBMF 2009 Formal Software Engineering (Master2, ALMA 2016-2017) - UFR Sciences (24h) Lesson 1 : Introduction to Formal Software Engineering Introduction to FM Introduction to Logics, Sets and Relations Exercices : LogisSets, B Some readings: landingGearSys, Article Event-B . .. Labs centrale nucleaire algo banquier mini-projets Lesson2 : B Method (C. Attiogbé) Classical B Method Memento of Software Construction . . . Formal Software Engineering (Master 2, ALMA 2015/2016) – UFR Sciences (24h) Lesson1 : Introduction to Formal Software Engineering (C. Attiogbé) Introduction to FM Introduction to FOL and Set Theory Exercices : Logics and Set Theory Lesson2 : B Method (C. Attiogbé) (2 slots : November 5, November 12) Classical B Method Exercices with B – Atelier B / Rodin Memento of Software Construction (with AtelierB V4 – from spec to code) Lesson3 : Event B (C. Attiogbé) (3 slots : November 20, Nov. 27, Dec 4) Event B slides2x1 Exercices with B – Atelier B / Rodin Exercices nucl Articles à lire, compte-rendu (2 pages) à rendre le vendredi 6 décembre : - Tree FileSystem, ICFEM2008 - File System, SBMF 2009 Formal Software Engineering (Master 2, ALMA 2013/2014) – UFR Sciences Lesson1 : Introduction to Formal Software Engineering (C. Attiogbé) Introduction to FM Exercices : Logics and Set Theory Lesson2 : B Method (C. Attiogbé) (2 slots : October 2, October 9) Classical B Method Exercices with B – Atelier B / Rodin Memento of Software Construction (with AtelierB V4 – from spec to code) Lesson3 : Event B (C. Attiogbé) (3 slots : November 20, Nov. 27, Dec 4) Event B slides2x1 Exercices with B – Atelier B / Rodin Articles à lire, compte-rendu (2 pages) à rendre le vendredi 6 décembre : - Tree FileSystem, ICFEM2008 - File System, SBMF 2009 Formal Software Engineering (Master 2, ALMA 2012/2013) – UFR Sciences Lesson1 : Introduction to Formal Software Engineering (C. Attiogbé) B Method – (Classical B) Introduction B Method Part1 slides2x1 slides1x1 Exercices : Logics and Set Theory exosLogicsSetTheory Exercices with B and AtelierB / Rodin : CahierB1, CahierB2, Article à lire pour le 21 novembre 2012 FileSystem2009 Event B Event B slides2x1 slides1x1 Exercices with Event B and AtelierB / Rodin Projects (B and Event-B) to be done by groups of 3 students Memento of Software Construction (with AtelierB V4 – from spec to code)
Construction formelle de logiciels (Master 2, ALMA 2011) Introduction générale aux méthodes formelles Chap1 : Intro. Méthodes formelles Chap2 : Modélisation, Abstraction Rappels de Logique, Théo des ensembles Méthode B Cours Chap 1 : Bases de la modélisation en B Chap 2 : Raffinement Chap 3 : Event B TD/TP/Projets exos Logique exos Ensembles exos Modelisation B – 1 memento_raffinement (ABv4) Lotos NT Cours Chap 1 : Intro aux Alpg de proc. Et Bases de Lotos(NT) TD/TP/Projets Cahier exos 1 Presentation de cadp Projet « Client/Serveur » Docs Manuel de Lotos Cours de F. Lang
Méthodes formelles (Master, avant 2011) spécifications, développement de systèmes
	Modèles orientés état :  Z - Méthode B (Master 2) Bibliothèque NaBLA (B) Intégration de Méthodes Formelles (Master2 R) Modélisation des processus communicants (algèbres de processus, ccs, csp, lotos...) Vérification de programmes par évaluation de modèle  (model checking) Autres ressources d'enseignement

Dernière modification : 19/11/2018
Prenom.Nom@univ-nantes.fr