Work Area: Logics and Logic Programming
Keywords algebraic specification, formal methods, software technology, system development
Start Date: 1 October 92 / Duration: 36 months / Status: running
[ participants / contact ]
Abstract The COMPASS Working Group attempts to consolidate and integrate the theoretical basis of algebraic specification methods and to apply it in software technology. The algebraic approach supports the precise specification of the semantics of generic reusable system components, providing the formal conceptual basis for their stepwise and correct development.
An industry of interchangeable and widely marketable software components in Europe is only possible if the functionality of a component can be precisely specified and the implementation relied upon. It is highly desirable to be able to specify only the necessary properties of a component or system in a requirements specification. This is the interface seen by the user that serves as a guideline for the implementor. It should be as precise as necessary, but also as loose as possible, avoiding overspecification of details.
The particular design remains hidden for proprietary reasons; an implementation can be replaced by another one for the same requirement specification. In this way a high level of abstraction from subsequently introduced design detail can be achieved. The COMPASS Working Group is investigating the stepwise development of more detailed and efficient versions, supported by semi-automatic tools, such that the overall correctness proof is broken down into the verification of correctness at each step. The development process itself could then be formalised as a basis for a library of generally applicable development methods.
The Group aims to provide a comprehensive algebraic approach to the specification of systems and their components, provide a formal basis for their correct development, consolidate the theoretical background, lay the basis for an increased power of support tools, encompass new programming methodologies and application areas, and make progress towards the development of a uniform mathematical framework for logic and semantics within computer science.
During the first three years of the COMPASS working group, over 300 research papers (including a survey and annotated bibliography volume) have been published by group members (not counting those of associated Scientific Correspondents).
In the past year, there have been the following workshops and subgroup meetings:
For the next two years, two COMPASS Workshops and two ADT/COMPASS Workshops are planned: COMPASS Workshop at Dresden in autumn 1993, joint ADT/COMPASS Workshop at Genova in spring 1994, COMPASS Workshop in autumn 1994, joint ADT/COMPASS Workshop in spring 1995. In addition, several smaller meetings between partners are also planned.
During the past year, over 100 research papers have been published by group members.
Consolidation of different approaches and extensions into new areas have been attempted in several focal areas, with emphasis on the structure of systems (modularisation, re-usability), structure of developments and proofs, and concurrency. Other fruitful areas of work include logical foundations, development concepts (methodology, specification languages), environments and tools (prototyping, theorem proving, term rewriting), and applications.
Group members have significantly contributed to the development of specification languages and methodologies for development, and also semi-automatic tools and development environments based on algebraic specifications.
Industry has a growing interest in formal methods and tools to increase reliability. Government institutions and private industry are starting to require adherence to formal development methodologies in security and safety critical areas. The economic impact of reliability, re-usability and the potential for early prototyping is increasingly recognised in industry, influenced by a traditionally stronger awareness in the hardware area.
The majority of over 100 research papers have been presented at international conferences. In addition, results have been presented at workshops, seminars and summer schools (not organised by the group), eg Seminar on Parallel Programming (Lisboa, June 93), International Workshop on Specifications and Semantics (Dagstuhl, May 1993), Fifth European Summer School on Logic, Language and Information (Lisboa, Aug. 1993).
Universität Bremen, Fachbereich Mathematik and Informatik - D
Postfach 330 440
D - 28359 BREMEN
Max-Planck Institut für Informatik - D
Technische Universität München - D
Technische Universität Berlin - D
Ludwig Maximilians Universität München - D
Technische Universität Braunschweig - D
Technische Univeristät Dresden - D
Arhus Universitet - DK
Universidad Politecnica de Catalunya - E
LIENS - F
CNRS - LRI - F
CNRS - CRIN - F
Università di Genova - I
Università degli Studi de l'Aquila - I
Univeristy of Oslo - N
Universiteit Nijmegen - NL
INESC - P
University of Edinburgh - UK
University of Oxford - UK
Prof. Dr. B. Krieg-Brückner
tel +49/421 218 3660
fax +49/421 218 3054
COMPASS - 6112, August 1994
please address enquiries to the ESPRIT Information Desk
html version of synopsis by Nick Cook