ENSEIRB


IF311 - Conception formelle des logiciels

Ce cours est une étude du model-checking comme technique de conception formelle des logiciels. Une description complète de l'enseignement est disponible dans le syllabus.

Intervenant

Frédéric Herbreteau

Documents

Documents de cours

  1. Introduction
  2. Writing algorithms with the TLA toolbox
  3. Verification of sequential programs
  4. Linear Temporal Logic (LTL)
  5. Multi-process algorithms in PlusCal/TLA
  6. Fairness
  7. Formal design of a lift controller
  8. Formal design of a distributed mutual exclusion algorithm
  9. Simulation and bisimulation
  10. Counter-Example Guided Abstraction Refinement
  11. Model-checking LTL formulas

Devoirs

  1. Verification of the Dutch National Flag algorithm
  2. Dining Philosophers

Ressources

L'excellent cours sur le Model-Checking de Srivathsan B. est disponible sur la plateforme NPTEL.

Le blog de Ron Pressler:

Outils

La boîte à outils TLA

Une installation locale de la boîte à outils TLA est disponible sous ~herbrete/public/TLA/toolbox (ajouter le chemin d'accès à votre variable d'environnement PATH). La boîte à outils se lance par la commande toolbox. Un manuel de PlusCal est disponible ici: ~herbrete/public/TLA/c-manual.pdf.