IF311 - Conception formelle des logiciels

Ce cours étudie la conception formelle des logiciels à l'aide du model-checking.

Intervenant

Frédéric Herbreteau

Documents

Documents de cours

1. Introduction: slides
   • En complément vidéo d'introduction à la vérification (par Leslie Lamport)
2. Test vs. Model-checking vs. Proof: exercices
3. Introduction to formal modeling slides / exercicses
4. Specification in Linear-time Temporal Logic (LTL): slides / exercises
5. Formal design of a concurrent mutex algorithm: exercises
6. Fairness: slides / exercises
7. LTL model-checking: slides / exercises

Devoirs

1. Modeling a transfer between bank accounts, please refer to thor for more informations
2. Debugging a Java Producer-Consumer program, please refer to thor for more informations

Ressources

Le blog de Ron Pressler:

• Why writing correct software is hard
• Part 1: The principles of TLA+
• Part 2: The + in TLA+
• Part 3: The (temporal) logic of actions
• Part 4: Order in TLA+

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.