Information Technology Reference
In-Depth Information
lemma
upd_names_eq:
CL^(getName c2)= Some c1; getName'(cpSet c2)=getName'(cpSet c1)
=
⇒
getName'(cpListset CL) = getName'(cpListset (CL<-c2))
4.2
Reconfiguration
Reconfiguration represents all the transformations of the component structure
or content that can be handled at runtime. We consider here mainly structural
reconfiguration, which includes changes of the bindings, and of the content of a
component. For example replacement of a primitive component by a new one is
a form of reconfiguration that allows evolution of the business code.
In Fractal or GCM, configuration primitives are bind/unbind to manipulate
bindings, add/remove to change the set of subcomponent of a composite com-
ponent; also it is possible to start/stop a component.
Our framework enables reasoning on reconfiguration primitives and behaviour
of a reconfigured component system. We illustrate below a few encodings of re-
configuration primitives and some theorems that can be proved in Isabelle/HOL
thanks to our framework.
We illustrate reconfiguration capacities of our approach by defining two re-
configuration primitives and proving two related lemmas. But beforehand, we
define the notion of
complete component
.
Completeness.
Similarly to [6], we say that a composite component is complete if
all interfaces of its sub-components and all its internal interfaces are bound. This
can be easily defined in Isabelle by the following primitive recursive predicate.
primrec
Complete::Component
⇒
bool
where
Complete (Primitive N itf s) = True |
Complete (Composite N itf sub bindings s) =
(
∀
C
∈
set sub. allExternalItfsBound C bindings)
∧
(allInternalItfsBound (Composite N itf sub bindings s) bindings)
∧
(CompleteList sub)
Here,
allInternalItfsBound C b
checks that all external interfaces of
C
are
bound by bindings
b
,and
allExternalItfsBound C b
that all internal inter-
faces of
C
are bound by bindings
b
. Finally, similar to
cpListlist
in Section
3.2,
CompleteList
recursively checks that all subcomponents are complete.
As there is no notion of optional interface in our model, this definition is really
straightforward. For a complete component, any request emitted by a component
will arrive at a destination component.
Unbind primitive.
The unbind primitive removes one of the bindings defined by
a composite component.
primrec
unbind:: Component
⇒
Binding
⇒
Component
where
unbind (Primitive N itf s) b = (Primitive N itf s) |
unbind (Composite N itf sub bindings s) b =
(Composite N itf sub (bindings-{b}) s)
