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

Granny's Free-Phone Service

Fig. 6. Granny's Free-Phone Service with Forbidden Billing Error Location View

If the model checker detects an inconsistency, a plain text explanation of
the violated constraint appears in a window as shown in Figure 6, and an error
view is automatically generated, concentrating on the SIBs containing informa-
tion relevant for the error detection, thus simplifying the location of the error.
Corrections can be done directly on the error view, and the subsequent view
application automatically updates the underlying concrete model.

3.4 Example: Granny's Free-Phone

The service shown in Fig. 6 presents the flow graph of a simple kind of Free-
Phone (800-service). In essence, the service logic is the following: after a call
initialization section common to all services, the caller dials the desired specic
Free-Phone number, then a prompt requires entering a Personal Identication