Animation prototyping of real-time systems specifications

Describes how animation prototyping can be applied to the formal specifications of real-time safety-critical systems as an aid to client/specifier communication. In particular, a method is defined for stating specifications in a structured hierarchical manner, while enabling the resulting decomposition to be mathematically verified. The method enables sequential ordering to be associated with VDM specifications. The methods by which VDM specifications generate animated displays of the behaviour of the system being specified are defined, and how it has been applied to a real-time embedded system is described