Formal specification : Alloy vs TLA+ #9
Description
A propos de vous
- Prénom Nom: Guillaume ANDRIEU
Description de votre sujet.
- Nom de la techno : TLA+
- Techno alternative: Alloy
Les développeurs aiment coder, et codent parfois trop, et trop vite. Pour des algorithmes sensibles, incluant par exemple des questions de concurrence, il est facile de se tromper sur la manière de s'y prendre, et de ne pas être en mesure de prévenir des cas d'erreur, même en écrivant des tests poussés.
Des langages de vérification formelle se développent depuis le début des années 2000: ils permettent d'écrire une spécification qui est ensuite vérifiée par un solveur s'assurant que des invariants sont effectivement invariants.
TLA+ se base sur une notion de machine à états, et excelle à décrire des sytèmes évoluant dans le temps. Alloy est plus basé sur des sytèmes statiques et de la logique relationnelle.
Pour référence:
- https://link.springer.com/chapter/10.1007/978-3-662-43652-3_3
- https://arxiv.org/pdf/1603.03599.pdf
- https://www.researchgate.net/publication/220694084_Software_Abstractions_logic_language_and_analysis
- https://lamport.azurewebsites.net/tla/book.html?back-link=learning.html#book
Détails
-
Exercices du matin: familiarisation avec les concepts et le langage
-
Exercice de l'après-midi: fournir la spec formelle d'un système, sous forme de jeu avec déverrouilage d'étapes qui complexifie l'algo à spécifier au fur et à mesure
-
Tags (e.g: angular, android, web, iot) : formal specs
-
Disponibilité (e.g: ASAP, avant/aprés XXX): ?