Information Technology Reference
In-Depth Information
Component Behaviour.
In our model, the primitive components represent
the business logic and can have any internal behaviour. Primitive components
treat all the requests they receive, choosing a processing order and the way
to treat them. On the other hand, the behaviour of a composite component is
more restricted: it is strictly defined by its constituent subcomponents and the
way they are composed. A composite component serves its requests in a FIFO
manner, delegating them to other components bound to it. A delegated request
is delivered unchanged to the target component. Once the service of a request
is finished, the produced result is stored in the computed results for future use.
It can then be transmitted to other components, as determined by the reply
strategy [17, 14].
2.3
Positioning
This paper provides formalisation of hierarchical components and their structure.
At our level of abstraction, this structure is shared by several component levels
like Fractal, GCM, and SCA. However most implementations of SCA (except
FraSCAti) do not instantiate the component structure at runtime. By contrast,
to allow component introspection and reconfiguration at runtime, we consider a
specification where structural information is still available at runtime. This en-
ables adaptive and autonomic component behaviours. Indeed, component adap-
tation in those models can be expressed by reconfiguration of the component
structure. For example, reconfiguration allows replacement of an existing com-
ponent by a new one, which is impossible or very dicult to handle in a model
where component structure disappears at runtime.
Most existing works on formal methods for components focus on the support
for application development whereas we focus on the support for the design and
implementation of component models themselves. To our knowledge, this work
is the only one to support the design of component models in a theorem prover.
It allows proving very generic and varying properties ranging from structural
aspects to component semantics and component adaptation.
A formalisation of our communication model along with the component se-
mantics appear in [13]. An extended version of the formal semantics is presented
in [14], providing formalisation of one particular reply strategy. Other possible
strategies are discussed in [17]. Compared to our previous works, this paper relies
on the experience gained in specification and proof and demonstrated in [13, 14]
to design a framework for supporting mechanised proofs for distributed compo-
nents. In particular this paper focuses on the handling of component structure,
on a basic set of lemmas providing valuable tooling for further proof, and the
illustration of the presented framework to prove a few properties dealing with
component semantics and reconfiguration.
3 Formalisation of Component Model in Isabelle/HOL
Our component model is a subset of the GCM component model, but with a pre-
cisely defined structure and semantics. It incorporates hierarchical components
