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...

ver descrição completa

Detalhes bibliográficos
Autor principal: Campos, José C. (author)
Outros Autores: Sousa, Nuno (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2018
Assuntos:
Texto completo:http://hdl.handle.net/1822/66789
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/66789
Descrição
Resumo: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.