Information Technology Reference
In-Depth Information
that communicate via asynchronous requests and replies. We start with formalis-
ing the structure of our components. Based on the structure defined, we present
some of the various
infrastructure
operations that allow us to manipulate the com-
ponents for proving properties. Then we formalise additional constructs to define
component's state and request handling, and correctness of a component assem-
bly. Finally we provide a set of very useful lemmas dealing with component struc-
ture and component correctness.
3.1
Component Structure
As we have seen in Section 2.2, a component in our model can either be a
composite or primitive. A composite component comprises one or more subcom-
ponents. On the other hand, a primitive component is a leaf-level component
encapsulating the business logic.
datatype
Component = Primitive Name Interfaces PrimState
| Composite Name Interfaces (Component list) (Binding set) CompState
The above Isabelle/HOL datatype definition for
Component
s has two construc-
tors
Primitive
and
Composite
. We present below the various elements that
make up the structure of our components.
Name: Each component has a unique name. We use this name as the compo-
nent identifier/reference.
Interfaces: Each component has a number of public interfaces. All commu-
nication between components is via public interfaces. An interface can be either
client or server and by construction a component cannot have two interfaces
with the same name.
Subcomponents: Composite components have a list of subcomponents, given
by the
Component list
parameter. Primitive components do not have subcom-
ponents.
Bindings: In composite components, a binding allows an interface of one
component to be plugged to an interface of a second component.
(N1.i1,
N2.i2)
∈
bindings
if the interface
i1
of component
N1
is plugged to the in-
terface
i2
of
N2
where
N1
or
N2
can either be component names or
This
if the
plugged interface belongs to the composite component that defines the binding.
State: All components, primitive or composite have an associated state.
Component state is discussed in more detail in Section 3.3.
Design decisions.
In the Isabelle/HOL formalisation we chose to include the
name of the component into the component itself. Like for interfaces, a first
intuitive approach could be rather to define subcomponents as mappings from
names to components. There are, however, major advantages to our approach.
When we reason about a component we always have its name, which makes
the expression of several semantic rules and lemmas more natural. The main
advantage of maps is the implicit elegant encoding of the uniqueness of
Name
(s).
As mentioned before,
Name
(s)are used as component references. Unfortunately,
this advantage of maps is quite low in a multi-layered component model because