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

1. A rst draft of the service is usually obtained via modication of a pre-
existing service of similar application prole from the service library. A com-
pletely new design from scratch is also possible. Both design styles are sup-
ported by the macro facility and happen under model checking control.
2. The central design step consists of repeated, aspect-driven modication, im-
plementing a point-of-view design strategy: the user chooses an aspect of
interest, generates a corresponding view of the current service which ab-
stracts from all details irrelevant for this point of view, and modies it where
necessary. Due to the on-line verication with the model checker, which is
separately applicable also on views, constraint violations can be detected
immediately. In this phase automatic expansion of macros may be required,
in order to resolve `internal errors'. The eect of view modications can be
automatically transferred to the underlying model. This `apply' operation is
automatically supervised by the model checker: modications disrupting the
service structure are rejected.
3. Current service prototypes can at any time be tested, compiled, executed,
and, if satisfactory, stored in the service repository.

In combination with our concept of macros, views provide an extremely flex-
ible service development. In addition, views support the realization of a very
flexible access control mechanism , by enabling designers and service providers
to dene customer specic views with restricted modication potential. Views
provide in fact a natural means to organize the central design process (step 2)
into successive levels of renement taking adequate care of role-specic areas of
competences. In particular this allows us to tailor the environment for the spe-
cic needs of the service designer, the service provider, the customizer, and the
user. The view-specic hiding can be used to automatically dene and enforce
access permissions.

3.3 Model Checking-Based Formal Verication

The service creation process is constantly accompanied by on-line verication of
the global correctness and consistency of the service logic (Fig. 5). Vital prop-
erties concerning the interplay between (arbitrarily distant) SIBs of a service
and the executability conditions for intermediate prototypes can be veried at
any time during the design phase in a push-button fashion,via model checking.
Design decisions that conflict with the constraints and consistency conditions of
the intended service are thus immediately detected.

Global properties concerning the interplay between the SIBs of a service are
expressed in a user-friendly specication language based on SLTL, and gathered
in a constraint library that is automatically accessed by the model checker during
the verication. The maintenance of the constraint library is supported by a
hypertext system. Our model checker is optimized for dealing with hundreds of
constraints and moderate size systems (around 10.000 nodes), in order to allow
their verication in real time.