The seminar was concerned with a challenging problem in current software technology: the use of non-sequential components in heterogeneous systems. Both topics are related and raise many interesting issues, such as concurrency, distribution, reliability, etc. They challenge existing formalisms and methods and were addressed at the workshop by various speakers. Heterogeneity of systems (e.g., hardware vs. software, continuous vs. discrete, etc.) is asking for the assumption that software can be considered in isolation. The methods used for sequential component development are being extended in an attempt to cope with these new requirements. At present, it is not clear whether these methods are in fact extendable. New methods and formalisms are being invented to address the challenges of building such systems.

To tackle the task of rigorous analysis of large systems, the methods will focus on high level specifications. That is, complex heterogeneous systems and the constituent components are described more abstractly, say on the level of system architecture rather than on the level of mere programs. A system architecture reflects interaction and interfaces between the components without specifying all their complex internal functionality. Analysis of such an architecture is a new challenge for methods being applied to ordinary software systems so far.

When discussing about systems in the large, we are also faced with refinement issues. Detailed information about timing or any physical limitation is not known on the abstract level of specification. For supporting the incremental development new strategies for refinement are introduced, i.e. how to develop a system design straightforward from a high level specification.

In practice, semi formal methods like UML are accepted by a broad audience of software engineers in order to describe heterogeneous systems on a high level. Although UML models are primarily used to communicate only a design, the emerging question is how formal notations and languages, which are developed for rigorous analysis already, can support the design phase. A formalisation that bridges the gap between semi formal and formal notations is to be developed and investigated.

In order to make technologies available and useful, adequate tool support has to be provided for actual usage in real applications. We aim at environments in which tools and notations are adequately integrated and which support methodological guidance without constraining the users creativity and individual progress.

In addition to the topics dealt with by the speakers, the workshop participants formed three working groups to discuss further questions of interest:

In order to get a comparison in the results of the different formal approaches, the community should benefit from treating a particular case study with the different formalisms. A new case study reflecting the needs of software intensive systems has to be found. In one working group a list of criteria to be characteristic for a suitable case study was worked out. According to these criteria the group agreed upon a rapid transportation management system (including a train control system, data management, etc.) to be a suitable case study.

In a second working group possible integration of UML with formal methods were discussed. Although UML is known as an uprising formalism it lacks a formal foundation as well as tool support through formal treatment. Several suggestions how to relate the notations of UML with formal notations were discussed.

A standardisation of formal methods based on a formal methods web repository was discussed in the third working group. The repository to be set up should collect all current formalisms as well as their corresponding software environments (if available) and case studies treated so far. This is to give a survey to industry or other potential users.

As a result of these discussions and the subsequent presentations, it was decided to apply for another Dagstuhl seminar, in the year 2001, with a similar orientation but calling additionally for the presentation of techniques and methods in the framework of a common case study to be distributed with the call for participation. A suggestion for this case study was the development of a train-control system (the result of one of the working groups)

The organisers wish to thank all the workshop participants for their work and interest in the topic. Special thanks go to the organisers of the working groups and especially to those who arranged the accompanying musical programme.

• Stephan Jähnichen
• Michel Lemoine
• Tom Maibaum
• Martin Wirsing