genFamMem Home Page
A specification generator and type checker for families of formal
requirements.
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.
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.
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.
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
tool daVinci 2.1.
In the year 2005, this tool was renamed due to a trademark conflict.
Now, it is called
uDraw(Graph).
However, I did not test genFamMem with the current version of
uDraw(Graph).
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.
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".
See also my Web page about
typesetting Z specifications with family constructs, which is
about a more recent version of family constructs.
Note: Some of the following links to abstracts
are currently not available, due a to restructuring of this Web site.
The papers themselves should be fine. Please email me if this page
should get a higher priority for getting fixed.
Bredereke, J.:
Maintaining Families of Rigorous Requirements
for Embedded Software Systems.
Habilitation thesis, University of Bremen, Germany (2005).
(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)
|
