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

Constraints

Control

Building
Blocks

Modification

Control

Synthesis

Selection

Concretization

View

Prototype

Abstraction

Compilation

Application
Program

Fig. 1. Application Development Process in M eta Frame

End Users: They may modify a given application program by adding require-
ments in terms of behavioural traces. These requirements are then `merged' with
the given program to obtain a new application program that behaves as required
along the new dening traces, but still as the original program everywhere else.
Section 3.6 sketches this method together with the required frame conditions.
The collection of professional proles needed is often dictated by the application
domain. The above list can of course be rened much further.

M eta Frame
is two-dimensional: both the application and the environment can be enriched
during the development process.

The resulting overall lifecycle for application development using

Application Development. Its corresponding lifecycle is summarized in Figure 1.
Based on libraries of BBs and constraints, an initial application program (the
prototype) is graphically constructed under model checking control, and sub-
sequently modied in an aspect-driven fashion: the application expert chooses
an aspect of interest, generates the corresponding view abstracting from all ir-
relevant details, and modies it where necessary. The eect of the modication
can be automatically transferred to the underlying application program in a
concretization step. This cycle is iterated until all relevant aspects have been
treated. Due to the on-line verication with the model checker, constraint viola-
tions are immediately detected. Current prototypes can at any time be tested,
compiled, executed, and, if satisfactory, stored in a repository.