Information Technology Reference
In-Depth Information
Buffer
get(; T out)
Component
put(T in ; )
Fig. 1.
A component with syntactic interface only
-
An interface for a component in a sequential system is obviously different
from one in a communicating concurrent system. A contract for the former
only needs to specify the functionality of the methods, e.g. in terms of their
pre- and post-conditions. A contract for the later should include a description
of the communicating protocol, for example in terms of interaction traces.
The protocol specifies the order in which the interaction events happen.
-
An interface for a component in a real-time application will need to provide
the real-time constraints of services, but an untimed application does not.
-
Components in distributed, mobile or internet-based systems require their
interfaces to include information about their locations or addresses.
-
An interface (component) should be stateless when the component is required
to be used dynamically and independently from other components.
-
A service component has different features from a middleware component.
It is the contract of the interface that determines the external behavior and fea-
tures of the component and allows the component to be used as a black box
.
Based on the above discussion, rCOS defines the notion of an interface con-
tract for a component as a description of what is needed for the component to be
used
in building and maintaining software systems. The description of an inter-
face must contain information about all the viewpoints among, e.g., functionality,
behavior, protocols, safety, reliability, real-time, power, bandwidth, memory con-
sumption and communication mechanisms, that are needed for composing the
component in the given architecture for the application of the system. However,
this description can be incremental in the sense that newly required properties
or view points can be added when needed according to the application. Also, the
consistency of these viewpoints should be formalizable and checkable. For this,
rCOS is built on Hoare and He's Unifying Theories of Programming [16].
The Minimal Use of UTP.
In UTP, a
sequential program
(but possibly non-
deterministic) is represented by a
design D
=(
α, P
), where
-
α
denotes the set of state variables (called observables) of the program
-
P
is a predicate
p
(
x
)
R
(
x, x
)
def
=(
ok ∧ p
(
x
))
⇒
(
ok
∧ R
(
x, x
))
, meaning that
if the program is activated
ok
in a state where the
precondition
p
(
x
)
holds
the execution will terminate
ok
in a state where the postcondition holds that
post-state
x
and the initial state
x
are related by relation
R
.
It is proven in UTP that the set of designs is closed under the classical pro-
gramming constructs of
sequential composition
,
conditional choice
,
nondetermin-
istic choice
, and fixed point of iterations. Refinement between designs is defined
Search WWH ::
Custom Search