Survey and Consistency Checking of Formal Requirements Animations

Formal requirements are written in mathematical language enabling powerful verification but are complex to validate by domain end-users or stakeholders. Requirements animations answer this problem by providing techniques to explore system traces and interact with them using domain specific graphical views and controls. Most formal tools include features to ease the development of such animations for different formal notations. However, to be sound, animations require to be carefully designed. This paper analyses major animation frameworks for system design in order to clearly identify their validation scope and purpose. Based on this, it identifies and discusses a number of checks to make sure an animation is well-designed. Different case studies are used as illustrative support.