The MAL Interactors Animator: Supporting model validation through animation

The IVY workbench is a model checking based tool for the analysis of interactive system designs. Experience shows that there is a need to complement the analytic power of model checking with support for model validation and analysis of verification results. Animation of the model provides this suppo...

Full description

Bibliographic Details
Main Author: Campos, José C. (author)
Other Authors: Sousa, Nuno (author)
Format: conferencePaper
Language:eng
Published: 2018
Subjects:
Online Access:http://hdl.handle.net/1822/66789
Country:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/66789
Description
Summary:The IVY workbench is a model checking based tool for the analysis of interactive system designs. Experience shows that there is a need to complement the analytic power of model checking with support for model validation and analysis of verification results. Animation of the model provides this support by allowing iterative exploration of its behaviour. This paper introduces a new model animation plugin for the IVY workbench. The plugin (AniMAL) complements the modelling and verification capabilities of IVY by providing users with the possibility to interact directly with the model.