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

Incremental Formalization: The successive enrichment of the application-specic
development environment is two-dimensional. Besides the library of application
specic BBs, which dynamically grows whenever new functionalities are made
available,

supports the dynamic growth of a hierarchically organized
library of constraints , controlling and governing the adequate use of these BBs
within application programs. This library is intended to grow with the experience
gained while using the environment, e.g., detected errors, strengthened policies,
and new BBs may directly impose the addition of constraints. It is the possible
looseness of these constraints which makes the constraints highly reusable and
intuitively understandable. Here we consciously privilege understandability and
practicality of the specication mechanisms over their completeness.

M eta Frame

Library-Based Consistency Checking: Throughout the behaviour-oriented devel-
opment process, oers access to mechanisms for the verication of

libraries of constraints by means of model checking. The model checker individu-
ally checks hundreds of typically very small and application- and purpose-specic
constraints over the flow graph structure. This allows concise and comprehen-
sible diagnostic information in the case of a constraint violation, in particular
as the information is given at the application rather than at the programming
level.

M eta Frame

These characteristics are the key towards distributing labour according to the
various levels of expertise. We envisage

Programming Experts: They are responsible for the software infrastructure,
the runtime-environment for the compiled services, as well as the programming
of BBs. Infrastructure and BB development require advanced programming ex-
pertise. In comparison, the wrapping of existing (legacy) components to BBs,
which is explicitly supported by M eta Frame , is simpler, as it always follows a

similar pattern.

Constraint Modelling Experts: They classify the BBs, typically according to
technical criteria like their version or specic hardware or software requirements,
their origin (where they were developed) and, here, most importantly, according
to their intent for a given application area. The resulting classication scheme
(called taxonomy, Section 2.1) is the basis for the constraint denition in terms
of modal formulas. The design of the taxonomies should go hand in hand with
the denition of aspect-specic views, as both are mutually supportive means to
an application specic structuring of the design process.

Application Experts: They develop concrete applications, by graphically com-
bining BBs into coarse-granular flow graphs. These graphs can be immediately
executed by means of an interpreter, in order to validate the intended behaviour
(rapid prototyping). Model checking (Sect. 3.3) guarantees the consistency of
the constructed graph with respect to the constraint library.