http://www.dagstuhl.de/00411

October 8 – 13 , 2000, Dagstuhl Seminar 00411

Semi-Formal and Formal Specification Techniques for Software Systems

Organizers

H. Ehrig (TU, Berlin), G. Engels (Paderborn), F. Orejas (Barcelona), M. Wirsing (Uni München)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl-Seminar-Report 288

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.

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.