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: slides
  2. Test vs. Model-checking vs. Proof: exercices
  3. Formal modelling: slides / exercices

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.