Information Technology Reference
In-Depth Information
the description of abstract data types to the algebraic model CCS [MIL 80] for
specification of the behavior of processes and their interactions. This combination of
models adapts LOTOS language to the description of concurrent systems.
4.3.1.3.
Models based on extended states automatons
The models based on extended states automatons [HOP 07] are concerned with
changes in the state of the system; they are therefore adapted to the specification
of the dynamic and reactive systems. The system is modeled by processes
communicating via messages or shared variables, where each process is an extended
finished state machine evolving by transitions The models based on extended states
automatons associate an algebra model for the static description of the system in
their specification. They inherit the refinement and proof mechanisms. The dynamic
part of the specification offers the possibility of the specification using a temporal
logic in order to verify the properties at a high level of abstraction via the model
checking verification technique (see section 4.3.2.2) or by techniques of proof (see
section 4.3.2.1). The models that are based on automatons with extended states,
which are the most well known, are
SDL
[ELL 97] and
Estelle
[EST 97].
4.3.1.4.
Models based on the logic of a higher order
The logic of a higher order is a logic that has a high level of expressivity as it
enables us to consider a predicate as an object that can vary or even be used as an
argument of a function or a predicate [MON 96]. This logic is combined with a type
system. It proposes a different mechanism by extraction of the program that enables
it to simultaneously develop a functional program and to prove it. The high degree
of expressivity offered by the logic of higher order enables it to specify a variety of
systems but increases the complexity of the proof process. Among such models we
can cite
Coq
[HUE 07],
HOL
[GOR 93] and
Isabelle
[PAU 93].
4.3.2.
Formal verification
Formal verification consists of verifying that the desired properties are respected
by a given system (model). This verification is done by confronting a formal
expression of the properties of a system with a mathematical model, based on a
formal language, which represents the system. The mechanism of verification must
examine whether the desired properties are met by the behaviors of the system. There
are two main approaches to formal verification:
theorem proof
and
model checking
.
4.3.2.1.
Theorem proof
Introduced by Hoare [HOA 69], this approach is based on mathematical proof.
It involves describing the system and its properties in an axiomatisable model of
semantics (expressed by axioms) and demonstrating that the properties can be
