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

All these methods aim at making a global behaviour-oriented approach to pro-
gramming applicable, essentially by reducing the apparent size of the underly-
ing global model. The success of this approach therefore strongly depends on
the existence of an adequate granularity and on the adequacy of the temporal
constraint-based specication mechanism. We have a very promising experience
with `workflow-oriented' systems, which provide a flexible management and or-
ganization of collections of components, like in the IN application. On the other
hand, the design of the underlying libraries of components themselves or the
construction of large concurrent systems should be done by other means. E.g.,
we use the object-oriented approach for the design of our component libraries.

5 Conclusions

The presented approach exactly meets the demands for the emerging paradigm
of Domain Specic Formal Methods [10]: use formal methods on a large or huge
grain level rather than on elementary statements, thus support the programming
with whole subroutines and modules as elementary building blocks. This is pre-
cisely what

M eta Frame is designed for and what the application to IN services

embodies.
Still, the step towards the use of formal methods is rather big and can hardly
be done at once. The

M eta Frame

environment therefore oers a lazy and incre-
mental use of formal methods: if no formal constraints are dened, the system
behaves like standard systems for service creation. However, the more constraints
are added, the better is the automatic control and the more reliable are the cre-
ated services. In fact, in the extreme case of a full specication of the vital frame
conditions, very few representative tests are required to guarantee the correct-
ness of the service.
Experience shows that it is often impossible to write complete formal spec-
ications in practice. E.g. in the case of service creation, the knowledge about
the exact requirements is distributed over several groups along the development
process, and it is only used implicitely during the development. Thus people
need to learn that and how this knowledge should be made explicit. The incre-
mental renement of the formal specication, by successively adding more and
more constraints, provides a `soft' entry into the world of formal methods.

Acknowledgement

The technical development of the environment, as well as of its

instance for the IN application, was competently promoted and supervised by
Volker Braun. He took over leadership of the

M eta Frame

team from Andreas
Claen early in 1995, and made sure that the environment reaches industrial
strength. We are very grateful to the whole

M eta Frame

team, in particular to
Achim Dannecker and Andreas Holzmann, who accompanied the development
from the very beginning.
Finally, we would like to thank Gerhard Goos, Bengt Jonsson, Markus Muller-
Olm and Perdita Stevens for their constructive feedback.

M eta Frame