Information Technology Reference
In-Depth Information
However, we only reason on a subset of all possible components that can be
constructed according to the described component structure. We refer to this
subset of components as correct components . Correct components are not only
well-formed, but they adhere to some additional constraints. The various well-
formedness rules along with the correctness constraints are presented in the
following.
We start with specifying the structure of a well-formed component. A com-
posite component is considered as correctly structured if it passes the criteria
specified by the function CorrectComponentStructure given below.
primrec CorrectComponentStructure :: Component bool where
CorrectComponentStructure (Composite N itfs sub b s) =
(( b bindings.(GetQualified(src b) (Composite N itfs sub b s =
Some kind=Client,cardinality=Single )
(GetQualified(dest b)(Composite N itfs sub b s) =
Some
kind=Server,cardinality=Single ))
NoDuplicateSrc b
distinct (map getName sub)
( Q set (Cqueue s). (invokedItf Q) dom itfs
kind (the (itfs (invokedItf Q))) = Server)
A composite component has a correct structure if: each binding only connects
an existing client interface to another existing server interface; each client in-
terface is connected only once; all subcomponents have distinct names; and all
requests in the request queue of the composite refer to existing server interfaces.
A primitive component has a correct structure if it follows the last requirement
plus a couple of constraints relating its behaviour with its interfaces.
constdefs CorrectComponent :: Component bool
CorrectComponent c == CorrectComponentStructure c distinct(RqIdList c)
(ReferencedRqs c) (set(RqIdList c))
distinct (map getName (cpList c))
( f set (RqIdList c). snd f set(map getName(cpList c)))
A correct component is a correctly structured component that also has uniquely
defined request identifiers ( RqIdList c gives all requests computed by c and
its subcomponents), and all future referenced by the components should cor-
respond to an existing request. Finally, names of all components in the com-
position should be unique. This differs from the well-formedness requirement
which only requires the names of all direct subcomponents to be unique. The
requirement of checking correct future referencing throughout the composition
hierarchy is stronger than what is needed for most proofs, and can at times be
relaxed resulting in a weaker correctness requirement CorrectComponentWeak .
CorrectComponentWeakList gives similar constraints but for a list of compo-
nents. Using CorrectComponentWeak eases proofs involving component
hierarchy because if a component verifies CorrectComponentWeak then all its
subcomponents also verify it.
Search WWH ::




Custom Search