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

of the entire system mechanics, the failure mechanisms, and their manifestation in
the signatures. The accuracy of the system is fully dependent on the feature or pa-
rameter values being used. Feature extraction involves simplifying the amount of
resources required to describe a large set of data accurately. When performing anal-
ysis of a complex data one of the major problems stems from the number of vari-
ables involved. Analysis with numerous variables generally requires a large amount
of memory and computation power or a classification algorithm which overfits the
training sample and generalises poorly to new samples. Feature extraction is a gen-
eral term for methods of constructing combinations of the variables to get around
these problems while still describing the data with sufficient accuracy. Collecting
measured data and processing these data to accurately determine model parameter
values is an essential task for the complete characterisation of a formal model.
5.5.3 Database
The database unit is optional. It stores the feature or parameter values in a database
file in any specific format. This database file of parameters or features can be used
in future to execute the model. Sometimes, feature extraction algorithms take more
time to calculate the parameters or the features. In such a situation, modeller can
store the parameters or the features in a database file to test the model in the future.
A modeller can also use the extracted parameters or features directly in the formal
model, without using the database.
5.5.4 Graphical Animations Tool: Macromedia Flash
The animated graphics are designed in the Macromedia Flash tool [ 44 ]. Macrome-
dia Flash, a popular authoring software developed by Macromedia, is used to create
vector graphics-based animation programs with high graphic illustrations and sim-
ple interactivity. Here, we use this tool to create an animated model of the physical
environment and to use the Brama plug-in to connect the Flash animation and the
Event-B model. This tool also helps to connect the real-time data set to a formal
model specification using some intermediate steps and finally makes the animated
model closer to the domain expert expectations.
5.5.5 Animator: Brama Plug-in
Brama [ 48 ] is an animator for Event-B specification, which is designed by ClearSy.
Brama is an Eclipse plug-in suit and Macromedia Flash extension that can be used
with Windows, Linux and MacOS for Rodin platform [ 46 ]. Brama can be used to