Reference/Literaturverweis [Bre01a]

Bredereke, J.:
A Tool for Generating Specifications from a Family of Formal Requirements.
In Kim, M., Chin, B., Kang, S., and Lee, D. (eds.): "Formal Techniques for Networked and Distributed Systems", pp. 319-334. Kluwer Academic Publishers (Aug. 2001).

Abstract / Zusammenfassung

We are concerned with the maintenance of formal requirements documents in the application area of telephone switching. We propose a specification methodology that avoids some of the so-called feature interaction problems from the beginning, and that converts some more into type errors. We maintain all the variants and versions of such a system together as one family of formal specifications. For this, we define a formal feature combination mechanism. We present a tool which checks for feature interaction problems, which extracts a desired family member from the family document, and which generates documentation on the structure of the family. We also report on a quite large case study.

Keywords

tools; formal requirements; maintenance; feature interaction problems; telephone switching; Object-Z.

Tool / Werkzeug