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

of works have been done over the last few decades in this area while the idea was
originally proposed by Balzer et al. [ 3 ]. The contributions mainly differ by (a) how
far the model is from the underlying requirements, (b) how far the visualisation
is from phenomena within the software environment, (c) how the simulation works
(through direct execution of the model or preliminary translation to some executable
form), and (d) how interactive and controlled the simulation can be [ 51 ]. Bloomfield
et al. [ 7 ] had presented a case study in which a simple prototype for nuclear reac-
tor protection was modelled in VDM [ 5 ], whereas a part of the safety assessment
process was presented using Prolog [ 13 ] animation. Another interesting study of the
industrial use of animation in the analysis of a formal model of information flow in
dynamic virtual organisations (VOs) is presented by John et al. [ 19 ]. VDM tool is
used for developing the formal model of virtual organisation (VO) structure. This
development also supports interaction with the model without requiring exposure
to the formalism. All kinds of simulation tools for Requirements Engineering (RE)
with compressive comparison study have been presented by Schmid et al. [ 47 ].
A reference model for requirements and specifications is given by Gunter et
al. [ 24 ]. This model is based on mainly five artifacts W, R, S, P, and M for ap-
plying formal methods to the development of user requirements and their reduction
to a behavioural system specification. This paper presents the shared phenomena
that defines an interface between system and environment.
Run-time technique for monitoring requirements satisfaction is presented in [ 17 ,
18 ], where requirements are monitored for violations, and system behaviour dynam-
ically adapted the new behaviours. New introduced behaviours change the system
requirements, which should meet the higher-level goal. Our proposed approach is
based on monitoring of the animation, which is controlled by the proved formal
specifications and real-time data sets. According to our literature survey, none of
the existing approaches discuss to construct a formal specification based prototype,
which can use a real-time data set to test the validation of the formal specifications
for developing any critical systems like avionic and medical systems. Most of the
existing tools are used a toy-data set for validating the formal specifications. Limita-
tions of existing tools are that they cannot support real-time environment to capture
the data set for testing. We have proposed an architecture for real-time animation
using formal specification [ 41 ], which can be used for real-time animation for any
existing animation tool and formal language. We have given the prototype model
of this framework for Event-B specification. This tool is very helpful to show the
real-time system behaviour from a formal specification and meets stakeholders re-
quirements. Moreover, it bridges the gap between different kinds of domain experts.
It can help a formal model designer to gain confidence that the formal model that is
being designed, refined in an incremental way and finally implemented, does meet
the domain requirements. The real-time animation tool is very helpful for evidence-
based validation as well as in the certification process. This technique uniformly
establishes what to check and how to check it and gives certain evidence of correct-
ness.