WildAniMAL - MAL Interactors Model Animator

Abstract

The IVY Workbench is a tool for modeling and analysis of interactive systems which has been developed at the Department of Informatics of the University of Minho (http://ivy.di.uminho.pt). It's a platform developed in Java, using a plugins mechanism. The available plugins include a set of editors (textual and graphical) and tools to analyse the behaviour of the models. The experience on using the tool has demonstrated the need for a model animator which could enable a first interactive evaluation of the models. Therefore this dissertation describes the design and implementation of WildAniMAL - a MAL (Modal Action Logic) interactors models animator – as a plugin for the IVY Workbench. The plugin uses the NuSMV model checker simulations capabilities, and enables users to explore the formal models interactively.

A IVY Workbench é uma ferramenta de modelação e análise de sistemas interativos que tem vindo a ser desenvolvida no Departamento de Informática da Universidade do Minho (http://ivy.di.uminho.pt). Trata-se de uma plataforma desenvolvida maioritariamente em Java, utilizando um mecanismo de plugins. Os plugins existentes incluem um conjunto de editores (em modo texto e gráfico), e de ferramentas de análise do comportamento dos modelos. A experiência de utilização da ferramenta tem, no entanto, demonstrado a necessidade de um animador de modelos que permita efetuar uma primeira validação interativa dos mesmos. Sendo assim, esta dissertação descreve o desenho e implementação do WildAniMAL – um animador de modelos de MAL (Modal Action-Logic) Interactors – como plugin para a IVY Workbench. O plugin usa as capacidades de simulação do model checker NuSMV, e permite aos utilizadores explorar os modelos formais de forma interativa.