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
 
Search WWH ::




Custom Search