COMPASS Summary

Seven Years of

Bernd Krieg-Brückner

Bremen Institute for Safe Systems
FB3, Universität Bremen
bkb@Informatik.Uni-Bremen.DE

Abstract. The ESPRIT Basic Research Working Group COMPASS has brought together most European scientists in the area of algebraic specification methods in an effort to consolidate and integrate the theoretical basis and apply it to software technology. The algebraic approach treats not just the syntactic aspects of interfaces but supports the precise specification of the semantics of generic reusable system components, providing the formal conceptual basis for their stepwise and correct development.

Introduction

As Coordinator of the COMPASS Working Group for seven years, I would like to take this opportunity to look back on what we set out to achieve, what we achieved, and what our future might be.

Historical Development

The systematic investigation of algebraic specification methods in the context of computer science started in the early seventies in the USA and Canada. In the late seventies, the topic also became a major research issue in Europe. Since then, the number of researchers in this area has grown considerably, and the algebraic approach has come to play a central role in research on formal program specification and development, as its range of applications was extended to the specification of complete software systems, to the formal description of the program development process, and to the uniform definition of syntax and semantics of programming languages. Meanwhile this approach extends beyond just software to the development of integrated hardware and software systems.

Today the field of algebraic specification has grown into one of the major areas of research in theoretical computer science. The flourishing activities in this area in the past twenty years have led to an abundance of technically different approaches, theories, and concepts. This seeming diversity is only superficial; all approaches share a common framework and mathematical basis.

The Working Group

COMPASS (a COMPrehensive Algebraic approach to System Specification and development) was funded as an ESPRIT Basic Research Working Group 3264 from April 1989 (COMPASS 1), and, as a continuation, as Working Group 6112 until March 1996 (COMPASS 2).

The COMPASS Working Group originally consisted of 11 Partner organisations with 18 team leaders and about 90 scientists; in the second phase it was extended to 19 Partners. In addition to members of the partner organisations, a varying number of so-called Scientific Correspondents received funding for travel to COMPASS Workshops, joint meetings and visits.

In effect, the COMPASS Working Group has brought together most European scientists in the area of algebraic specification methods in an effort to consolidate and integrate the theoretical basis and apply it to software technology.

Aims and Objectives

Original Aims

The potential effects and ramifications of the originally stated aims (quoted from [1, 2] in this section) are as important now as they were at the beginning of COMPASS:

• to provide a comprehensive algebraic approach to the specification of systems and their components,
• to provide a formal basis for their correct development,
• to consolidate the theoretical background,
• to lay the basis for an increased power of support tools,
• to encompass new programming methodologies and application areas, and
• to make progress towards the development of a uniform mathematical framework for logic and semantics within computer science.

An Industry of Reusable and Interchangeable Software Components will have significant advantages (and is perhaps only possible) with formal methods, i.e. if the meaning of a component is precisely specified and the implementation can be relied on to be correct. It should be possible to understand and use a system component only on the basis of its interface, making it reusable. For the implementor, it is equally important to be able to hide the body for proprietary reasons, and to replace it when the interface is not affected. Generic reusable system components avoid duplication of development efforts, ease prototyping and speed up system construction.

Formal Specification and Development. It is common practice in software technology that only the syntactic aspects of interfaces are specified, i.e. the data types and operations that the component provides. User and implementor have to rely on natural language comments for information about their meaning. This poses a severe danger of misinterpretation, inconsistency and incompleteness; there is no way to increase confidence by any means of verification other than inspection of code. This violation of the information hiding principle makes system improvements and evolution extremely cumbersome and error-prone, if not impossible.

The algebraic approach supports the precise specification of the semantic aspects of interfaces, providing the conceptual basis for their use and the theoretical foundations for the formal development of correct system components from their specifications. Thus it covers the whole software development process from the specification of requirements to the finished system.

Loose Specification of Requirements. 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: this avoids over-specification of details, leaves freedom for different design decisions by the implementor, and is therefore likely to decrease cost and increase efficiency.

Independence of Design. The particular design implementing the interface should remain hidden. The hiding principle eases replacement of components at the development stage, for example of a prototype component by a final implementation, and during system evolution when requirements change.

Purely model-oriented approaches, specifying the meaning of a component by giving a very abstract implementation (for example by sets, or by lists in a functional programming language) may give away more detail about the particular design than desirable since they specify a particular model. Transition to another design may be very difficult since a specification of the abstract properties common to both is not available; in fact, such a property-oriented specification, which is loose enough to characterize a class of distinct models, has to be constructed in this situation.

Stepwise Development. Thus a high level of abstraction from subsequently introduced design details can be achieved. Perhaps most importantly, the refinement relations between a specification and a sequence of more detailed designs, that is the correctness of the implementation with respect to the interface, can be formally verified.

The COMPASS Working Group investigates the stepwise development of more detailed and more efficient versions, supported by semi-automatic tools, such that the overall correctness proof is broken down into the verification of correctness at each step. It is a challenge to formalize the development process itself as a basis for a library of reusable development methods.

Impact and Potential. Government institutions and private industry are starting to require adherence to formal development methodologies in security and safety critical areas. The economic impact of increased reliability, productivity through reuse, and the potential for early prototyping is increasingly recognized.

Original Objectives

The main goals of the COMPASS Working Group are the further investigation and consolidation of the algebraic approach to system specification and development in a comprehensive way. There are considerable needs for clarification, unification, extension and integration of other programming and specification paradigms, in particular, the relationship between the algebraic approach and other formal approaches. The hope is to bridge the gap between the state of the art of the algebraic approach and the practical needs of the specification and formal development of system components.

The COMPASS Working Group brings together the leading experts in the area of (algebraic) system specification and development in Europe. It is expected that its members will continue to have a major influence in the area of formal methods on ESPRIT projects, ESPRIT Basic Research projects and working groups, and national projects. The increased cooperation will lead to further cohesion, consolidation of approaches, and, in some cases, perhaps even some form of quasi-standardisation.

Actions

Apart from many individual joint meetings on specialized topics and visits, there have been business meetings adjoining major conferences at Barcelona, E (1989), Brighton, UK (1991), Orsay, F (1993), Aarhus, DK (1995) and Oxford, UK (1996), COMPASS Workshops at Bremen, D (1989), Nancy, F (1990), Bastei, D (1993), Sintra, P (1994), and International Workshops on Abstract Data Types, jointly organized with the COMPASS WG, at Wusterhausen, D (1990, [5]), Dourdan, F (1991, [6]), Caldes de Malavella, E (1992, [7]), Sta. Margherita, I (1994, [8]), and Oslo, N (1995, [9]).

The primary areas of research were:

1. Foundations

1.1. Models and Logics

1.2. Structure and refinement

2.1. Methodology

2.2. Specification Languages

2.3. Concepts for Environments and Tools

2.4. Theorem Proving

2.5. Term Rewriting

3.1. Software Development Process

3.2. Programming Languages

3.3. Special Applications

Object orientation and concurrency, and structuring of specifications and proofs received a certain prominence.

Results

Algebraic techniques, stimulated by COMPASS members, have already played a dominant role in several national and international research projects, among them various ESPRIT projects such as DRAGON, FOR-ME-TOO, GRASPIN, LOTOSPHERE, METEOR, PEACOCK, PROSPECTRA, RAISE, and SEDOS.

During the first phase of COMPASS [3], over 300 research papers and an Annotated Bibliography [4] were published by group members (not counting those of associated Scientific Correspondents), more than 20% by joint authorship from different teams. More are expected for the second phase; the final count will be available from the update of the Annotated Bibliography [10] shortly. A continuing source of information is the series of ADT/COMPASS Workshop Proceedings in Springer Lecture Notes in Computer Science [5-9].

Another major outcome of COMPASS will be a comprehensive volume on Algebraic Foundations of System Specification [11] (with 14 chapters and a total of about 500 pages), written jointly by 20 authors from the COMPASS WG (with 2 exceptions) and developed jointly with IFIP WG 14.3. Indeed, this latter international Working Group ("Foundations of System Specification ") has been started by members from COMPASS, includes many of the team leaders and will provide some form of continuation of COMPASS.

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.

The significant efforts to move away from individualistic research efforts (occasionally even contradicting each other) to a coherent basis, but with a lot of diversity, deserve particular emphasis. The survey papers written by COMPASS members, often by co-autors from several groups (cf. those invited at WADT/COMPASS workshops in [5-9]), have dramatically clarified the state of the art. During the life of COMPASS, new cooperations between members were established, producing indeed much more coherent views on some topics (e.g. observability). In many such areas, nobody in the field today will consider the topic without starting from the results that have been obtained in cooperation, hence COMPASS was successful in clarification and extension of several existing directions of research.

Group members have also significantly contributed to the development of specification languages and methodologies for development, and also semi-automatic tools and development environments based on algebraic specifications, e.g. the ESPRIT project PROSPECTRA, in which 6 COMPASS members have been involved; the ASSPEGIQUE system has been used in METEOR; the ACT set of tools is integrated into the systems developed in SEDOS and LOTOSPHERE.

It should be emphasized that work under the auspices and cooperation of the COMPASS community has provided a very productive forum for the work of numerous younger scientists, in particular PhD students; the educational aspect should not be underestimated.

Common Framework Initiative for Algebraic Specification

In the original proposal [1] it was envisaged to have an R&D project in the third phase of ESPRIT for a Uniform European Algebraic Language and Environment for System Specification and Development with an associated formal semantics and development methodology.

In fact, such a collaborative effort, the so-called Common Framework Initiative (CoFI), was started some time ago by the COMPASS WG and IFIP WG 14.3 and has been in full swing since Autumn 1995, with the goal of having a first result in Autumn 1996. To have most impact, it is intended as an open international effort, driven by the European COMPASS community but involving people beyond it. Some 25 leading researchers in algebraic specification have already agreed to participate, and others are being invited to join.

The Common Framework is perceived as a major chance for integration and standardization, indeed the very basis for relating existing methods and tools to overcome the apparent gap between theory and industrial application that still exists. For the COMPASS community, there is agreement that only with a common framework, where language and logics serve as a vehicle for communication, will new integrated environments be developed in which specialized methods and tools can coexist; only with such tools and environments, first as public domain prototypes, later in industrial-level versions, will industry be convinced to apply formal methods on a larger scale, whether in-house or with outside help.

Aims and Scope

Quoting from the "Charter" (see [12]) of the Common Framework Initiative for Algebraic Specification:

The rationale behind this initiative is that the lack of such a framework greatly hinders the dissemination and application of research results. In particular, the proliferation of specification languages, some differing in only quite minor ways from each other, is a considerable obstacle for the use of algebraic methods in industrial contexts, making it difficult to exploit standard examples, case studies and training material. A common framework with widespread support throughout the research community is urgently needed.

The current aim is to base the common framework as much as possible on a critical selection of features that have already been explored in various contexts. The collective experience and expertise of the participants provides a unique opportunity to achieve this aim within a short time-span.

The common framework will provide a family of languages at different levels (cf. fig. 2).

   *-*-*  Extension Languages
    \|/
     *    The Common Language
    /|\
   *-*-*  Sub-Languages

The Overall Aims of the initiative are:

• A Common Framework (CoFI) for algebraic specification and software development is to be designed, developed, and disseminated.
• The production of CoFI is to be a collaborative effort, involving a large number of experts (30-50) from many different groups (20-30) working on algebraic specifications.
• In the short term (e.g., by 1997) CoFI is to become accepted as an appropriate basis for a significant proportion of the research and development in algebraic specification.
• CoFI is to include a uniform family of related specification languages, all with a consistent, user-friendly syntax and straightforward semantics. It is expected that some of the CoFI languages could replace existing specification languages.
• CoFI is to be supported by concise reference manuals, users' guides, libraries of specifications, tools, and educational materials.
• In the longer term, CoFI is to be made attractive for use in industrial contexts.
• CoFI is to be available free of charge, both to academic institutions and to industrial companies. It is to be protected against appropriation.

Functionality. CoFI is to allow and be useful for:

• Algebraic specification of the functional requirements of software systems, for some significant class of software systems.
• Formal development of design specifications from requirements specifications, using some particular methods.
• Documenting the relation between informal statements of requirements and formal specifications.
• Verification of correctness of development steps from (formal) requirements to design specifications.
• Documenting the relation between design specifications and implementations in software.
• Exploration of the (logical) consequences of specifications: e.g., rewriting, theorem-proving, prototyping.
• Reuse of parts of specifications.
• Adjustment of specifications and developments to changes in requirements.
• Providing a library of useful specification modules.
• Providing a workbench of tools supporting the above.

The CoFI Family of Specification Languages

Quite important for the success of CoFI is the coverage of most concepts of existing specification languages on the one hand, but, more importantly, uniformity and simplicity. How can these seemingly conflicting goals both be achieved? The key idea here (and the challenge for the design) is not to have one huge specification language, but to impose some structure such that a family of specification languages emerges. It is to consist of three main levels (cf. fig. 2):

The Common Language (CL). This general-purpose specification language is to be the most prominent of the CoFI family: the other languages are to be obtained by restriction or extension of it. CL should be at least as expressive as various existing languages. Its intended applicability is for specifying abstract data types, and requirements and design for programs (at least for programs which do not react with their environment during execution). It is also to be the main topic of the documentation (reference manual, user's guide, text book).

Some Sublanguages (SLs). These are to be obtained from CL by imposing syntactic and/or semantic restrictions. The sublanguages need not have a common kernel. Their intended applicability is in connection with particular kinds of tools (e.g., a first-order equational SL might support tools for term rewriting and completion).

Some Extended Languages (XLs). These are to be obtained from CL (or perhaps from SLs) by syntactic and/or semantic extensions. The extended languages need not have a common super-language. Their intended applicability is to include advanced features well-adapted to specifying requirements and design of systems involving various programming paradigms (e.g., reactive systems, object-oriented systems).

CoFI Task Groups

Various CoFI Task Groups have been defined, with the following coordinators:

Coordination:     Peter D. Mosses (Aarhus)
Language:         Bernd Krieg-Brückner (Bremen)
Semantics:        Don Sannella (Edinburgh
Methodology:      Marie-Claude Gaudel (Paris) /
                  Andrzej Tarlecki (Warsaw)
Tools:            Michel Bidoit (Paris)
Reactive Systems: Egidio Astesiano (Genova)

Language Design and Formal Semantics. The design of the Common Language of the language family will proceed as fast as possible to keep up the momentum. It will be followed by a formal semantics (an absolute necessity for formal methods); here also, the challenge is going to be, how the semantics might be structured, and perhaps how simpler semantics for sublanguages can be derived.

A checklist of language concepts and, based on this, a catalogue of existing specification languages for comparison and easy cross-referencing is being compiled [13]. Language design study notes are being written and the design is well under way.

Methodology. The language design is influenced by methodological considerations. Among the issues to be considered are the role of specifications in the development process (relationship between specifications and programs, formal vs. semi-formal specifications), an abstract view of the development process (refinement and proof obligations, structuring issues, reusability, flexibility and evolution), and techniques for writing specifications of individual system modules.

Introductory material, documentation of development strategies and proof strategies, description of case studies, and libraries of specifications and developments designed for re-use will have to be developed eventually.

Tools. To be used, the language family must be supported by a minimal but widely available set of tools (syntax and static semantics checkers, library support, etc.); to some extent, such considerations influence the design of the language family. A most important aspect is the potential for reuse of an abundance of existing tools. Many of these are specialised, that is only applicable to a particular sublanguage and its associated logics. This raises the issue of multiple logics (see below) and suitable embedding translations, but also of "interchange formats" and means for exchanging libraries of specifications.

Reactive Systems. After the design of the Common Language is in good shape, the design of Extended Languages will proceed in full force. Very prominent among the concerns are language extensions to support state change, reactive systems, and object-orientation.

Multiple Formalisms and Logics

It has already been mentioned that the issue of integrating tools in a common support environment raises theoretical problems of combining and embedding different logics. The general issue of coexistence, transition between and combination of different paradigms and formalisms is an even deeper research issue:

• for heterogeneous systems comprising components developed with different paradigms, e.g. components encapsulating complex data and algorithms, and components for concurrent control and real-time behaviour,
• at different stages of the development, e.g. from a property-oriented specification to an executable program, from temporal logic to a CSP program,
• in a variety of specialised tools, e.g. for validation, prototyping, verification, analysis, or refinement by transformation.

In the particular context of Formal Methods guaranteeing correct software, one universal language or development methodology to cover all problems would lead to unrealistic complexity. It is therefore mandatory to tailor languages, semantics, methodology and tools to specific problem domains to be effective. Then the question is, how to decompose problems and how to combine partial solutions.

A formal framework should be developed, in which various specific paradigms, formalisms, and tools, each as simple as possible for the task at hand, can coexist and be combined in a systematic way. To be able to combine existing software components from a library, to develop heterogeneous systems or to move from one paradigm or tool to another, fundamental problems of semantic consistency and integration, compositionality and interoperability have to be solved.

Logic provides the key for the solution of the semantic aspects of these problems. The semantic core of each specific formalism is mapped to a specific logic. Thus by establishing a firm theoretical basis for relating and combining different logics, a basis for relating and combining formalisms is provided. Specific logics should be related in a Logic Graph. The Logic Graph can be supported by a tool which would enable even non-specialists to naturally navigate to find the formal framework best suiting their needs, e.g. for assembling elementary components or tailoring to the needs of a specialised tool.

The above concerns, both theoretical and practical, have prompted COMPASS members several times over the years to submit various research proposals.

Conclusion

The COMPASS community is now closer-knit than ever. The theoretical basis has been consolidated (cf. [11]), differences between technically different approaches have been bridged, approaches (and people) have matured.

The funding of COMPASS as a European Working Group has come to an end with the termination of COMPASS 2. Efforts to keep the COMPASS community together, to maintain the immensely fruitful cooperation, have to be reinforced; it would be just too sad to see it disintegrate.

I am personally very happy that initiatives such as the Common Framework Initiative have finally materialized and are taken very seriously by COMPASS members (and others); the network of close contacts and friends that has developed over the years in the COMPASS community is probably an essential ingredient here, not only to convince people that such an effort is essential for the future of the research area, its perception in public, its potential for impact on industrial application and its financial support, but also to actually make things happen. In effect, many colleagues have set aside old (and now almost forgotten) technical differences and are willing to melt their pet specification languages into the family pot of CoFI, significantly capitalizing on their experiences, of course. Under the general coordination of Peter Mosses, international support for the effort is growing. Let us hope the effort will be successful, and that some support from the EU will eventually come to bear.

Similarly, funding in the area of Multiple Formalisms and Logics is needed and would have a very beneficial effect on the community in relating their technical work.

Much more work needs to be done by individual groups and in cooperation to make the vision of integrated and industrially useful support environments based on CoFI a reality; these can then gradually be supplemented by individual tools. One effort in this direction is the UniForM Workbench (Universal Formal Methods Workbench) funded by the German ministry of research BMBF [14].

Tony Hoare, in his lecture given at this last COMPASS meeting/11th ADT conference in Oslo, was kind enough to pat our egos by suggesting that we stick to theory (that we do best, apparently), driven by wonderment, cultivating our genuine curiosity, generating results elegant enough to enjoy and admire; he was exceedingly generous to extend such attributes to some of the results from COMPASS. However, many of us are sufficiently ambitious to attempt to participate in the engineering science of developing languages, methodologies and tools. I wish that we would all get our hands genuinely dirty in the future and have an effect, producing something that is really widely used in practice - and still come out with something simple, elegant and beautiful.