IF311 - Conception formelle des logiciels

Ce cours étudie le model-checking comme technique de conception formelle des logiciels.

Intervenant

Frédéric Herbreteau

Documents

Documents de cours

  1. Introduction
  2. Sequential algorithms in PlusCal/TLA
  3. Comparing test, model-checking and proof on the binary search algorithm
  4. Multi-process algorithms in PlusCal (Notes de cours)
  5. Specifications in LTL / Linear Temporal Logic (Notes de cours / Notes de cours 2)
  6. Designing a producer/consumer protocol
  7. LTL model-checking / Model-checking LTL Specifications
  8. Fairness / Model-checking under fairness assumptions

Ressources

Le blog de Ron Pressler:

Outils

Nous utiliserons l'outil Spot (voir ci-dessous) pour les exercices sur la logique LTL et l'algorithme de model-checking. Les autres séances se basent sur PlusCal/TLA+. Vous pouvez choisir de travailler soit sous Codium ou VS Code, soit avec la boîte à outils TLA. Nous recommandons autant que possible Codium.

Codium ou Visual Studio Code

L'extension TLA+ pour Codium ou Visual Studio Code permet d'éditer et de vérifier des modèles PlusCal/TLA+. Elle est disponible directement dans le magasin d'extensions et également ici.

NB: Codium est la version open source de Visual Studio Code, qui ne contient pas les extensions de télémétrie que Microsoft ajoute à Visual Studio Code. Nous recommandons, autant que possible, d'utiliser Codium. Pour installer l'extension sous Codium, il faut d'abord la télécharger au lien ci-dessus, puis l'installer dans Codium.

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.

Spot

Une installation locale de Spot est disponible sous ~herbrete/public/linux/bin. Ajouter ce chemin à votre variable d'environnement PATH ou invoquez les outils en ajoutant le chemin d'accès complet, par exemple: ~herbrete/public/linux/bin/ltl2tgba --version. Il faudra également ajouter le chemin ~herbrete/public/linux/lib64/python3.6/site-packages à votre variable d'environnement PYTHONPATH pour accéder aux bibiothèques python de Spot.