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

in Practice:
Design of Intelligent Network Services

M eta Frame

Bernhard Steen 1 and Tiziana Margaria 2

1 LS V, Universitat Dortmund, Baroper Str.301, D-44221 Dortmund (Germany),
[e-mail]
2 LS I, Universitat Dortmund, Otto-Hahn Str. 16, D-44227 Dortmund (Germany),
[e-mail]

Abstract. In this paper we present M eta Frame , an environment for
formal methods-based, application-specic software design. Characteris-
tic for

are the following features: library-based development ,
meaning software construction by combination of components on a coarse
granular level, incremental formalization , through successive enrichment
of a special-purpose development environment, and library-based con-
sistency checking , allowing continuous verication of application- and
purpose-specic properties by means of model checking.
These features and their impact for application developers and end users
will be illustrated along an industrial application, the design of intelligent
network (IN) services.

M eta Frame

1 Motivation

With the increasing dependency of every day's life on computer-aided support,
moving large portions of the needed application programming load from pro-
gramming experts to application experts or even to end users becomes a major
challenge. For application experts, this requires freeing programming activities,
intrinsic to the development of applications, from their current need of program-
ming expertise . For end users, taking over advanced reshapings of applications
additionally requires freedom from expertise in the particular application do-
main .
Classical software engineering tools do not provide means to support the re-
quired `programming-free' programming style. They are typically designed to
support programming experts in their usual programming activities, e.g. by
starting from semi-formal modelling or description languages like OMT and later
UML, as in the case of ObjectGEODE [14], or from Statecharts, as for State-
mate [11], or from SDL, as for SDT and more recently Tau [26], or Petri Nets,
as for Design/CPN [13, 8]. This target is shared by and large also by the known
formal methods-based tools, which provide support to development activities by
means of renement from specications expressed in various specication lan-
guages (like e.g. [1, 2] or [17]). These methods and tools are better suited to
design from scratch rather than for reengineering and component integration
purposes, and tend to require both programming and verication skills.