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

Number (PIN) and, depending on the time of the day, the call is either released
(in the forbidden time windows) after an announcement, or it is routed to the
desired destination number.

A `Billing Constraint'. The following Billing Constraint
Unsuccessful calling sections will not be charged

guaranteeing a property Germans are used to, can be expressed by the formula

release ) : zone prompt _ initdp

( BU ( ))

Here BU stands for a backward until modality, which is not part of SLTL, but
can nevertheless be dealt with by our model checker. Intuitively, it is inter-
preted as the standard until operator on a service model, where all edges have
been reverted. Intuitively the formula expresses the Billing Constraint as fol-
lows: traversing the service model backward from the

release SIB, which marks

unsuccessful call attempts, no (i.e. call segment charging) SIB should be

met on the segment, which is delimited by a

zone

prompt or by an initdp SIB. The

verbal formulation is shown in Fig. 6(middle).
Here we see that the logic allows expressing constraints not only along the
flow of the call (forward constraints), but also in the opposite direction. Thus,
a wide class of causality interactions can be elegantly and concisely formulated,
successfully checked, and eciently enforced.
In our example, model checking the Free-Phone service wrt. this constraint
results in the discovery of erroneous paths in the graph. To ease its location and
the correction of the error, an abstract error view is automatically generated, to
evidence only the (usually few) relevant nodes. In order to supply a maximum of
information concerning the error, error views do not touch the erroneous part,
but constrain the application of the (model) collapse to the correct portion of
the service. This choice also supports error correction, since the attention is
immediately drawn on the (usually small) erroneous portion of the service logic,
which is presented to a level of detail typically sucient for correcting the error.

Fig. 6(right) shows the automatically generated error view with error location
information for that same service and constraint.

{ The error locating view has been obtained automatically after the failed
model checking. Irrelevant nodes are collapsed in the unlabelled nodes. It is
now easy to see that there is a constraint violation along the (unsuccessful)
path between the

release and the initdp SIBs: the portion evidenced by the

SIB which is not allowed on this path.
The location of the error is thus much more easily spotted than by inspection
of the whole graph.
{ The view graph can be directly edited, e.g. by deleting the

highlighted arrows contains a zone

SIB.
{ The view application actualizes the corresponding IN-service model which is
thus automatically corrected. A new verication via model checking conrms
the conformance of the resulting service.

zone