Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 01221

Can Formal Methods Cope with Software-Intensive Systems?

( May 27 – Jun 01, 2001 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:



During the last years practical Software Engineering techniques are used more and more to conduct systematic and rigorous development of large software systems. UML has become the standard notation for guiding and documenting Software Engineering projects. CASE tools of today offer not only the UML notation but also are able to generate code templates and to support round trip engineering between class diagrams and program code. However, all case tools and more generally the Software Engineering techniques used in practice do not support well the early phases of software development; they still lack analysis and validation methods for requirements and design specifications which are easily connected to the implementation phase.

Formal techniques have undergone a steep development during the last years. Based on formal foundations and deep theoretical results, methods and tools have been developed to support specification and design of software systems. Model-based and algebraic specifications, abstract state machines, CSP and CCS, temporal logics, rewriting techniques, finite automata, model checking and many other formal specification and verification Bettina Buthtechniques have been applied to non-trivial examples and are used in practice e.g. for the development of safety critical systems.

Several case studies have proved to be useful for validating and evaluating formal software development techniques. Case studies such as the production cell [1], the steamboiler [2] and the memory cell [3] are now used as references for the applicability of formal methods. However, all these case studies tackle the development in the small; what is missing is a comparison of the development in the large. How do the known formal techniques scale up? How do they cope with aspects such as architecture, componentware, distribution, mobility, reconfiguration?

The aim of this workshop is to contribute to the field of Experimental System Engineering by proposing a case study for system development which allows one to compare different formal techniques in their abilities to specify, design, analyze and validate large software intensive systems. The case study addresses the actual problem of controlling autonomous trains and contains features such as local control in a distributed system, synchronous and asynchronous communication, heterogeneous components, and optimization problems. The requirements of the case study can be found at

During the workshop the solutions for the case study shall be presented and discussed by the participants.


[1] M. Broy, S. Jaehnichen (eds.): KORSO: Methods, Languages, and Tools for the Construction of Correct Software. Lecture Notes in Computer Science 1009, Berlin: Springer, 1995.

[2] J.R. Abrial, E. Boerger, H. Langmaack (eds.): Methods for Semantics and Specification, Dagstuhl-Seminar 9523, Also: J.R. Abrial, E. Boerger, H. Langmaack (eds.): Formal Methods for Industrial Applications. Lecture Notes in Computer Science 1165, Berlin: Springer, 1996.

[3] Manfred Broy, Leslie Lamport: Specification and Refinement of Reactive Systems, Dagstuhl-Seminar 9439. Also: M. Broy, S. Merz, K. Spies (eds): Formal System Specification: The RPC-Memory Specification Case Study. Lecture Notes in Computer Science 1169, Berlin: Springer, 1996.

  • Egon Börger (University of Pisa, IT) [dblp]
  • Jan Bredereke (Verden (Aller), DE)
  • Christine Choppy (University of Paris North, FR)
  • Lori A. Clarke (University of Massachusetts - Amherst, US) [dblp]
  • Jorge R. Cuéllar (Siemens AG - München, DE) [dblp]
  • Adriaan deGroot (University of Nijmegen, NL)
  • Martin Gogolla (Universität Bremen, DE) [dblp]
  • Maritta Heisel (Universität Duisburg-Essen, DE) [dblp]
  • Steffen Helke (TU Berlin, DE)
  • Paola Inverardi (University of L'Aquila, IT) [dblp]
  • Stefan Jähnichen (Fraunhofer Institut - Berlin, DE) [dblp]
  • Florian Kammüller (TU Berlin, DE) [dblp]
  • Fabrice Kordon (UPMC - Paris, FR) [dblp]
  • Jeff Kramer (Imperial College London, GB) [dblp]
  • Michel Lemoine (ONERA - Toulouse, FR)
  • Jeff Magee (Imperial College London, GB) [dblp]
  • Stephan Merz (LORIA - Nancy, FR) [dblp]
  • Leon J. Osterweil (University of Massachusetts - Amherst, US) [dblp]
  • Barbara Paech (Universität Heidelberg, DE) [dblp]
  • Emmanuel Paviot-Adel (UPMC - Paris, FR)
  • Steve Roach (University of Texas - El Paso, US)
  • Thomas Santen (TU Berlin, DE) [dblp]
  • Bernhard Schätz (TU München, DE) [dblp]
  • Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
  • Michel Sintzoff (University of Brussels, BE)
  • Werner Stephan (DFKI - Saarbrücken, DE) [dblp]
  • Alfred W. Strohmeier (EPFL - Lausanne, CH)
  • Carsten Sühl (Fraunhofer Institut - Berlin, DE)
  • Sebastián Uchitel (Imperial College London, GB)
  • Victor Winter (Sandia National Labs - Albuquerque, US) [dblp]
  • Martin Wirsing (LMU München, DE) [dblp]
  • Steffen Zschaler (TU Dresden, DE) [dblp]