Information Technology Reference
In-Depth Information
4.3.1.
Formal models
A formal model uses a syntax associated with a rigorous and non-ambiguous
semantics enabling us to carry out mathematical and logical reasoning. With rules
of deduction or inference
3
, it is possible to verify the particular properties of a
system specified with the help of these models. Finally, the formal models use an
abstract description of the system. This is why certain modeling approaches propose
refinement mechanisms to derive the concrete system.
Formal models can be classed according to the theories that they originate from
[MON 96] (sets, algebra types, automatons and high order typed logic) as are
discussed in the following sections.
4.3.1.1.
Set models
Set models are based on the theory of sets. They suit the specification of so-called
sequential systems. The most well known representatives of this family of models are:
the Z notation [SPI 88], the VDM language [JON 92] and the B method [ABR 96].
The Z notation not enabling complete refining of the specifications is restricted
to the functional specifications. This is why it is not accompanied by obligations
of particular proofs. Conversely, the VDM and B methods propose refinement
mechanisms involving proof obligations. B method being more elaborate, complete
and tooled, is undergoing a considerable expansion in the industrial sector. Indeed,
it is based on a process of progressive refinement leading to a practical description
that can be automated. The process of proof has to do with the coherence of the
mathematical model and on preservation of the properties of the initial model by the
successive refinements. Method B has a tool called
Atelier B
that includes a generator
of proof obligations and an assistant for proof.
4.3.1.2.
Algebra models
Algebra models, used for sequential and concurrent systems, use high-order and
algebra logic. Indeed, a system is modeled by using the concept of data abstract type
that correspond to a type of data class, the description of which is independent of any
implementation. The refinement is carried out by corresponding a practical type to
each abstract type by means of a function of practical expression. The refinement
mechanism used requires us to carry out certain proof, which ensures the coherence
between abstract and concrete types. The process of proof is often supported by tools
that use rewriting techniques [BAA 99], solving of equations [LEH 05] or recurrence.
The algebra models are very little tooled (
ACT ONE
[DEM 92],
LPG
[BER 00]);
this is why they are not used in practice, with the exception of
LOTOS
[EIJ 89],
which is considered a hybrid model combing the algebra mode of ACT ONE for
3 Rules producing new facts from assumptions and axioms.
