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

Chapter 5
Real-Time Animator and Requirements
Traceability
Abstract According to the development life-cycle of a critical system, first of all
we emphasise on requirements traceability using a real-time animator. Formal mod-
elling of requirements is a challenging task, which is used to reasoning in earlier
phases of the system development and to make sure that the completeness, consis-
tency, and automated verification of the requirements. This is an initial step in the
proposed development methodology of the critical system development. The real-
time animation of a formal model has been recognised to be a promising approach
to support the process of validation of requirements specification. It is crucial to
get an approval and feedback when domain experts have a lack of knowledge of any
specification language, to avoid the cost of changing a specification at the later stage
of development. This chapter introduces a new architecture, together with a direct
and an efficient method of using real-time data set, in a formal model without gener-
ating the source code in any target language. This is a phase for validating a system
through domain experts in our development life-cycle methodology. The principle
is to simulate the desired behaviours of a given system using formal models in the
real-time environment and to visualise the simulation in some form appealing to
stakeholders. The real-time environment assists in the construction, clarification,
validation and visualisation of a formal specification.
5.1 Introduction
Formal methods aim to improve software quality and to produce zero-defect soft-
ware, by controlling the whole software-development process, from specifications
to implementations. In formal model development, they use top-down approaches
and start from high-level and abstract specifications, by describing the fundamental
properties of the final system. Requirements Engineering (RE) provides a frame-
work for simplifying a complex system to get a better understanding and to develop
the quality systems. The role of verification and validation is very important in the
development of safety critical systems. Verification starts from the requirements
analysis stage where design reviews and checklists are used for validation where
functional testing and environmental modelling are done.