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

5.3 Related Work
Traceability is a necessary system characteristic as it supports software manage-
ment, software evolution, and validation [ 21 ]. Traceability approaches help for un-
derstanding the complexity of the problems and assist for capturing, tracking and
verification of the actual requirements during the software life-cycle. We believe
that the established use of animation approaches should explicitly include trace-
ability support to provide more benefits on developing software for medical and
automotive domains. An interesting related work for the traceability is presented
in [ 2 , 21 ], where the authors review the most-recent advances techniques for trace-
ability and also survey on tracing approaches in traditional software engineering.
Prototype refers to an incomplete version of the system development, which
simulates only few aspects of the final system when requirements are indefinite
and system behaviour is unclear [ 14 ].Theprototypeisonlyusedtobeclarified
and validated requirements. The experiences gain from prototypes are helping to
produce a quality system and the requirements specification document. The proto-
types work very well for only small parts of the complex problems. Various kinds
of traditional techniques are used to build a rapid throwaway prototype; these in-
clude functional and logic programming languages, simulation techniques, object-
oriented languages, and visual programming languages.
A prototype of executable formal specifications is used to bridge the gap between
a traditional software prototyping and formal methods. An executable formal spec-
ification is considered as an abstract program which enables abstract requirements,
designs formulation, explored and validated at an early stage of the system develop-
ment [ 20 ]. Such kinds of prototyping techniques help to discover behaviour of the
system interacting with its environment that can be observed before it exists in the
actual system. Validation of a system assists to design formal documentation using
the specification descriptions of system. In few cases, an executable specification
forms only relevant document for all phases of the system development, such as in
the use of executable specifications with transformational approaches [ 4 ].
Goguen and Meseguer [ 22 ] have proposed a novel approach for constructing a
prototype using formal specification. They advocated the use of an algebraic specifi-
cation language named OBJ, which can be executed by interpreting the equations of
the OBJ specification as a left-to-right term rewriting system. Since several, attempts
have been made to execute formal notations for rapid prototyping. Siddiqi et al. [ 49 ]
have divided these attempts into three categories. First category belongs to the use
of functional and logical programming languages for the construction of the proto-
types [ 27 , 35 , 38 , 50 ]. Second category is distinguished by “specially designed and
specific purpose” executable specification languages that are usually embedded in
an existing programming language which provides the execution mechanism [ 28 ].
Last category can be characterised as the development of an environment for the
automatic prototyping of specifications. Siddiqi et al. [ 49 ] have proposed distinct
approach for supporting environment, which combines the benefits of a formal sys-
tem specification and its subsequent execution via rapid prototype model.
Animation is a simulation technique which is used to execute a model and shows
the animation in the visual form using a formal model of a given specification. Lots