Animation of formal specifications of information systems with RoZ and JazaGUIv3 (demo)
1 : Validation de Systèmes, Composants et Objets logiciels
(VASCO)
* : Auteur correspondant
Laboratoire d'Informatique de Grenoble
Laboratoire LIG - Bâtiment IMAG - 700 avenue Centrale, CS 40700 - 38058 Grenoble cedex 9 -
France
RoZ is a tool that translates a class diagram, enhanced with Z annotations, into a Z specification. This demo will present how this Z specification can be animated with the latest version of JazaGUI. JazaGUI is based on the jaza animator enhanced with a graphical user interface. This interface displays animation scenarios as a tree of method calls. It generates object diagrams from the current state of the animation, and uses the "why" feature of jaza to help explain animations which led to a failure. The tool is used to teach formal methods to Master's students.
Working group : HiFi (and IDM)
| Type : | : | typdoc_34556 |
| Langue du texte intégral | : | anglais |
| Date de production, écriture | : | 26/12/2024 |
| Thématiques | : | Posters et DEMO |
| Mots-Clés | : | animation of specifications ; integrated formal methods ; validation ; HiFi |
| PDF version | : |  PDF version |
- Poster
