Real-Time Animator and Requirements Traceability - Using Event-B for Critical Device Software Systems - page 85

Fig. 5.1 A functional architecture to animate a formal specification using real time data set without
generating source code

• Animation always focuses on the behavioural aspects of a system. However, non-

functional requirements, such as reliability, cannot be animated from require-
ments. The mean life function, such as the mean time to failure (MTTF), is widely
used as the measurement of a product's reliability and performance. This value
is often calculated by dividing the total operating time of the units tested by the
total number of failures encountered. Hence, reliability is usually measured by a
rate. For example, the reliability of a system is 95 %, then how it is possible to
measure that the reliability of that system is 95 % through animation.

5.5 Proposed Architecture

Figure 5.1 depicts a functional architecture that can use the real-time data set to
animate a formal model without generating a source code in any target language
(C, C++, VHDL, etc.). This architecture has six components: Data acquisition and
preprocessing unit; Feature extraction unit; Database; Graphical animations tools;
Interfacing plug-in; and formal specification model. All these six components can
use any particular tool for building a prototype for realising the concepts of a real-
time animator.
We have used some existing tools to build a prototype model of this proposed ar-
chitecture. Figure 5.2 presents prototype implementations in order to understand the
different development phases of the real-time animator. This architecture is applica-
ble to building an animation tool for any formal modelling languages like VDM, Z,
TLA + , etc. Here, we present an equivalent architecture of the real-time animator in
the context of Event-B formal modelling language. The prototype architecture has
six components: Data acquisition and preprocessing unit; Feature extraction unit;
Database; Graphical animations dedicated tool: Macromedia Flash; a Formal model
animation tool Brama plug-in to interface between Flash animation and Event-B
model; and formal specification system Event-B.