ViBBA: A Toolbox for Automatic Model Driven

In this paper, we present ViBBA (Visual Bean Based Animator), a toolbox supporting the automatic model driven animation [7] consisting in automatically deriving scenarios exposing critical system behaviors from requirements specifications, and animating those scenarios through a graphical interface. ViBBA allows visual construction of graphical animators and scenarios animation. It is integrated with the ATGT [5], that automatically generates scenarios (in XML format) from Abstract State Machines (ASMs) by exploiting counter example generation capability of the model checker Spin. The operation of ViBBA is shown by means of an example of formal specification where scenarios are automatically generated from the model and then animated