MetaFrame in Practice: Design of Intelligent Network Services - Correct System Design: Recent Insights and Advances - page 395

Note the precision and conciseness of the diagnostic information: the checked
properties involve an interplay of several SIBs along a path, which usually de-
scribe their relative positioning in a loose fashion. Thus they leave room for
several alternatives. As a consequence, legal error correction is not unique (in
the example, one could insert a new call segment delimiter (

prompt ) at any place

on the path below the SIBs), and a corresponding automatic selection pro-

cess is not wished, as it would unnecessarily constrain the designer, who usually
chooses the appropriate correction according to other (semantic) criteria. In this
case, service providers may desire billings to be valid on the longest possible
portion of a call segment. Thus the most convenient location for the

zone

zone SIB is

immediately before the last SIB on the path.

Of course this simple example service could have been still easily handled
by hand, but current IN services have reached sizes and complexities which de-
mand for automated support for error detection, diagnosis, and correction. Our
environment encourages the use of the new method, as it can be introduced
incrementally : if no formal constraints are dened, the system behaves like stan-
dard systems for service creation. However, the more constraints are added, the
more reliable are the created services [21].

prompt

3.5 Typical Constraints

This section summarizes some typical constraints, which provide a good feeling
for the style and common patterns in temporal constraint specication. They
comprise backward modalities and examples for constraints written in our rst-
order extension of SLTL:

{ `All call sections (which are separated by SIBs) are sepa-

ratedly billed'. Billed segments are determined by an initializing

prompt or initdp

billing SIB

and a corresponding closing call-line-charging SIB.

( prompt _ initdp ) ) ( : call-line-charging U billing )

{ `Every pin-protected path in a service only leads to a successful connection
if the nal pin check was successful'. The slightly indirect modelling of this
property assumes that the

check pin SIB only has two outgoing branches,

marked False and True .

check pin ) [ False ]( : destination U check pin )

{ More technical is the following constraint:

write user destination ) : prompt read dialled number

( BU )

which means that `every write user destination SIB must be preceded by a

read dialled number SIB occurs'. This is exactly the

constraint underlying the error view in Figure 4.

SIB before a prompt