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

Fig. 4.1 Formal methods based development methodology of critical system

of a system and to make explicit assumptions on which the safety of a system is
based. Once the developer reaches a general understanding of the problem, static
development proceeds to the formal requirements specification.

4.3.2 Formal Specification

The required security requirements are formally expressed as properties of the state-
based model that underlies the informal requirements. The categorised requirements
fragments describe through the set of formal notations in any specific modelling lan-
guage like Event-B [ 1 ], Z [ 66 ], ASM [ 11 ], VDM [ 9 ], RAISE [ 58 ], TLA + [ 44 ], etc.
Formal specification languages have a mathematical (usually formal logic) basis and
employ a formal notation to express the system requirements. The formal specifi-
cation is typically a mathematical based description of the system behaviour, using
state tables or mathematical logic. In this stage, more detailed requirements analysis
is carried out by building a formal specification. Using the formal notation, preci-
sion and conciseness of specifications can be achieved. Formal specification will