Paper Description: MIP-9516

Motivation:

In his invited talk at TAPSOFT'95e, Joseph Goguen claimed that practical succes of formal methods is bound to a tool-supported domain specific paradigm (cf. [GoLu95]). which he characterized as follows:

1. a narrow, well defined, well understood problem domain is addressed; there may already be a success library for this domain,
2. there is a community of users who understand the domain, have good communication among themselves, and have potential financial resources,
3. the tool has a graphical user interface that is intuitive to the user comunity, embodying their own language and conventions,
4. the tool takes a large grain approach; rahter than synthesizing procedures out of statements, it synthesizes systems out of modules; it may use a library of components and synthesize code for putting them together,
5. inside the tool is a powerful engine that encapsulates formal methods concepts and/or algorithms; it may be a theorem prover or a code generator; users do not have to know how it works, or even that it is there.

The META-Frame environment [StMC95] developed in Passau arose exactly from the need for such tool support. Other systems fitting this description are: CAPS [Luqi93], ControlH and MetaH [Vest94], AMPHION [SWLP94], and DSDL [BeKi94, KBBH95]. It supports programming with whole subroutines and modules as elementary building blocks on the basis of a specifically instantiated repository. Originally, the need arose from the problem of the construction of application-specific heterogeneous analysis and verifications tools on the basis of a repository of elementary tools and algorithms [MaCS95, StMC95b]. In the meantime it turned out that META-Frame has a much wider application profile, as will be illustrated by means of a completely different application: the construction of intelligent network (IN) services. This application, which is described in detail in Section 3, led to a very successful industrial cooperation with the Siemens Nixdorf Informationsysteme AG (SNI). In fact, a corresponding product, prototypes of which are currently presented by SNI on various Telecommunication Fairs, will be on the market in 1996. Its development required the collaboration of five different sites (two in Munich, Berlin, Vienna and Passau), with Passau spending more than 6 man years in '95 on this project, involving 17 students, researchers and post-docs.
Incremental formalization, ranging from 'no specification', which results in the old-fashioned development style, to 'detailed specification' with full tool support, was the key to the acceptance of our underlying method in an industrial environment.This observation is in full correspondence with Christiane Floyd's statements at TAPSOFT'95 [Floy95]. However there were also other important factors for acceptance, like e.g. the strong support of software reuse (Sec. 4), enhanced flexibility (Sec. 5), an intuitive specification language (Sec. 6), graphical interface and hypertext support (Sec. 8), which we will discuss along the lines of the "Ten Commandments of Formal Methods" proposed by Bown and Hinchey in [BoHi95].
After sketching the basics of META-Frame, and of its industrial application in the next two sections, we present our philosophy and design decisions in Sections 4 to 9. As this discussion complements the brief sketch of our scenario, a full picture of our industrial application will be proved at the end. Section 10 summarizes our experience and perspectives.

Paper itself:

• compressed file (for previewing)

Cross links:

• more reports
• Lehrstuhlübersicht der Fakultät für Mathematik und Informatik
• Fakultät für Mathematik und Informatik
• Universität Passau