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 http://www.pst.informatik.uni-muenchen.de/dagstuhl/

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

References:

[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.