Formal Methods Europe Logo Formal Methods Europe
   
   
 
  Choosing
  Methods
  Tools
  Applications
  FAQs
  Literature
  Journals
  Courses
  Projects
  Universities
  Industry
  Groups
  Links
 

Application name:

Case Study Production Cell

Organisation:

Forschungszentrum Informatik Karlsruhe (Research Center for Computer Science, Karlsruhe, Germany).

Method:

Comparative case study. Currently (November 1994) 21 different methods have been used, others are invited to join.

Tools:

Several, depending on the method used.

Domain:

Robotics

Period:

1993 -

Size:

Length of specifications differ between 300 and 3000 loc, effort between one person week and two person months.

Description:

Aim of the case study is to develop control software for a real world production cell. The production cell serves to forge metal blanks and can be controlled using 14 sensors and 13 actuators. A number of safety and liveness properties have to hold. The case study is realistic, of medium complexity (about 10^15 to 10^22 states, depending on the granularity of the model), and is a good example of the application of formal methods.

Conclusions:

The case study showed both limitations and benefits of formal methods. This is documented in detail in the below mentioned references.

Publications:

C. Lewerentz, T. Lindner: "Case Study Production Cell -- A Comparative Study in Formal Software Development", LNCS, Springer-Verlag, 1994.

Contact:

Name:Thomas Lindner
Organisation: Forschungszentrum Informatik
Address: Haid-und-Neu-Strasse 10-14 76131 Karlsruhe
Country:Germany
Phone number:+49 (721) 9654616
Fax:+49 (721) 9654609
E-mail:lindner@fzi.de
Personal website:http://www.comlab.ox.ac/archive/procos/prod-cell.html

URL:

http://www.comlab.ox.ac/archive/procos/prod-cell.html

Remarks:

The case study is a joint activity with institutes spread over Europe. FZI coordinates the study.