Critical System Development Methodology - Using Event-B for Critical Device Software Systems - page 71

proposed system design and expected system behaviour according to the domain
experts using real-time environment in early phase of the development without gen-
erating the source code.
4.4.1 Improving Requirements
Using our methodology to capture requirements provides a simple validation check
in early stage of critical-system development. Requirements expressed in a formal
notation can also be analysed early to detect inconsistency and incompleteness for
removing errors that are normally found later in the development process.
4.4.2 Reducing Error Introduction
Formalised requirements prevent misunderstandings due to ambiguities that lead
to an error introduction. As development proceeds, compliance can be continually
checked using a formal analysis to ensure that errors have not been introduced.
A further advantage of using our methodology at the requirements level is the ability
to derive or refine from these requirements the code itself, thus ensuring that no error
is introduced at this stage. Alternatively their use at the requirements level allows
formal analysis to establish correctness between requirements and final generated
source code of the complex systems.
4.4.3 Improving Error Detection
Out methodology can provide exhaustive verification at whatever levels it is applied:
high level requirements or low level requirements. Exhaustive verification means
that the whole structure is verified over all the possible inputs and states. This can
detect errors that would be difficult or impossible to find using only a test based
approach.
4.4.4 Reducing Development Cost
Our proposed methodology is based on formal techniques. In general, software er-
rors are less expensive to correct the earlier in the development life-cycle they are
detected in the critical systems. The effort required to generate formal models is
generally more than offset by the early identification of errors. That is, when for-
mal methods are used early in the life-cycle, they can reduce the overall cost of the
project development. When requirements have been formalised, the costs of down-
stream activities are reduced. Formal notations also reduce cost by enabling the
automation of verification activities.