During the last 20 years several different formal and semi-formal specification techniques have been successfully developed and used. Applications comprise the specification of simple programs, data types and processes as well as of complex hardware and software systems. The variety of specification techniques ranges from formal set theoretical, algebraic and logic approaches for specifying sequential systems and from Petri-nets, process algebras, automata, graph grammars for specifying concurrent and distributed behaviors to semi-formal software engineering methods such as UML which has become the de facto software engineering standard for developing large and complex systems.

Formal and semi-formal approaches have their advantages and disadvantages: the informal diagrammatic methods are easier to understand and to apply but they can be ambiguous. Due to the different nature of the employed diagrams and descriptions it is often difficult to get a comprehensive view of all functional and dynamic properties. On the other hand, the formal approaches are more difficult to learn and require mathematical training. But they provide mathematical rigor for analysis and prototyping of designs. Verification is possible only with formal techniques.

The talks and discussions of a previous seminar held in Dagstuhl in 1998 on this topics have shown that many researchers and research groups are putting more and more effort in closing this gap by integrating semi-formal and formal specification techniques. Their studies and experiences show the added value of combining semi-formal and formal techniques and at the same time open a whole range of new problems and questions which cannot be asked when studying formalisms in isolation. The talks and discussions of the previous seminar have shown particular interest and first results in studying the relationship between UML as de facto standard for diagrammatic modeling languages and CASL as the new standard algebraic specification language.

The goal of this seminar is to study possibilities and solutions for integrating and validating different formal and semi-formal specification techniques. Similarities and differences of several specification formalisms as well as possibilities for combining such techniques shall be discussed. The talks in this seminar should not concentrate on a single technique in isolation but should analyze, compare or integrate at least two techniques. As a prominent example we propose to study the relationship between UML and the formal techniques in order to give added value to both, the diagrammatic as well as the formal specification techniques.

The comparisons could be based on semantical concepts, available specification constructs and their theory, proof calculi, methodical support and tool support, and important application areas. Typical integration problems are the combination of static and dynamic aspects as well as the integration of different phases of the software development process. The validation of methods should take into account the mathematical elegance and foundation as well as the practical applicability in different areas.