Comment utiliser TLA+ avec arKITect
Il est maintenant possible d’interfacer arKItect avec des environnements de preuve formelle. Aujourd’hui nous parlons de l’interface TLA+.
Il y a maintenant la possibilité de configurer un export TLA+ à partir d’un modèle arKItect. Cela peut aider à valider vos exigences au début du processus de conception.
TLA+ est un langage de haut niveau pour la modélisation de programmes et de systèmes, en particulier concurrents et distribués. Il repose sur l’idée que la meilleure façon de décrire les choses avec précision est d’utiliser des mathématiques simples. TLA+ et ses outils sont utiles pour éliminer les erreurs de conception fondamentales. 📌Regardez ce lien : https://lamport.azurewebsites.net/tla/tla.html
arKItect est le modèle DSML et DSL le plus agile au monde. C’est un environnement à faible code.
Que ce soit avec 3SE ou SEA, deux DSL prêts à l’emploi pour l’ingénierie des systèmes, ou avec un DSL personnalisé, vous pouvez interfacer les descriptions des exigences opérationnelles avec TLA+.
Cette approche semble très pertinente lorsque vous travaillez sur les états du système.
Dans la présentation ci-dessous, vous trouverez un teaser expliquant l’approche. N’hésitez pas à nous contacter pour plus d’informations.