genFamMem Home Page

genFamMem

A specification generator and type checker for families of formal requirements.

overview
formal languages supported
versions
download
documentation
related publications
links

Overview

genFamMem is a tool that supports the maintenance of formal requirements specifications written in an extension of one of the languages CSP-OZ, CSP-Z, or Z. The tool helps to avoid so-called feature interaction problems in requirements documents, or to detect them, by

allowing to maintain all variants of a requirements document together, by
using a specification style that encapsulates variant choices, and by
allowing/urging the original specifier to document as much of the information as possible that another specifier of an incremental feature will need.
The information provided formally by a specification written in CSP-OZ with our extension comprises
- the dependences among the features, through the hierarchy of parents sections sets and of class inheritance, and
- what is the core of a feature, by the distinction between default sections, which are changeable, and normal sections, which are essential.
This information can help the maintenance specifier to avoid problems, and it can be used for automated type checks, as performed by the tool genFamMem.

Formal Languages Supported

Currently, there is active work with CSP-OZ. But the language extension is defined not only for CSP-OZ, but also for CSP-Z and for Z. The tool genFamMem supports all of these languages.

CSP-OZ is a combination of CSP (Communicating Sequential Processes) and Object-Z by Clemens Fischer. CSP-Z is a variant of CSP that uses Z for the data representation. Object-Z is an object-based extension by Graeme Smith.

Versions

genFamMem 2.x

Now provides support for multiple formal languages. It is based on Flex/Bison and C code.

genFamMem 1.x

Is now obsolete. It supports a previous version of the family extension for CSP-OZ. It was written in Perl.

Download

You may obtain and use genFamMem free of charge, provided that you share some of your experiences with me.

Downloading: the gzip-ed tar ball of the sources of genFamMem 2.0.3 is available here. It also contains the necessary LaTeX style files for type-setting specifications. You find compiling and installation instructions in the file INSTALL.

In order to display the graphical output, you will need the daVinci 2.1 tool.

Platform: The genFamMem tool compiles fine with Flex, Bison, and the Gnu C compiler on Linux platforms, but should not cause major difficulties on other Unix platforms, as long as you use these Gnu tools, too.

Documentation

See also the list of related publications below.

Manual

Bredereke, J.:
genFamMem 2.0 Manual - a Specification Generator and Type Checker for Families of Formal Requirements.
University of Bremen, Germany (Oct. 2000). (ps/gzip)

Short Overview of Command Line Options

Usage:
        genFamMem  familymember infile
        genFamMem  --uhier-all infile
        genFamMem  --uhier-familymember familymember infile
        genFamMem  --uhier-feature feature infile
Options are:
        --uhier-all, -l:
                print uses-hierarchy of all sections, only
        --uhier-familymember familymember, -a familymember:
                same, for one family member
        --uhier-feature feature, -e feature:
                same, for one feature
        --ascii, -x:
                when --uhier-*, use ASCII output format
        --daVinci, -X:
                when --uhier-*, use daVinci output format (default)
        --only-features, -f:
                when --uhier-*, abstract sections to features
        --language-z, -z:
                input language is Z
        --language-cspz, -c:
                input language is CSP_Z
        --language-cspoz, -o:
                input language is CSP-OZ (default)
        --help, -?, -h:
                print this help info
        --version, -V:
                print version information
        --debug, -d:
                print additional debug information
        --bison-debug, -D:
                let the bison parser print its debug information
        --markup, -M:
                do mark-up only and print it (useful for debugging)
Output appears on stdout.
An option argument is specified as in "--uhier-feature=foo",
in "--uhier-feature foo", or in "-efoo".

Related Publications

See also my Web page about typesetting Z specifications with family constructs, which is about a more recent version of family constructs.

Bredereke, J.:
Maintaining Families of Rigorous Requirements for Embedded Software Systems.
Habilitation thesis, University of Bremen, Germany (2005). To appear. (abstract)

Bredereke, J.:
On Feature Orientation and on Requirements Encapsulation Using Families of Requirements.
In Ehrich, H.-D., Meyer, J.-J., and Ryan, M. editors, "Objects, Agents, and Features", pp. 26-44. (c) Springer Verlag, LNCS 2975 (2004). (abstract - ps/gzip - pdf)

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 - ps/gzip of a draft)

Bredereke, J.:
Hierarchische Familien formaler Anforderungen.
In: Grabowski, J., Heymer, S. (editors), " Formale Beschreibungstechniken für verteilte Systeme - 10. GI/ITG-Fachgespräch", pp. 31-40, Lübeck, Germany (22-23 June 2000). Shaker Verlag, Aachen, Germany. (abstract - ps/gzip)

Bredereke, J.:
Families of Formal Requirements in Telephone Switching.
In: Calder, M. and Magill, E. (eds.), "Feature Interactions in Telecommunication Networks VI", pp. 257-273, Amsterdam (May 2000). IOS Press. (abstract - ps/gzip)

Bredereke, J.:
Specifying Features in Requirements using CSP-OZ.
In: Gilmore, S. and Ryan, M. (eds.), "Proc. of Workshop on Language Constructs for Describing Features", pp. 87-88, Glasgow, Scotland (15-16 May 2000). ESPRIT Working Group 23531 - Feature Integration in Requirements Engineering. (abstract)

Bredereke, J.:
Modular, changeable requirements for telephone switching in CSP-OZ.
Tech. Rep. IBS-99-1, Univ. of Oldenburg, Oldenburg, Germany (Oct. 1999). (abstract - ps/gzip)

Bredereke, J.:
Requirements specification and design of a simplified telephone network by functional documentation.
CRL Report 367, McMaster University, Hamilton, Ontario, Canada (Dec. 1998). (abstract - ps/gzip-letter - ps/gzip-A4)