Information Technology Reference
In-Depth Information
Indeed most existing frameworks focus on the correctness or the adaptation of
applications; we focus on generic properties.
In this context, introduction of mechanised proofs will increase confidence in
the properties of the component model and its adaptation procedures. We start
from a formalisation close to the component model specification and implemen-
tation; then we use a framework allowing us to express properties in a simple
and natural way. This way, we can convince the framework programmer and the
application programmer of the safety of communication patterns, optimisations,
and reconfiguration procedures.
We write our mechanised formalisation in Isabelle/HOL but we are convinced
that our approach can be adapted to other theorem provers. The generic meta-
logic of Isabelle/HOL constitutes a deductive frame for reasoning in an object
logic. Isabelle/HOL also provides a set of generic constructors, like datatypes,
records, and inductive definitions supporting natural definitions while automat-
ically deriving proof support for these definitions. Isabelle has automated proof
strategies: a simplifier and classical reasoner, implementing powerful proof tech-
niques. Isabelle, with the proof support tool Proofgeneral, provides an easy-
to-use theorem prover environment. For a precise description of Isabelle/HOL
specific syntax or predefined constructors, please refer to the tutorial [20].
We present here a framework that mechanically formalizes a distributed hi-
erarchical component model and its basic properties. We show that this frame-
work is expressive enough to allow both the expression of component semantics
and the manipulation of the component structure. Benefiting from our experi-
ences with different possible formalisations, and from the proof of several compo-
nent properties, we can now clearly justify the design choices we took and their
impact
1
. The technical contributions of this paper are the following:
- formal description in Isabelle of component structure, mapping component
concepts to Isabelle constructs,
- definition of a set of basic lemmas easing the proof of component-related
properties,
- additional constructs and proofs to ensure well-formedness of component
structures,
- proposal for a definition of component state, and runtime semantics for com-
ponents communicating by asynchronous request-replies,
- application to the design and first proofs about component reconfiguration.
The remainder of the paper is organised as follows. Section 2 gives an overview
of the context of this paper: it positions this paper relatively to related works
and previous works on the formalisation of the GCM component model, which
is also described in Section 2.2. Section 3 presents the formalisation of the com-
ponent model in Isabelle/HOL highlighting design decisions and their impact on
the basic proof infrastructure. We then summarize a semantics for distributed
components with its properties, and present a few reconfiguration primitives in
Section 4.1. Section 5 concludes and presents future directions.
1
The GCM specification framework is available at
www.inria.fr/oasis/Ludovic.Henrio/misc
