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

4.3.4 Formal Validation

Formal validation phase is the process of determining the degree to which a model
is an accurate representation of the real world from the perspective of the intended
uses of the model that is not covered by the formal verification. It consists of the
identification of a subset of the formalised requirements fragments for an automatic
validation analysis:
•

Validation ensures that the model meets its intended requirements in terms of the
methods employed and the results obtained.

• The ultimate goal of model validation is to make the model useful in the sense

that the model addresses the right problem, provides accurate information about
the system being modelled, and to make the model actually used.

Model checking [ 17 ] is a complementary technique for validation and verifica-
tion of a formal specification. Model checkers attempt to make formal techniques
easier to use by providing a high degree of automation at the expense of generality.
Inputs to a model checker are typically a finite state model of a system, along with
a set of properties that are expected to be preserved by the system. Properties to be
verified can be usually categorised as one of the following:

1. Correct sequences of events
2. Proper consequences of activities
3. Simultaneous occurrences of particular events
4. Mutual exclusion of particular events
5. Required precedence of activities

The model checker explores all the possible event sequences of a model to de-
termine that system is always holding required safety properties. If properties hold,
the model checker confirms the correctness of a system. If a property fails to hold
for some possible event sequences, the tool produces counter-examples, i.e., traces
of event sequences that lead to failure of the property [ 46 ].
In Fig. 4.1 , this phase also presents that it provides a feedback information to
the formalisation phase when a model is not satisfying expected behaviour of a
system. This feedback information helps to modify the developed formal model
and verify it through the formal verification phase and validation through a model
checker tool [ 17 , 46 ]. This cyclic process for finding a correct model is applied to
continue until not to find the correct formal model according to the expected system
behaviour.

4.3.5 Real-Time Animation Phase

This phase is a new validation technique to verify the formal model in the real-
time environment using real-time data set instead of using a toy-data set. A detailed
description about the architecture of the real-time animator is available in Chap. 7