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

{F ( )

which means `A

connect

connect SIB is guaranteed to be reached eventually'.

{G ( ))

which is a liveness property meaning `Whenever a

connect ) F ( charging

connect SIB occurs, then

a charging SIB is guaranteed to eventually occur as well'.

First-Order Extension. Our temporal logic also allows for rst-order quanti-
cation over nite parameter domains [12]. Quantied formulas are expanded as
needed for the considered service so that they can be checked by our iterative
model checker. This may lead to an explosion of the number of constraints to
be checked, but in our experience this did not turn out to be a serious bottle-
neck. Section 3.5 illustrates the use of these constraints in our Service Denition
environment.

2.3 Views

The denition of aspect-specic views is part of the domain modelling phase,
which is itself an incremental process. Structural Views allow capturing a sys-
tem (here, a service) at a certain level of granularity, where subsystems are
encapsulated as single SIBs. Behavioural Views are based on the idea of hiding
aspects, like a specic kind of SIBs or conditions. These views can be dened
explicitly by dening equivalences, i.e., visibility relations, on the set of SIBs
and conditions, together with some structural properties, like the preservation
of branching structure 10 , or implicitly by means of temporal formulas.

Structural Views: Macros.
Technically, hierarchy is realized in form of a powerful mechanism for the def-
inition, parametrization and reuse of macros , which is fully compatible with
both formal verication and behavioural views. The macro facility covers the
standard stepwise renement approaches. This allows developers to dene whole
subservices as primitive entities, which can be used just like SIBs. As macros
may be dened on-line and expanded whenever their interna become relevant,
this supports a truly incremental service construction. Moreover, as macros have
formally the same interfaces as SIBs, this enhances the reuse of already designed
(sub-) services.

Behavioural Views.
Behavioural views are abstract service models. As such, they show aspects of
actual, concrete models. They are used to hide any aspect of an IN model which
is irrelevant wrt. an intended operation. This is useful during the development
phase in order to concentrate on specic themes, e.g., the billing or the user-
interaction contained in a service, while abstracting from all the rest. This com-
plements the macro facility (for structural views) in order to attack the problem

10 In our case this is dened in terms of bisimulation[15].