Information Technology Reference
In-Depth Information
Global Constraints: The Temporal Aspect.
Global constraints allow users to specify causality, eventuality and other vital re-
lationships between SIBs, which are necessary in order to guarantee executability
and other frame conditions.
A service property is global if it does not only involve the immediate neigh-
bourhood of a SIB in the service model
5
, but also relations between SIBs which
may be arbitrarily distant and separated by arbitrarily heterogeneous submod-
els. The treatment of global properties is required in order to capture the essence
of the expertise of designers about do's and don'ts of service creation, e.g. which
SIBs are incompatible, or which can or cannot occur before/after some other
SIBs. Such properties are rarely straightforward, sometimes they are documented
as exceptions in thick user manuals, but more often they are not documented
at all, and have been discovered at a hard price as bugs of previously devel-
oped services. They are perfect examples of the kind of precious domain-specic
knowledge that expert designers accumulate over the years, and which is there-
fore particularly worthwhile to include in the design environment for future
automatic reuse.
In the presented environment such properties are gathered in a Constraint
Library, which can be easily updated and which is automatically accessed by the
model checker during the verication.
Besides the looseness in the specication of single BBs at the abstract level of
the taxonomies,
also supports the loose specication of whole call
flows in terms of abstract constraints specifying precedences, eventuality, and
conditional occurrence of single taxonomy objects. Typical pattern for this kind
of loose specication are
M
eta
Frame
{
general ordering properties
, like
this BB must be executed/reached some time before some other BB
,
{
abstract liveness properties
, like
a certain BB is required to be executed/reached eventually
,and
{
abstract safety properties
, like
two certain BBs must never occur within the same run of the system
.
In particular, users can specify elaborate requirements concerning the interplay
between the occurrences of SIBs and conditions during the run of a specied IN-
service. In the following we present an according temporal logic, which comprises
the taxonomic specications of SIBs.
Denition 3 (SLTL).
The syntax of Semantic Linear-time Temporal Logic (SLTL) is given in BNF
format by:
5
I.e., the set of all the predecessors/successors of a SIB along all paths in the model.
Search WWH ::
Custom Search