A case study to develop control software for a realistic industrial production cell, comprising several machines (e.g., a robot, a press, two conveyor belts) has been suggested by the Forschungszentrum Informatik (FZI), a ProCoS-WG partner, as the basis of a useful comparison between different formal and other development techniques. The software for the case study has to fulfil certain safety and liveness requirements (e.g., never close the press while a robot arm is inside it). The example is taken from the real world (a metal processing plant in Germany), but at the same time is of manageable complexity.
The case study was originally launched as part of the German KorSo (= Correct Software) project by FZI. More than a dozen different methods, including Esterel, Lustre, Statecharts, SDL, RAISE/CSP, Focus, Eiffel, Modula 3 and Spectrum, have been applied so far. The contributions have been evaluated and compared according to a set of criteria. Several people are using or considering the example for teaching formal methods.
As well as papers and reports, a book has been issued which comprises 10-20 page summaries for each contribution together with a comparative survey [29]. Further on-line information is available via anonymous FTP under the directory:
ftp.fzi.de:/pub/korso/production_cell
For example, a graphical simulation, running under X windows, is available on-line. It illustrates the operation of the production cell, but it can also be used to validate control software. Interfacing a program with the visualisation is straightforward. Additionally, FZI has a running model of the production cell which can be controlled by software using the same interface.
The case study is not considered to be finished. Currently, contributions in Object-Z (an object-orientation extension of the Z notation) and the Duration Calculus (similar to temporal logic) are in progress. If you would like to try your favourite method too, please feel free to do so. A second edition of the existing book [29] is in preparation and futher contributions are welcome. Guidelines for submissions and a task description can be found under the FTP directory mentioned above.
For further information, please contact:
Thomas Lindner
Software Engineering Department
Forschungszentrum Informatik
Haid-und-Neu-Straße 10-14
D-76131 Karlsruhe
GermanyEmail: lindner@fzi.de