L'objectif de ce bureau d'étude est de donner une sémantique formelle en Isabelle au langage de description d'automates défini lors du bureau d'étude du cours de modélisation.

La sémantique du DSL sera définie par une transformation Acceleo qui génère une théorie Isabelle, de façon similaire à la génération de code Java que vous avez déjà traitée.

Pour faciliter les preuves, vous disposez d'une classe Machine qui définit un certain nombre de fonctions et de prédicats, avec des théorèmes déjà démontrés. Le type que vous génèrerez pour chaque modèle de votre DSL devra instancier cette classe :

Afin de factoriser les définitions, les entrées d'une machine sont encodées avec des entiers naturels. Vous pouvez définir les entrées de la machine pour laquelle vous générez du code de manière symbolique. Voici ce que donnerait la théorie générée pour le régulateur de vitesse :

À partir de ce modèle, on devra pouvoir prouver certaines propriétés. Par exemple, le fait qu'il est possible d'activer la régulation de vitesse à partir de l'état initial en utilisant les entrées on et cruise :

ou que lorsqu'on appuie sur les freins, la régulation se désactive :

ou encore (plus difficile) qu'il est impossible d'activer la régulation de vitesse sans utiliser l'entrée cruise :