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

in the architecture for using the real-time data set to achieve the adaptability and
confidence on a formal model. Moreover, this architecture may provide validation
for the formal model with respect to the high level specifications according to the
domain experts (i.e. medical experts). At last, this proposed architecture should be
adaptable to various target platforms and formal models techniques (Event-B, Z,
Alloy, TLA + ,etc.).
Our approach has involved for designing and using of the real-time animator for
executing a formal specification to validate actual requirements. The main objectives
of our work are to promote the use of such kind of real-time animator [ 41 ] to bridge
the gap between software engineers and stakeholders to build a quality system, and
to discover all ambiguous informations from the requirements. Moreover, this tool
helps to verify the correctness of behaviour of a system according to the stakeholders
requirements. The formal verification and evidence based testing using an animation
offer to obtain that challenge of complying with FDA's QSR, ISO/IEC and IEEE
standards quality system directives [ 11 , 12 , 16 , 32 , 33 ] and help to get certification
for highly complex critical systems.
A key feature of this validation as it is full automation and animation of spec-
ification in the early stage of formal development. The case study (see Chap. 9 )
has shown that requirements specifications could be used directly in the real-time
environment without modifications for automatic test result evaluation using our
approach. Moreover, there are scientific and legal applications as well, where the
formal model based animation can be used to simulate (or emulate) certain sce-
narios to glean more information or better understandings of the system and assist
to improve the final given system. Main contributions of proposing this real-time
animator tool are,

• to reduce the gap between software engineers and stakeholders requirements us-

ing real-time animator and easy to explain model behaviour to the domain experts
as well stakeholders;

•

a real-time animation of a specification supplements inspection and reasoning
as means for validation. This is especially important for the validation of non-
functional behaviour;

• a real-time animation technique is available in early phase of the system devel-

opment life-cycle, which can be used to correct validation errors immediately,
without incurring costly redevelopment;

• ambiguous and incomplete requirements can be clarified and completed by hands-

on experience with the specifications using our approach;

•

the goal-oriented animation for evidence based expectation to verify particular
portions of a behaviour model;

• animation can be helpful for incremental model building and analysis of a com-

plex system;

• helps to domain experts to analyse work process guidelines;

• animator assists to regulatory agencies and helps to meet ISO/IEC and IEEE stan-

dards;