MAKING FORMAL SPECIFICATIONS ACCESSIBLE THROUGH THE USE OF ANIMATION PROTOTYPING

Formal methods are mathematically based techniques used to specify the structure, function and behaviour of software-based systems. Proponen ts of such methods claim their use has many benefits. However, practic al experience has shown that non-specialists have much difficulty in w orking with formal specifications. Major problems are caused by the sy ntactic and semantic complexity of the rotation used. This paper descr ibes how formal specifications can be made understandable by, and acce ssible to, the non-specialist. It does this by showing the meaning of such specifications in computer-generated pictures - a technique we ca ll 'animation prototyping'.