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

There are several ways to validate a specification: to model a prototype of a sys-
tem, structured walk-through, transformation into a graphical language, animation,
and others. Each technique has a common goal, to validate a system according to
the operational requirements. Animation focuses on the observable behaviour of the
system [ 51 ]. The principle is to simulate an executable version of the requirements
model and to visualise exact behaviours of the actual system. Animators use finite
state machines to generate a simulation process which can be then observed with the
help of UML diagrams, textual interfaces, or graphical animations [ 42 ]. Animation
can be used in the early stage of development during the elaboration of the specifi-
cation. As a relatively low cost activity, animation can be frequently used during the
process to validate important refinement steps.
The final code generation process consists of two stages: final level formal spec-
ifications are translated into programs in a given programming language, and then
these programs are compiled. Nevertheless, all approaches which support a formal
development from specification to code must manage several constraining require-
ments, particularly in the domain of embedded software where specific properties
on the code are expected likes timeliness, concurrency, liveness, reactivity, and het-
erogeneity [ 36 ]. All these properties can be represented abstractly. Finally, it is im-
possible to use the real-time data in the early stage of formal development without
compiling the source code in any target language.
Based on our various research experience using formal tools in industrial require-
ments ( verification and validation ) and our desire to disseminate formal methods,
we have imagined a new approach to present an animated model of specification
using real-time data set, in the early stage of formal development [ 41 ]. Animation
of formal specification is not a new idea, but capture the real-time data and perform
animation of formal methods in the real environment is a new idea. In this work,
we present an architecture which allows to easily develop the visualisations for a
given specification with support of existing tool Brama [ 48 ]. Here, we describe an
approach to extend an animator tool which will be useful to use the real-time data
set. Now, present time all the animation tools use a toy data set to test the model
while we are proposing a key idea to use the real-time data set with the model with-
out generating the source code in any target language (C, C++, VHDL, etc.). It can
help a specifier to gain confidence that the model that is being specified, refined and
implemented, does meet the domain requirements.
This architecture supports state-based animations, using simple pictures to rep-
resent a specific state of Event-B [ 1 ] specification, and transition-based animations
consisting of picture sequences by using real-time data set. A sequence of pictures
is controlled by the real-time data set, and it presents an actual view of a system.
Before moving on we should also mention that there are scientific and legal appli-
cations as well, where the formal model based animation can be used to simulate
(or emulate) certain scenarios to glean more information or better understandings
of the system requirements. Moreover, this real-time animation technique is very
helpful to assist in the certification process to analyse an evidence-based validation
in a critical system.