"Production Cell" Case Study
Information provided by Thomas Lindner. Further
details are available via anonymous FTP
together with
"README" information.
See also new
WWW information at
FZI.
A Comparative Study in Formal Software Development
The task of the
case study is to develop control software for a realistic
industrial production cell, comprising several machines (e.g., a robot,
a press, two conveyor belts). This software has to fulfill certain
safety and liveness requirements (e.g., never close the press while a
robot arm is inside it). The example is taken from real world (a metal
processing plant in Germany), but is at the same time of managable
complexity.
So far 14 Different Methods Applied
The case study was launched in the German "KorSo" (= Correct Software)
project by the Forschungszentrum Informatik (FZI). More than a dozen
different methods, amongst them Esterel,
Lustre, Statecharts, SDL,
RAISE/CSP, Focus, Eiffel,
Modula 3 and
Spectrum, have been applied. The
contributions have been evaluated and compared according to a set
of criteria. Several people are using the example for teaching formal methods, or are
considering using it.
Book Available
Besides some papers and reports, a book has been issued which comprises
10-20 page summaries for each contribution together with a
comparative survey (28 pages). All papers and
an
extract of the book (26 pages) are available. Information about how to
get the book is available too.
Graphical Simulation Available
A
graphical simulation, running under X Windows, is available via
anonymous FTP. (Check the
"README" information first.) It illustrates the operation
of the production cell, but it can also be used to validate control
software. Connecting a program with the visualization is easy. Besides
that, the FZI has a running toy model of the production cell which can
be controlled by software using the same interface.
Call for Contributions
The case study is not considered to be completed. Currently,
contributions in Object-Z and the Duration Calculus are in progress. If
you would like to try your favorite method, too, please feel free to do
so. The task
description is available. We are preparing a second edition of our
book and welcome other contributions.
Guidelines for
submissions can be found too.
Thomas Lindner
Software Engineering Department
Forschungszentrum Informatik
Haid-und-Neu-Straße 10-14
D-76131 Karlsruhe
Germany
lindner@fzi.de
See also
FZI, Karlsruhe Gopher service.
HTML page prepared by
Jonathan Bowen from a
plain text original submitted to the comp.specification and comp.software-eng
newsgroups.
Part of the ProCoS-WG
Working Group archive.