Abstract
In this paper, we present ViBBA (Visual Bean Based Animator), a toolbox supporting the automatic model driven animation consisting
in automatically derivingscenarios exposing critical system behaviors from requirements specifications, and animating those
scenarios through a graphical interface. ViBBA allows visual constructionof 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 checkerSpin. 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.
[download the pdf file]