Information Technology Reference
In-Depth Information
Let C be the parallel composition of a number of disjoint components C i ,
i =1 ...k . A glue program for C is a process P that makes calls to a set of X of
provided methods of C . The composition C [ X ] P of C and P is defined similarly
to the alphabetized parallel composition in CSP [30] with interleaving of events.
The gluing composition is defined by hiding the synchronized methods between
the component C and the process P. We have proven that ( C [ X ] P ) \X is a
component, and studied the algebraic laws of the composition of processes and
components. The glue composition is illustrated in Fig. 5, where in Fig. 5(a)
C 1 and C 2 are two one-place buffers and P is a process that keeps getting the
item from C 1 and putting it to C 2 . In Fig. 5(b), the get of C 1 and put of C 2
are synchronized into an atomic step by component M ;and M proves method
move () {get 1(; y ); put 2( y ;) } , that process P calls.
get 2
put 1
C 1
C 2
put
get
get 1
put 2
C1
C2
M
move
get1
put1
P
( a )
P
( b )
Fig. 5. (a) Gluing two one-place buffers forms a three-place Buffer, (b) Gluing two
One-place buffers forms a two-place buffer
An application program is a set of parallel processes that make use of the
services provided by components. As processes only interact with components
via the provided interfaces of the components, interoperability is thus supported
by the contracts which define the semantics of the common interface descrip-
tion language (IDL), even though components, glue programs and application
programs are not implemented in the same language. Analysis and verification
of an application program can be performed in the classical formal frameworks,
but at the level of contracts of components instead of implementations of com-
ponents. The analysis and verification can reuse any proved properties about
the components, such as divergence freedom and deadlock freedom without the
need to reprove them.
2.3
Object-Orientation in rCOS
The variables in the field declaration section can be of object types. This allows
us to apply OO techniques to the design and implementation of a component. In
our earlier work [14], we have extended UTP to formal treatment of OO program
and OO refinement. This is summarized as follows.
 
Search WWH ::




Custom Search