computer science research paper conclusion

Conclusion Academic research paper on " Computer and information sciences "

Computer and information sciences

Abstract of research paper on Computer and information sciences, author of scientific article — S.F.M. van Vlijmen

Abstract This document is one of the parts of the electronic version of the PhD thesis by S.F.M. van Vlijmen [91]. The goal of the PhD project was to get a better understanding of the problems with the integration of formal specification technique in the day to day software practice. The approach followed was to execute a number of projects in cooperation with industry on realistic cases. This document start with an overview of the case studies executed. Then are listed observations and conclusions that can be extracted from the case study evaluations. These observations and conclusions are then confronted with the hypotheses to be tested. The overall conclusion about the usefulness of formal specification technique turns out to be rather negative. A discussion on further work ends the chapter.

Academic research paper on topic "Conclusion"

Electronic Notes in Theoretical Computer Science 21 (1999)

URL: http://www.elsevier.nl/locate/entcs/volume21.html 38 pages

S.F.M. van Vlijmen

Faculty of Philosophy, Utrecht University Heidelberglaan 8, 3584 CS, Utrecht, The Netherlands

This document is one of the parts of the electronic version of the PhD thesis by S.F.M. van Vlijmen [91]. The goal of the PhD project was to get a better understanding of the problems with the integration of formal specification technique in the day to day software practice. The approach followed was to execute a number of projects in cooperation with industry on realistic cases.

This document start with an overview of the case studies executed. Then are listed observations and conclusions that can be extracted from the case study evaluations. These observations and conclusions are then confronted with the hypotheses to be tested. The overall conclusion about the usefulness of formal specification technique turns out to be rather negative. A discussion on further work ends the chapter.

As mentioned in the preface, the goal of the project was to enhance the understanding of the application of algebraic specification; shed some light on the mismatch between enthusiastic proponents of formal specification technique and reluctant practitioners; show the potential of algebraic specification and the formal specification technique in general; get feedback from practice; and find ways to bridge the gap. Assumptions, beliefs and ideas that endorsed this effort have been presented as hypotheses in Section 41 of Chapter 1 of [92].

In the project, a number of cases was studied in which the central technique was algebraic specification. Nine of these are discussed in this thesis. In an introductory chapter, a succinct overview was presented on process patterns, methods, techniques, notions and terminology from engineering and software engineering. This material serves as a context and to structure the evaluations that accompany the chapters on the nine cases as well as the discussion in the conclusion.

1 Note that references are made to chapters and sometimes to sections that may be stored as separate files at the ENTCS site [92]. The original text has been partitioned into: preface and the Chapters 1 to 8, each part is stored in a separate file, and each part has its own bibliography and appendices. To circumvent confusion, a reference to a part of the thesis outside the part at hand is followed by a bibliography style reference.

Case cpt reg com ctr rtm

app spc app spc app spc app spc app spc

Traffic Control 0 0 0 0 0 0 + + + 0

Protocold 0 _ 0 _ 0 _ + + + _

GSE 0 _ + _ 0 + _ + _ _

VPI 0 0 _ _ 0 _ + + + +

CDB + + 0 0 0 0 + + + +

Model Factory _ _ _ _ 0 + + + 0 _

SIBs 0 0 0 0 + + + + + 0

IDEAL 0 0 _ _ + + + + + +

Lamp Remplace + + + + _ _ 0 0 _ _

Overview of the cases with respect to the focus of the application versus the specification. Legend: app = application; spc = specification; cpt = computation; reg = registration; com = communication; ctr = control; rtm = real time. Plus '+' means clear emphasis; zero '0' means that the aspect is apparent but not dominant; minus means of minor importance or not contained.

I start in Section 1 with an overview of the ease studies that highlight aspects that I will use in the rest of the argument. Section 2 presents observations and conclusions on the technical and software engineering aspects of the application of the project languages. Then, the qualities from Section 2 of Chapter 1 of [92] are discussed in the light of these observations and conclusions (3).

In Section 4, the focus is on applied research of formal specification technique in cooperation with industry. Observations and conclusions presented here may come in handy for further work in the field.

A summary of the conclusion follows in Section 5. Here the main results are confronted with the hypotheses. Some remarks summarizing the weak and strong points of the project languages, and comments on opinions from the literature are also given here. Next, I consider how the main results may stand amidst formal specification technique in a more general setting (6). The chapter ends in Section 7 with ideas and suggestions for further work. This is a succinct discussion on what appears to be the feasible directions and forms with which one may successfully continue this type of applied research.

1 Overview of the eases

In this section, overviews of the cases are presented by means of a number of tables. Table 1 characterizes applications and their specification on five tvpi-

Case Language

Traffic Control PSF

Protocold BPA(-f)

GSE PSF, InterWorkings

VPI ASF+SDF, psCRL & modal logic, propositional logic, C

CDB ASF+SDF, ToolBus, Perl, TCL/TK, Cplex

Model Factory PSF

IDEAL ASF+SDF

Lamp Remplace ACP, PSF, Pascal

The languages used in the nine cases.

Case type of engineering activity

UoD obj req dec imp frw rev ree val ver

Traffic Control 0 _ + + _ _ + _ _ _

Protocold _ _ + _ _ _ + 0 _ _

GSE 0 _ _ + _ _ + + _ _

VPI 0 0 + + _ _ + _ _ +

CDB 0 0 + + + + _ _ 0 _

Model Factory _ _ _ + _ _ + _ _ _

SIBs _ _ _ + _ _ + + _ _

IDEAL _ _ _ + _ _ + 0 _ _

Lamp Remplace 0 0 + + + + _ _ 0 0

Overview of the cases with respect to engineering activity. Legend: UoD = Universe of Discourse; obj = objectives specification; req = requirements specification; dec = decomposition specification; imp = implementation; frw =

forward engineering; rev = reverse engineering; ree = re-engineering; val = validation; ver = verification. Plus '+' means clear emphasis; zero '0' means not dominant; minus means of minor importance or not considered.

cal computational aspects: computation, registration, communication, control and real time. The first four stem from Wieringa [99]. I added real time. There are three levels of containment of an aspect, indicated by '+' (clear emphasis), '0' (aspect clearly apparent but not dominant), and (of minor importance or not contained). The valuation is relative to the application as a whole, respectively the specification as a whole. For example, the specification can pay much attention (+) to a feature that is of minor importance in the application (0).

To illustrate how to read the contents, consider GSE. The editor (app) is not really computation (cpt) intensive. However, the parsing for structured editing is not trivial. Therefore, I valuated the aspect with '0'. In the specification, the computational aspect does not play a role whatsoever. Therefore, I have chosen '-'. Registration (reg), which means gathering text in this context, is an important activity of the editor ('+'), but not for the specification ('-'). Communication (com) and control (ctr) are not a main issue for the editor ('0' and respectively). It is, however, the major subject of the specification (both '+'). Finally, real time is neither a topic in the editor nor in the specification.

Table 2 lists the formalisms 2 used per project. Table 3 shows how the work can be characterized following the engineering terminology from Chapter 1. The scale (+, 0, -) is the same as used in Table 1. For the cases Protocold and IDEAL, the characterization in Table 3 concerns the characteristics of systems intended to be specified with these languages.

The data in the Tables 1 and 3 are coarse and (I fear) subjective, as well. Nevertheless, I think they suffice to elicit some major characteristics. Furthermore, they help endorse words of caution that put the conclusions found in the coming sections in perspective. First, from Table 1, it follows that the majority of the systems have a strong control bias. Other aspects have obtained less attention, especially computation and registration. All aspects have appeared in the specification work, i.e. all categories score a '+' in the 'spc' field at least once. Nevertheless, some caution is called for when the conclusions concern systems that differ from more or less technical control systems, for example.

Second, from Table 2, it is clear that only a few specification languages have been used, and moreover, from one particular corner of the spectrum (see Section 3.4 of Chapter 1 of [92]). This was, of course, known from the start. However, some observations used to support the conclusions may not be valid if I had used other languages. Sometimes I will comment on this in passing. However, Section 6 is especially devoted to this issue.

2 The various specification techniques used in this thesis are not accompanied by preliminaries, as these are easily accessible in the literature. The languages used, together with some general references, are: ACP, [11,4]; PSF, [72-74,86,87]; Synchronous Interworkings, [75]; pCRL , [53,54]; the modal logic for pCRL, [55]; ASF+SDF & ToolBus, [63,37,9,10]; and prepositional logic [34].

Finally, Table 3 clearly shows other 'imbalances'. In the majority of the cases, the specification is a decomposition specification. By this I mean a description in which operational and structural aspects are dominant. Please note that most cases are of the reverse engineering type. These two observations are related for two reasons. First, this is how such a project apparently works. You start with existing systems, gain experience and eventually get involved in forward engineering. Please note, with respect to this, that CDB and LE are the final cases executed in the project. Second, given an existing system, it is relatively easy to write a specification at that 'low' level. This project is somewhat weakened by the fact that I did not pay more attention to the other types of specification. In my opinion, the languages I used are not particularly suited for other types of specification than decomposition specifications (see Observations I and J), Although the other areas of specification are represented more weakly, I feel confident that some relevant observations can be made here.

2 Application of the project languages

In this section, the technical and methodical experiences with the project languages are compiled, A discussion covering the qualities of the specifications produced in the cases plus the project organization follow in the next two sections. The results gathered in these three sections are confronted with the hypotheses in Section 5, In Section 6, I will discuss to what extent the conclusions here carry over to algebraic specification technique in general and formal specification technique as a whole.

Position statements in the rest of this chapter take the form of conclusions and observations. Observations summarize a number of points that are of a supportive nature to conclusions. Conclusions and main observations are identified with roman numerals I, II, ,,,; other observations are named A, B, et cetera.

2.1 Basic applicability

In all cases, we reasonably succeeded in specifying meaningful self-contained texts. That is, the project languages did not fail in a severe way. If we then consider the Tables 1 and 3, it appears that the cases cover a wide range of computational aspects, including language engineering and various types of engineering deliverables. This leads to the following observation.

Conclusion I. The project languages can be used for the specification of at least some deliverables in the development of a wide range of systems, whether in forward, reverse or re-engineering. There is no doubt about the basic applicability of the project languages.

There were troubles. With the VPI, /iCEL was not sufficient to express all requirements (e.g. when signal A shows red, then ,,,), With LE, it was a burden to shoehorn the mainly registration biased system in PSF, The point is that in all cases you can successfully specify some deliverable: /iCEL was successful as the formal basis of the whole project; PSF was able express the decision support system, but I skipped one level in the system decomposition. Of course, one should not do that.

At this point in the argumentation, the above conclusion does not yet say much. It merely states that there are plenty cases in which you can write sensible texts in the project languages. Below, I embed the statement by presenting observations on the apparent weak and strong points of the project languages,

2.2 Methodical support

Formal specification technique is not homogeneous terrain, nor are the project languages one and the same. They differ, for instance, in the two following ways. First, in their suitability to model certain computational aspects, e.g. the aspects in Table 1, Second, in their suitability at a certain level in product development. We find examples of this in the cases, ASF+SDF was the language for the syntax and semantics of IDEAL, Nobody would favour ACP here, /iCEL was not suited for the requirements to be imposed on interloek-ings; the modal logic was. Nevertheless, /iCEL was successful for a detailed operational specification. The module constructs of PSF render this language stronger for an initial specification of the traffic regulation system than /¿CEL. However, if verification was the issue, we might have opted for /¿CEL.

What was and is known about the use of the project languages? It appears that the project languages are merely technical results, that the practical and methodical underpinning of their use in software engineering is weakly developed, at least ill-documented, and that it was not a serious issue in the years in which I worked on the cases. The lack of methodical underpinning is a severe handicap for practical use, especially by non-intimates. This is a discrepancy that needs attention. After all, the research groups that work on the project languages think their work has practical value and they have the clear ambition of having their work applied.

In other words, the project languages lack firm statements that link the languages into methods and that supply clear and motivated rules for use, e.g. rules specifying the circumstances when language must or must not be used, how to specify, how to proceed with validation and verification in practice, how to document, how to carry out version management on specifications, I don't mean that this all has to be invented. It is readily available — the connection must only be made. In Section 7 on future work, I discuss how to make this connection. Still, the observation is:

Observation I. The project languages were not, and are still not accompanied

by elaborate guidelines endorsed by convincing practical work that specify when and how to use them in practical and methodical software engineering.

Documents and work by the 'project language groups' that addresses methodical issues are: the thesis of Brunekreef in which styles of specifications are discussed [25]; the project that aims at the formal development of a /iCRL toolbox in /iCRL [35]; the systematic approach of Verhoef in the set-up of a reverse engineering factory [22]; the elaborate treatment of ASF+SDF for language prototyping in [37], However, this is a minority of the published work.

The observation above does not mean that specifications are isolated assertions that show no links to reality. The opposite is true. In the cases, the languages often function as a mathematical glue in which notions of many domains can be presented and manipulated. Examples are /iCRL in the VPI case and PSF in Lamp Remplace, In the latter, the operations research optimization functions could be sufficiently presented by their signature, input and output data structures only.

Nevertheless, the differences in the applicability and suitability of languages for certain domains and certain stages of product development mean that it is impossible to avoid using more than one language in project development, This is clearly supported by the cases, see, for instance, the VPI case in Table 2,

Observation II. There is a need for multiple languages in one project.

When multiple languages are used in a project, their interrelation becomes an issue. Using a combination of languages is difficult and tedious if complete formality and rigour is at stake. With respect to this, consider the semantical problems with wide spectrum specification languages as Cold, Nevertheless, clear interrelations are certainly not beyond reach, I expect, however, that an informal link may suffice in many cases. That is to say, in an academic setting. For industrial application, more rigour is most likely needed because industrial users may be less aware of pitfalls, and therefore, need protection. Some work has been done to integrate the project languages, e.g. the Tool Interface Language [87] that enables simulation of /iCRL by means of the PSF Toolkit, I suspect that we must observe that, from a software engineering perspective, combination and position of the project languages in development is not seriously studied. Local syntactical and semantical issues of the project languages attain far more attention.

Observation III. The project languages are isles.

With the above observations, the tone for the main line of thought of this section is set: a lack of methodical support. The observations presented above focus on the project languages as a whole. Below detailed discussions on languages constructs in the light of methodical support follow. In essence, the points put forward below suggest a weak support of means that may faeil-

itate integration of the project languages in software engineering processes. Specifications evolve, ripen, change and grow just like any other artefact. Furthermore, engineering is not only product development. It is also concept development, sedimentation of domain knowledge and heuristics as well as generalization of this in theories (including mathematical theories). Formal specification technique may well be the lingua franca in software engineering for meta project communication and reflection. However, support for this does not yet seem very elaborate.

In the specifications it is often difficult to judge the roles and the state of the specified elements, e.g. sorts, functions, assertions and modules. In particular, it is not possible to differentiate between the following in an integrated and language-supported fashion:

A. Meaning of conditions. Whether a guard testing the delineation of problem domain and chosen solution, or just a member of a case distinction within such a delineated space.

B. Status of modules. Whether concept, draft or finalized.

C. Purpose of a 'modularization. Whether for presentation or system decomposition.

Others have noted the confusion surrounding the above, too, Johnson says in [60] about projects with GIST, "We needed ways of describing the intended roles of components of high-level specifications",

As addressed above, modelling of error and exception handling are a source of conditions and symbols with a possibly difficult status. In the cases, I bumped into error and exception handling but skipped an elaborate treatment because, despite its importance, it was in conflict with the bridgehead strategy in two ways. First, it aggravates the communieability of the specifications because extra symbols and axioms are added — not a nice property of initial and already longwinded texts. Second, it is tedious, and we'd better make sure to start a new project. The point here is that, to my knowledge, there has been no systematic study of practical approaches to error and exception handling and its roots in partial functions for specifications in the project languages. At least not for the general case. Specific techniques have been defined for language engineering in ASF+SDF, e.g. generic error messages and origin tracking [37], Recent theoretical work is [14], Other references can be found in [17], A specific approach, with additional notation and error objects, is proposed in [59], Van Vliet argues that error and exception handling in algebraic specifications is difficult [90], I don't believe that it is a problem with algebraic specification in particular, I suppose that formal specification merely exposes the true severity of error and exception handling. Hence, it is omnipresent. For example, in VDM-SL, one uses a three-valued logic to cope. In Z, one choose not to do so. Clearly, the discussion is still open.

D. Systematic and practical approaches for error and exception handling have attained sparse attention in the design of and documentation on the project languages.

During the writing of a specification, a lot of ideas and reminders spontaneously come to mind. The languages offer no support to directly capture these in a structured manner, A typical example of this is the following. When one writes process definitions and data types in parallel, there is a risk that the particular use of the data terms by the processes or the particular occurrences of data terms in the processes negatively influence an objective view of the data type. In the worst case, it only caters to the process related cases. This may be acceptable in some cases, but only when accompanied by a clear statement or precondition,

E. Important assertions about the specification itself are easily lost. Typical examples are theorems on the data types and process terms, but also on the effect of imports on sorts, e.g. whether the import is intended to be persistent.

The above observation is about relations between specification objects. The same can be said about the relations between specification objects and their real world counterparts and contexts,

F. Assumptions about the part of the world the specification describes are easily lost.

I think it is necessary that these ideas are captured as a part of the specification text, not in a separate document. Literate programming is to some extent proposed to circumvent the problems captured in the above two observations [67], Brov makes similar observations about the Larch Proof Assistant, He argues that there is a clear need for support of the management of theories [24].

The means that are offered by the project languages are a step in the right direction, in particular, modularization, parametrization, hiding and a distinction between generators and operators. But, in my experience, they are not sufficiently elaborated. For instance, in PSF, a module can only specify what is exported from the objects introduced by the module; it cannot hide imported objects. This causes difficulties when it comes to reusability: the top module may export functionality that is not requested in a requirements document, ASF+SDF is another example. It does not offer the convenient parametrization and renaming facilities of PSF, It should be noted, however, that fundamental work on features like modularity, renaming, parametrization, polymorphism and higher order functions is in progress. See the work on module algebra in [8,83], and the extensions of ASF+SDF in [37,89],

G. There is a need to extend the hiding and export mechanisms.

All points in the above can also be mitigated and partly overcome by writing comments in the specification. However, these comments are hard to interpret by machines.

Software engineering problems that are well-known at the implementation level reappear at the specification level. Nevertheless, there are no means for version management, administration of evolution and refinement, documentation and maintenance of specifications. There are many CASE tools around [42,88], In [33], Craigen and Ralston recommend the incorporation of ideas from CASE and software engineering environments. The point is that, to my knowledge, no one has yet investigated how these kinds of tools could be used to support the use of the project languages. What is lacking, and what works well? In my cases, the specifications are small and mainly cover a tiny fraction of product development. The need for additional support, as suggested above, was really only noticed in the VPI case. Here, ASF+SDF specifications were written of a number of transformation tools. When Wilco Koorn commenced with the implementation of the tools in C, it became an issue to maintain a clear relation between specification and implementation. We did not maintain the relation; the costs were too high,

H. .U with implementations, specifications also need to be documented, managed and maintained. There is no real support offered yet.

Automatic generation of implementations from specifications may abate the trouble sketched above. It is doubtful whether this will be enough. There is a real chance that there will often be specifications at a level of abstraction that does not lend itself to automatic code generation. Then the problem moves just a 'language level' up.

The following points are of a more syntactical and semantical nature. Nevertheless, the methodical consequences are also clear.

As noted above, it may be difficult to elicit motivation for modelling choices for the unprepared reader. Examples of this are found in the specification of the traffic regulation system (endless nestings of functions) and the numerical library of van Wamel [98] (the nat("l"2"3) notation). Furthermore, in general one needs auxiliary objects in algebraic specifications. One cannot restrict oneself to properties of the desired functions [90], This is a theoretical fact [15] and can be a source of distraction,

I suspect that these notational inconveniences are not that problematic for specialists at some level further down the system decomposition. The representation becomes more important at higher levels of specification, close to or at the requirements level where non-specialists are involved. In a number of cases, the notations distracted our industrial partners (VPI, Traffic Control, Lamp Remplace), But the strict equational style of /iCRL and PSF forces one to dive directly into notational detail. This can perhaps be mitigated by extra text, but extra text can also lead to extra faults, ASF+SDF is clearly more expressive and flexible at this point. Furthermore, the ToLaTeX prettvprinter of ASF+SDF allows for nice presentation and a choice of compact and familiar symbols.

I. Often, modelling choices are motivated by the syntactical and semantical weakness of the languages. Most notable are data types in fj,CRL and PSF.

A semantical problem is that project languages which are based on equa-tional logic and/or process algebra have a strong operational bias, e.g. in process algebra, one tends to generate a space instead of a specification of its boundary, and one tends to specify the behaviour of data structures in term rewrite rules. This makes them less suitable for specifications at the requirements level. In this case, a declarative style is more suitable. Such styles could include plain mathematical style, notations from first order logic, derivatives as modal logic, and set theory. These are compact and offer the flexibility and expressiveness that seems better suited for requirements specification and initial system decomposition specifications. The VPI case supports this point. The re-specification of Lamp Eemplace in [97] may also serve as support (graphical presentation with first order/modal semantics), as could the alternative specification of the traffic regulation system in [68] (timed process algebra notation + first order logic and set theory). Other support is the fact that 'popular' specification languages (Z, VDM-SL, Larch) offer a rich set of operators from first order logic and set theory,

J. Requirements specification in the project languages is difficult due to syntactical and semantical obstacles. They seem more suitable for the more detailed lower levels in product development and an operational style.

Therefore, in general, the project languages do not offer support for all levels of specification in product development. The project languages are not wide spectrum languages, they are thematic, i.e. they exploit specific paradigms [12], Nevertheless, it must be stated in light of the hypotheses about ambitions of the project and the project languages. The advantages are also clear: the theory behind the project languages is relatively simple, resulting in well-defined and understood languages; e.g. verification techniques for /iCRL are advanced, ASF+SDF and the ToolBus are powerful means for prototyping and implementation. The following conclusion summarizes all the above observations.

Conclusion II. The project languages are not accompanied by clear methodical guidelines, or engineering process considerations, or embedding in development methods. Furthermore, the languages do not offer sufficient means to facilitate smooth integration in a software engineering process method. Finally, the support for integrated, gradual and multi-level development (from requirements down to implementation) is weak.

2.3 Formal versus informal

A specification can be viewed as a theory about a need and a solution: the system. This is particularly true of a formal specification. The following five points illustrate that embedding a theory in an informal context is important

for the correct interpretation of a theory (a formal specification), and essential for the validation of the theory.

First, what does the structure and wording of a specification imply? Is a decomposition into a certain set of processes imperative, i.e. are these processes supposed to actually run on separate processors, or is it a means of presentation merely to achieve specific external behaviour for test purposes, or is the decomposition a detailed study of sequential components 3 ? Similar comments can be made about the modular structure and the choice of function names. To generalize, the 'what', 'why' and 'how' leave much room for interpretation if the specification is not accompanied by clear documentation, EUEIS is an example of the confusion that may arise when the position of a text is not clear (see Section 1,3 of Chapter 1 of [92]),

Second, lack of expressiveness forces one to use oblique formulations that may distract the reader from the main line of thought and thus encourage divergent interpretations. For example, the list notation for elements of N and the use of an injection function to the naturals in order to succinctly define an equality function.

Third, the writer and reader do not neeessarlv need to have the same intuition and knowledge of the real world notions represented by a specification. Abstractions and generalizations are choices. These need not be as logical, objective and obvious to the writer as to the reader. Writer and reader may not agree on whether assertions about the world have the status of assumptions, hypotheses or facts. These differences are sources of divergent interpretations. Fourth, a proof of correctness is, in general, an argument that an assertion holds about a model of a system that resides in a hypothetical world. There is no single answer to the value of the proof in practice. The value greatly depends on the validation of the specification.

Fifth, a reasonably formal proof of a property of a system modelled by a specification is often out of scope. Rigorous reasoning is a useful alternative, but because one often makes use of 'well-known' properties of the informal world, it greatly depends on a valid relation to the informal world,

K. Formal specifications can only be properly written, interpreted and validated when the specification is carefully embedded in the informal world.

In my experience, formal specifications do not possess natural obviousness. They are horrifyingly local, ad-hoc and particular. Naturally, this is no new pattern. It is typical of empirical science, I see two consequences here.

First, it shows that software engineering is, in many cases, not yet engineering, It is a mix of empirical science and engineering. This observation is also made by others [56,23,99], Brinksma puts emphasis on the language incorporated axioms about general system behaviour. Process algebras are

3 For an example of the latter, see Observation L further below.

a good example of eases in which this is elaborate and explicit. There are three sources when a conflict between the specification and the system under design is detected: the language axioms, the theory about the system under construction or the current decomposition specification, A similar remark has been made in the evaluation of the case on Protocold (Section 7 of Chapter 3 of [92]).

That specifications and their implementation often tend to diverge may be seen as an argument in favour of the position about the convolution of empiricism and engineering. Divergence is rejection of the theory (in cases when the decomposition is right). Models such as ('MM respond to this divergence by placing emphasis on the evaluation of projects. The outcome can be used to adapt the theory and thus reinforce domain and system knowledge. This process may eventually lead to texts with an autonomous and natural obviousness, However, a similar trend, incited by pragmatism and not idealism, may be seen in the advancement in the modelling power of, for example, database systems of major vendors such as Oracle,

Second, Observation K suggests that the application of formal specification technique in forward engineering, especially in a completely new domain, may be cumbersome. In the cases, two may classify as forward engineering: CDB and LE, see Table 3, With CDB, ASF+SDF essentially blurred the view on the concepts. Please refer to the evaluation of CDB, Section 7 of Chapter 6 of [92], for details. To a lesser extent, this was also the case with LE when PSF was used. It seemed that formal specification did not necessarily lead to good insight into the peculiarities of the projected systems. It may well be the case that informal modelling and prototyping should be carried out first, or concurrently, to strengthen the intuitions about the key notions, features and functions of the projected system. The GSE case also supports the point, twofold; to some extent GSE takes a middle position between forward and reverse engineering. First, interaction between the editor components was not functioning, A solution was proposed: a forward engineering activity, Interworkings were used as a means to built the necessary intuition, before the final text in PSF was produced. Second, Section 3 of Chapter 4 of [92] (the evaluation of the GSE case) includes the information that van Waveren, van Wamel and myself were engaged in the birth of the ToolBus, and more important, how we failed to formally capture the ideas expressed by Klint and Koorn due to a lack of intuition on our side. We were bogged down by our process algebra.

Observation IV. The project languages worked fine when the intuitions about a system were strong; the key notions, features and functions were familiar and stable.

Apparently, one must be careful in other cases and be ready to experiment and prototype. The feedback gained through this may then be used for writing formal specifications. In [47], a reference is made to a cognitive science study

by V, Goel that "suggests that in the early stages of problem solving, when the problem area is relatively ill-structured, the use of formal representations inhibits the exploration of alternatives and is detrimental to the quality of the outcome",

2-4 Concurrency

Finally, a remark on ACP, A strong point of ACP that may be overlooked is the 'other face' of concurrency or parallelism in ACP, The obvious concurrency is: one or more fairly autonomous processes that happen to communicate from time-to-time. The typical example is two or more systems and a network. The less obvious form is concurrency to isolate the behaviour of parts that are strongly related, to the point of sequentially, I noted this when carrying out specification work. Nevertheless, there are no clear instances in the cases in this thesis. An example of the other face of ACP can be found in the specification of the semantics of EUEIS in [7]. Here, certain entities are modelled as processes; entities that in an implementation are most probably largely modelled by plain data structures. Furthermore, ACP allows one to integrate isolated parts into larger, less partioned processes, and study equivalence,

L. The || in ACP models concurrency, but also allows the isolated study of elements that function in a sequential context.

3 Qualities and formal specification revisited

There is one severe problem with the discussion of the qualities in Section

4 of Chapter 1 of [92], and in the following. There is no objective measure. The problem starts with the rather informal and intuitive description of the qualities themselves. Therefore, it is wise to attempt to succinctly identify some relevant observations in order to elicit some of the major issues and avoid details that are too sensitive for subjective interpretation,

(i) Communieability,

It is interesting to consider some observations on the audiences of the respective case study reports. In the majority of the cases, the audience was unacquainted with formal specification technique. Such audiences form the most interesting observation category. The clear exception is Protocold, and GSE to some extent. The SIBs do not count, because we never met the audience. This leaves 7 cases, if I include GSE, Here, the typical reaction was "you understand, we did not read that part of the text", I virtually never got a reaction about a specification. The caveat I would like to insert here is that there were no strong incentives for the audience to read the specification: in order to check our understanding of the domain, one could get away with reading the introductory sections and the conclusion. Furthermore, the specifications are all written in one type of language. Maybe other notations would have led to clear

reactions. Thus, with respect to formal specification novices, the specifications apparently did not encourage reading or arouse curiosity, GSE was clearly a negative experience (see Section 3 of Chapter 4 of [92]), Communieabilitv is inconclusive,

(ii) Trueness, Completeness, Feasibility, Verifiabilitv, and Correctness,

I have had no negative experiences. This comes as no surprise, at least for the last three qualities. It is probably a direct consequence of the fact that specification in the project languages is very down to earth, concrete and allows for formal reasoning about properties. Despite this optimism, a proper embedding in the system context, stability of concepts, and clarity of intuitions is a prerequisite for a positive score. Please refer to Observations K and IV,

(iii) Traceabilitv, and Maintainability,

I cannot say anything about this. Apparently the cases were simply too small to elicit gripping intricacies and idiosyncrasies that can be related to traceabilitv and maintainability. The maintainability issue did occur (VPI), but to the extent that we can say that specifications also need maintenance, the same as other deliverables (see Observation H), I expect, however, that a 'higher degree' of traceabilitv and maintainability can be reached than with documents that are solely informal due to the fitness of formal specification for machine manipulation. Sticking with the project languages, support for this claim comes from a project by First Results, There, CVS is used with success to do the version management of a large ASF+SDF specification [64],

(iv) Reusability,

Reuse is found in the cases, albeit on a very modest scale: the specifications of basic data types are reused, e.g. queues and tables. The library for PSF was especially extensively used [98], Reuse at a more domain-specific level did not take place, at least not to the extent that would allow many observations to be made, except the following. At the level of formal texts, reuse is simple to achieve: cut and paste. However, a word of warning would be suitable here. Given a situation in which formal specification are reused, I expect that a consequent strive towards generality and implementation independence would lead to abstract terminology, i.e. application independent terminology. For some applications, this may lead to extra documentation that describes the relation between the general notions and the application specific notions, and extra layers to connect components to specific environments. This may have a negative effect on communieability, because the amount of documentation and layering of notions increases, unless the parties involved are accustomed to the reused specification. Furthermore, reuse means reuse at a number of levels of specifications, formal and informal. This can be a difficult and time consuming task.

The above discussion of the qualities reveals how hard it is to say something concrete about the properties of formal specification technique and the benefits of the use in software engineering. Therefore, it reveals the need for a far more rigid and systematic approach of assessment. In other words:

Conclusion III. The assessment of the qualities is largely inconclusive. Objectivity of the assessment of qualities needs to be enhanced. Furthermore, for a fair and reliable judgement, cases need to be studied more extensively: over a longer period of time, with a number of specification approaches in parallel, and with, at least once, the completion of the whole engineering cycle. Moreover, the involvement of the 1audience' needs to be intensified.

In [80], Pfleeger and Hatton give an example of how such a comparison could be set up. Many authors lament on the lack of metrics and useful historical data [33,84],

4 Applied research

In the previous section, the cases were considered from a mainly technical perspective. In this section, I will present a number of observations from a project management and project strategy perspective. How did the projects function? These observations will be used in the final section as a basis for suggestions and ideas that may contribute to the success of continued work in the field of application of formal specification technique. In this section, I use Table 4 extensively and begin to expound on the contents of the table.

The first two columns specify the effort in man months by participating research institutions and industrial partners respectively. The next two columns specify the technical reports and publications (journals & proceedings) about the work. The fifth column specifies whether or not the project was a paid assignment. The sixth column shows the number of follow-up projects. This is taken very liberally. Every separate action that followed is counted, from practical assignments and students up to assignments and serious cooperation projects. The technical reports and publications that resulted from the follow-up are specified next. The next to the last column specifies the state of the bridgeheads. There are four categories: evaporated, i.e., the subject lost relevance, or the industrial partner left the subject; terminated, i.e., the theme is abandoned and is unlikely to be reanimated in the near future, or we lost the subject; dormant, i.e., no current activity, but new work can commence reasonably easily; active, i.e., work still in progress. The final column specifies the number of years between the start of work on the bridgehead and

4 Lamp Remplace and CDB were the 'ask' follow-up for Traffic Control. For VPI and IDEAL, the 'ask' follow-up came in the form of an assignment from Holland Railconsult about EURIS. This project was, in turn, followed by an assignment by Rail Infrabeheer, which was executed in cooperation with Holland Railconsult. Neither project is reported in this thesis. Please refer to [7,38] resp. [49].

Case amm imm rps pbs pas fpr rps pbs ste cc

Traffic Control 5 0.25 [96] no 5 [27] [68] d 2

Protocold 3 0.25 [94] no 0 t

GSE 5 0.5 [93] no 0 e

VPI 8 1 [50] [52] no 5 [45] [46] a 3

CDB 9 1 [65] yes 0 d

Model Factory 3 0.25 [95] no 4 [58] e

SIBs 5 0.25 [66] no 1 [28] e

IDEAL 7 0.5 [18] no 3 [78] [6] a 3

Lamp Remplace 14 1 [40] [41] yes 1 [97] d

Overview of the cases with respect to effort versus impact, spin-off and results until June 1998. Legend: amm = man months by academia; imm = man months by industry; rps = technical reports; pbs = publications; pas = paid assignment; fpr = number of follow-up projects; ste = state: evaporated; terminated, dormant, active; ask = lead time to clear mutual interest in years.

the first sign of substantial reverse interest by industry, e.g. in the form of an assignment.

Now, let us recall the strategy as formulated in the preface. There we read that the idea was to start work in various areas (bridgeheads) and encourage the continuation of the work by others. The cases in Chapters 2 to 7 prove that it is certainly possible to make starts, i.e. develop a subject and a theme from an application domain. This is also reflected by the fact that the work found its way into the literature (see Table 4), despite a lack of effort to publish. In other words, in all areas studied in the cases, one can find scientifically

relevant subjects for study that lend themselves to theory formation. It is also clear that formal specification technique is a useful format for this study. This sounds wonderful, but to put things in perspective see Observation IX further below.

Observation V. The development of themes from application domains is feasible.

Therefore, starting bridgeheads is not the problem. There is a clear difference, however, between the moment we start to establish domain knowledge (start of the project) and the moment that the industrial partner recognizes that we have established some domain knowledge. This latter moment is considered to be the moment when the industrial partner poses us a questions about its own domain. Table 4 clearly shows a long lead time to the moment the interest becomes mutual (see column 'ask'). It goes without saying that mutual interest is beneficial for the profoundness of the research effort.

Observation VI. It takes some years before a body of knowledge that is recognized by the industrial partners as relevant is established.

Starting a bridgehead is not without risk. The state (column 'ste') in Table 4 concerns the original partner. It disregards the fact that, in some cases, we could have teamed up with another partner. The table shows that four domains were discontinued (qualification t and e): the industrial partner terminated the site/subject (Model Factory, GSE), we lost the subject (Protocold) or the industrial partner changed its priorities because of market dynamics (SIBs), Three others (CDB, Lamp Eemplace, and Traffic Control) are dormant at the end of 1997 because of a change of priorities by the industrial partner. However, the work went on, though at a low key and not continuously. This concerns the re-specification in TRADE, and the publication on Lamp Eemplace, Nevertheless, I judged 'active' for Lamp Eemplace and CDB too high a rank. Therefore, only IDEAL and VPI were active: assignments from Holland Eaileonsult and Eail Infrabeheer,

Observation VII. There is a real chance that, after a couple of years, a theme becomes temporarily less prioritized by industrial partner, looses relevance for the industrial partner or is abandoned by the industrial partner.

As stated above in Observation V, one can feasibly start a theme. However, it is an altogether different task to arrange, motivate and encourage a flowering follow-up. Again, Table 4 clearly shows how projects die out. This can be partially imputed to the instability of the domains as stated in the observation above. But the work itself also does not attract researchers. Maybe the trouble is that the scientific content of work that lies more in the realm of software engineering than mathematical theorems is not valued by researchers. Maybe this is a consequence of the background of the people that form the research community. Follow-up only succeeded when it was explicitly pursued and encouraged by the originators of a case (e.g. the Model Factory was pushed

by Jan Bergstra),

Also, the industrial partner often hesistates to carry out sufficient follow-up, At least three projects (VPI, CBD and LE) resulted in prototypes that clearly show some product potential. This is not only my view, this is also endorsed in personal communication with our contacts. Nevertheless, none of these results was used. They did, however, add to our credibility. For example, without work on the VPI case, I believe that the EURIS project would never have been granted. In conclusion, we observe the following with respect to the strategy of the project.

Observation VIII. Themes did not sell themselves in the academic setting, nor did research results sell themselves in the industrial setting.

To summarize the observations in the above, themes can be found in and developed from application domains. However, it takes quite some time to gain interest, and bridgeheads thus formed are threatened by the evaporation of the domain and lack of follow-up. In order to fight these threats, I believe that more attention must be paid to organizational aspects. This point is put forward in the section on future work (7),

Below are three observations about the state and achievements at the bridgeheads, the choice of the languages and the disciplines involved in the projects.

The following can be noted about the state and achievements at bridgeheads, First, no project completed the whole engineering cycle. Moreover, Table 3 and the evaluation sections on the cases show that most specification work is at a rather detailed level of system decomposition. Requirements analysis and implementation have gained much less attention. Finally, the systematic compilation of domain knowledge and re-specification was only achieved to some extent in some of the cases: the Model Factory, Lamp Remplace and Traffic Control, The basis of the others is formed by clearly initial texts with specifications that are far from complete and sometimes even monolithic, unwieldy and clumsy.

Observation IX. The bridgeheads have not become finished, structured, autonomous structures.

The work on railway safety is probably the only project that is gradually gaining some momentum.

The following can be said about the choice of the languages and the style of specification. The motivation to use the project languages is clear and valid: these are the languages that are locally developed and one must build experience with their practical application. Nevertheless, this effort does not necessarily correspond to the another target of the project: build domain knowledge. To put it more precisely: in domain D with problem P, one has to ask oneself: do I want to learn something about language L, or do I want to shed light on P in the context £>? In the latter case, one may have to reconsider the style of working, in particular, the choice for L. In retrospect,

I think I was not sufficiently attentive concerning this point, I was too easily distracted by what I had used before and by what was close at hand, A typical example here is Lamp Eemplace, The situation asked for a semiformal or even an informal inventory of the requirements of a decision support system for Lamp Eemplace, Instead, Willem van Wilsem and I hacked together a 36 page PSF specification, A waste of time. Luckily, it led to no accidents, but accidents are not difficult to imagine.

Observation X. Some specification exercises were irrationally 'motivated, the not-invented-here syndrome (no unprejudiced choice from the available options) and dogma (e.g. it has to be formal) prevailed over project goal directed, rational and pragmatic arguments.

Finally, an observation about the disciplines involved in the projects. The cases are small and quite focused. Despite this, quite a number of disciplines played a role: requirements specification, data type specification, process specification (dynamics), syntactical aspects of language design, semantical aspects of language design, verification, mathematical logic, operations research, methodology of software engineering, implementation techniques, documentation technique, deliverable maintenance, management and acquisition, There is not one institute in the Netherlands that I know of which has professionals in all these disciplines. It comes as no surprise that, in order to execute the cases, a number of parties were involved: UIJ, UvA, CWI (two thematic groups) and TUE, In other words:

Observation XI. The cases were executed by an academic consortium.

5 Hypotheses versus

observations & conclusions

The hypotheses of Section 4 of Chapter 1 of [92] are discussed in light of the observations and conclusions from the previous sections of this chapter. The following is a succinct discussion of weak and strong points of the project languages (5,1),

Hypothesis 1. The project languages are superior in comparison with informal specification means with respect to the qualities. This superiority will show by a remarkable positive effect on the production process of software. Moreover, the superiority of the formal texts will immediately be noticed by information technology practitioners.

Conclusion III says that the assessment of the qualities is largely inconclusive.

Comment 1, Apparently, this project did not lead to a clear view — either positive or negative. What can we learn from this? Suppose the qualities are indeed desirable properties. Then we can point to a number of possible sources for the inconclusiveness. First, the project was too scattered. Too many domains were entered. This makes it difficult to make a comparison.

Second, our style of application and the context for application is unsuitable for revealing differences — a pneumatic drill will not help a caveman enlarge his home because he has no electricity. Third, the qualities are only vaguely described. How could we possibly measure anything? Fourth, perhaps formal specification technique flourishes in niches and the project was too broad to be able to reveal these. Given the basic applicability (Conclusion I), this suggests that further work needs more structure.

Hypothesis 2. The project languages are omni-applicable, but will be most beneficial in the requirements engineering and early system decomposition phases of a forward engineering process.

This is not the ease. First, the project languages are not particularly suited for requirements engineering (see Observation J), Second, the main concepts and intuitions can be expected to be weak and unstable in the requirements specification phase and in early decomposition phases in forward engineering, particularly in new domains. Contrary to the hypothesis, Observation IV reads that the use of the project languages in these situations may well hinder instead of support the effort towards strong and stable concepts and intuitions. In other words, one can only produce neat, formal specifications when it is clear what the system is. Otherwise, formal specification technique is just a means to hack a model in. There is nothing wrong with that kind of use, as long as one acknowledges that formal specifications evolve, too. But there may be stronger means for such exercises.

Comment 2, I think that this conclusion, in a more general setting, is dependent on the current state of formal specification technique and the stability of the domain. With respect to the former, integrated facilities will make a difference with, for example, strong animation (graphics), simulation and automatic verification. With respect to the latter, in the often chaotic and booming world of mainstream software engineering, each customer in need of a system is a world unto himself that must be conquered. Some reasonably stable concepts, architectures and solutions emerge with a market shake-out. Only then might it may pay off to invest in theory formation, i. e. elicitation of rules, generalization and abstraction. Consequently, formalization and formal specification technique creeps into the engineering process. Please note that the bridgeheads which did lead to assignments stand out in stability: road traffic control and railways.

Hypothesis 3. The project languages are sufficiently expressive for requirements engineering, down to detailed system decomposition, i.e. no other language is needed.

This is clearly not true. The outcome with respect to this hypothesis is twofold. First, the project languages in general are not expressive enough to cover all levels of product development. They are thematic languages. The project languages fail especially in the area of requirements specification. In

general, languages of various styles are needed (Observation II), Second, the hypothesis suggests a smooth transition from one level (with a language and a specification) to the next level (with a language and a specification). This is problematic due to the lack of methodical support (Conclusion II) and their isolated position (Observation III),

Comment 3, This was to be expected. Both of the above points are exactly the motivation behind designing wide spectrum languages. However, wide spectrum languages are sometimes unwieldy because too many features are integrated. This makes it worthwhile to see what can be achieved with thematic languages, such as the project languages, and to gradually reach an understanding of the demands that engineering processes impose on specification languages. It is interesting to note that, problems with wide spectrum languages as well as the need to use more than one formalism in a project was one of the motivations behind the development of the ToolBus [64].

Hypothesis 4. The project languages can handle the various demands of a wide range of application areas.

This is true to some extent. According to Conclusion I, the project languages are basically applicable in many domains. However, they are confined to certain specific levels in the system decomposition. It is reasonable expect that, in some domains and at these levels, stronger means already exist, particularly in specialized domains. An example of this is the specification in PSF of the decision support system for Lamp Eemplace, Database systems already solve this problem.

Hypothesis 5. Once a formal specification of a system is available, it will arouse discussion with the industrial partner about the vast amount of easily accessible system knowledge represented in this way. This will lead to cooperation in further product development and transfer of the formal techniques to the industrial partner. The industrial side of the bridgehead will thus be formed.

This does not work in the way the hypothesis suggests. The establishment of confidence by showing considerable tenacity and verbal expression of domain knowledge is important. This establishment effort takes some years (ObservationVI). The specification is not the important medium. Even promising results such as prototypes do not sell themselves (Observation VIII), Nevertheless, it is clearly true that, from an academic point of view, formal specification work is a valuable asset for building domain knowledge.

Hypothesis 6. The project languages can easily be integrated into existing engineering practices of the industrial partners.

The work is inconclusive with respect to this hypothesis: the situation did not occur. Nevertheless, in light of Conclusion II on the methodical weakness, I expect that integration can be troublesome.

Hypothesis 7. The formal specifications will arouse academic interest. The specification will serve as a means to develop attractive themes. In this way, domain theory will develop. The academic side of the bridgehead will thus be formed.

Yes, theme building works (Observation V), But, the themes do not easily survive. They do not sell themselves in the academic context (Observation VIII), Furthermore, there is a risk that the theme can lose practical relevance because of domain changes or the industrial partners quitting (Observation VII), making academic work less attractive.

To summarize the whole argumentation above: the expectations with regards to the possibilities and properties of the project languages turned out to be too high; the project aimed too directly at the promulgation of the project languages; the bridgehead strategy did not work as expected.

In Section 7, I will discuss what seems to be the feasible way in which to continue applied research on the project languages and formal specification technique in general,

5.1 Weak and strong points of the project languages

ACP is a general theoretical format to study and develop theory over system principles and features in an operational style. Features can be added and their relation to others can be studied. For an example, please refer to Observation L on the other face of concurrency. An elaborate body of theory about system behaviour is being compiled in this way. See also the evaluation of the Protocold case, Section 7 of Chapter 3 of [92],

ACP and its derivatives, such as discrete time process algebra and BPA(>f) (I discuss PSF and /iCRL below), tend to work for detailed operational descriptions, including many complicated features such as time, broadcasting and concurrency, A typical application is the detailed description of some operational behaviour, e.g. in communication protocols and semantics of specification and programming languages (PSF, //CRL, Protocold and the EURIS studies [7,49]), Although, the relation between service specifications (i.e. abstract behavioural description) and detailed specification (implementation) is straightforward (abstraction and proof of equivalence), it appears that logical formalisms with modal operators are better suited for the specification of operational requirements at higher levels of product development. They allow more freedom and expressiveness for the formulation of service specifications. The data specification parts of PSF and /iCRL (derivatives of ASF) are reasonably suited for the specification of data types. However, the format is restricted: equational logic (with conditions in the case of PSF) and initial semantics. Once again, this forms a handicap for specifications at higher levels of abstraction, and forces one towards a detailed and operational style of

specification. Furthermore, the languages are somewhat intransigent and lack delicacy, ASF+SDF is better suited, at least when it comes to conciseness and readability; the flexibility in the syntactical appearance of functions is great, ASF+SDF is geared towards language engineering and proved to work very well for that purpose. There are many examples of this, including VPI and IDEAL.

PSF and /iCRL inherit key aspects mentioned above from ASF and ACP which render them more suited, in general, for decomposition specifications. /iCRL is stronger than PSF when it comes to verification and mathematical rigour. PSF is stronger than /iCRL when it comes to structuring specifications, expressive power and tooling (though that may be about to change [35]). The ToolBus finally proved to be a fine environment for prototyping and implementation, especially for integrating heterogeneous components.

Bidoit, Gaudel and Mauboussin mention the popular complaint that algebraic specification is not suited for specification in the large [16]. Bowen [20] also says, "This approach is theoretically attractive but problems can occur in scaling up specification for industrially sized examples". I do not agree. There have been many algebraic specification specifications produced of reasonable size. Of relevance here are Conclusion II about the methodical embedding, the need for multiple languages as seen in Observation II and the fact that it is a thematic style. Armed with this knowledge, one realizes that it is not the size but the level of decomposition and the type of system that determine whether algebraic means are suited.

Van Vliet argues in [90] that consistency and completeness for algebraic specifications is often not simple at all. I don't agree. Yes, it is difficult and, in general, undecidable. However, with informal techniques it not even possible to exactly specify an assertion on consistency and completeness, let alone prove something.

6 Formal specification technique in general

In this small section, I investigate to what extent the conclusions and observations from the previous sections hold true for other formal specification languages. A large comparative study could be devoted to this. Naturally, such a study is beyond the scope of this text. Relevant input for this type of comparative research is being gathered by Nico Plat in the context of the Formal Methods Europe initiative [44].

Regarding the Conclusion I: a quick scan through the literature leaves no doubt about the basic applicability of many specification languages. There is too much to list. The references to languages in Figure 6 (Chapter 1 of [92]) as well as [1], [70], [44], [43], and journals like Formal Methods in System Design can be used as entrances to many other case studies. Nevertheless, the need for multiple languages in one project, and their isolation and shyness (Observation II and III) is often noted and has motivated various projects.

For an example, please refer to [20] and the elaborate work solely directed at the combination and integration of Z, COFI [30] is a recent project aimed at the definition of a common framework for development and the use of algebraic languages.

The technical, syntactical and semantical features that may help to enhance the suitability of the project languages for integration in software engineering methods are suggested in observations A to J, Many languages already offer features suggested there. For example, the status of the specification (Observation B) PLUSS offers two types modules: draft and spec, GIST has an operator 'achieve', which is used to indicate that a specification is operationally incomplete. It can also register whether an invariant is a goal (something that can be compromised) or a requirement (something that cannot be compromised). The pre- and postcondition style of VDM-SL and Cold makes it easy to immediately denote conditions, assertions and assumptions (Observations A, E and F), An integrated approach to error and exception handling in an equational language with initial semantics is described in [59], CIP-L offers partial functions [79], PLUSS seems to offer the hidden features that, for example, PSF lacks: hiding imported material and the forget command (Observation G), CIP-L, Larch, PLUSS, Z, VDM-SL and many others are more expressive languages than the project languages for data types. These languages allow more or less full first order logic formulas. This mitigates the problem of formulation dictated by lack of expressiveness (Observation I), Furthermore, it allows application at a larger number of levels in the decomposition hierarchy than the project languages.

It may seem that the project languages — thematic or combined thematic languages — in many ways fall short when compared to other languages. This is only partially true. First, smaller languages are better suited to studying the practical application of theoretical results. Second, the definition of the project languages seems less prone to error than many other languages, despite their formal aura, VDM-SL, SDL and Cold are typical examples of languages for which the semantics are a popular subject of debate. Third, they have a shorter learning curve. Fourth, Dill & Rushby and Zave suggest that targeted languages and tools may be worthwhile [84], Although targeted is not the same as thematic, it also suggests that wide spectrum is not an imperative.

It appears to me that, although many books have been published on case studies (e.g. [57,31,85]), the methodical aspects of the application have not received much attention (Conclusion II), This is also noted by others, Partsch talks about the need for increased methodical attention in [79], Brov complains about the Larch Proof Assistant that it "does not provide any method nor even hints how to use such a tool in practical applications" [24], In an article in which they categorize strategies for the incorporation of formal specification technique Fraser et al. note that relatively little effort has been devoted to methodical and tool support [47], A clear sign of this is that many studies do not specify the amount of work invested or discuss related issues.

Instead, they concentrate on modelling (a quick random scan of some fifteen books containing case studies reveals this), I have to admit that my own cases belong to this majority: Table 4 was produced when writing this thesis on the basis of some sparse historical data. The Steam Boiler project [1], the Production Cell project [70] and the (web)database of Plat and of Bowen seem to be remarkable exceptions. Of course, some projects did deal with the methodical embedding of formal specification technique. The SPRINT Method [62] and RAISE [48] must be mentioned here. The Rigorous Review Technique is an example of a first step in an incremental approach to import formal specification in established development frameworks: respeeifieation of a design in a formal notation after an initial design is finished using conventional structured techniques [2], A recent initiative is TRADE by Wieringa [100],

To summarize, I state the following with a reasonable level of certainty.

Assertion I. The conclusions about basic applicability (I), weak methodical embedding and integration (11), difficult assessment of qualities (111) and the related observations (like II, III and IVJ, are also largely valid for many other formal specification languages — give and take local deviations.

I will make a short contrast of this with two surveys on formal methods: by Austin and Parkin [3] and by Craigen, Gerhart and Ralston [32],

Austin and Parkin conclude in a summary that the main reasons for the lack of uptake of formal specification techniques are "use of mathematics and perhaps lack of tools". The survey does not really contradict my work. First, the 'mathematics' was discussed as part of the discussion on communieability in Section 3, However, I do not put that much emphasis on it due to a lack of evidence. Second, the lack of tools is a factor that is rapidly changing. An example is ASF+SDF, which is in use at a number of commercial sites. Their survey is based on cases prior to 1993, Finally, although I placed emphasis on methodical embedding and assessment of qualities, such needs also clearly appear in the tables in the survey: in the group of seven major issues that start each table, methods-related issues such as cost assessment, comparison to other methods, integration with existing methods and metrics are considered important,

Craigen et al. put less emphasis on 'mathematics' as a problem, but recognize the need for notation suitable to people who have no expertise in formal methods or mathematical logic. The tenor of their conclusion is similar to mine: their first and second recommendation (of seven in total) for further research read respectively: "There is a clear need for improved integration of formal methods techniques with other software engineering practices", and "While numerous formal methods related tools exist, industry needs stable versions, not buggy research prototypes. These tools need to be an integral part of a broader software development tool suite",

From the above quotes it follows that Craigen et al. consider further development of tools important. However, they also observe that tools are "neither

necessary nor sufficient for the successful application of formal methods", This is similar to Austin and Parkin, who are not so sure that tooling is the big problem. This is similar to my point of view, I did not make a specific and explicit remark on tooling,

Austin and Parkin, and also Craigen et al. do not explicitly mention the assessment of the qualities I have discussed. They do make remarks on the need for assessment of cost effectiveness. Please note that, in the section on the qualities I described, the qualities are a refinement of productivity focused at specification texts. Therefore, problems with the assessment of cost effectiveness includes problems with the assessment of the qualities. Thus, our conclusions are similar in this respect, as well,

Craigen et al. observe that the use of formal specification technique in the twelve cases they perused can be characterized by: re-engineering, stabilizing system requirements, communication between and among various levels of stakeholders and as evidence of 'best practice'. Apparently, formal specification technique was not used as an aid in the conception of and brainstorming about new systems. This is conform Observation IV, which reads that formalization only seems to work when some intuition about the system and some clarity about the major notions has been achieved,

A final general remark is captured in the following observation.

Observation XII. An abundant amount of basic application work has been done in virtually all areas of application and levels of decomposition thereof.

Craigen et al. come to the same observation when they say that "formal methods are maturing", "formal methods are applied now to develop systems of significant scale and importance ... which cut across a number of modern application domains". Please refer to the impressive list of cases compiled at [44], The above also suggests that it is time to make a next step in the industrial application of formal specification technique, as suggested in Section 5 after the treatment of the hypotheses. In the next section, I will suggest some ideas to that end,

7 Discussion on future research

Please recall the motivation for the project. It was aimed at a generating better view on the applicability of the project languages, shedding some light on the mismatch between practice and academia with respect to formal specification technique and finding ways to bridge this gap. Expectations and approaches to these aims have been formulated in the form of hypotheses. These contain assertions about properties of the project languages and a project strategy, i.e. the bridgehead approach. The hypotheses have been answered in Section 5,

A lot was learned about the project languages and cooperation with industry, But, the mismatch and the gap are still largely present. Let us return

to the basic goal of academic work in software engineering: control over productivity and quality in the software engineering process. What about formal specification technique? This is conceived as a means to contribute to that basic goal. What is available is a set of basically usable means (Conclusion I), However, in the effort to obtain these means, the methodical embedding has been neglected (Conclusion II), Finally, assessment of the quality and effectiveness of means is difficult (Conclusion III), Furthermore, the above formulated motivation is sometimes forgotten: when formal specification technique is a target as such, one diverges from the software engineering tasks found in industry. Therefore, I suggest that it is time to reinforce the methodical effort, to revive the original motivation and consequently rethink the role of formal specification technique. Nevertheless, the tenet still reads:

Formal specification technique offers valuable means to enhance the quality

of software products, and the productivity of software engineering processes.

Of course, it is still valid to be dogmatic and to study certain specific characteristics of specific systems or languages. That is no problem as long this motivation is clearly understood from the start by all participants. Moreover, it is clear that much work must be done. For an example, please refer to the observations and conclusions in this thesis, or the fundamental goals, directions and recommendations for further research as formulated by Craigen, Gerhart and Ralston in [32], and by Clark and Wing in [29], However, projects that pursue further practical application of formal specification technique need another form, because we need the necessary feedback and empirical evidence as well. Below, ideas on this form are further developed.

Conclusion III and Comment 1 suggest that, in order to know what you are doing, a controlled project and a precise methodical target are prerequisites. Formal specification technique will gain from a revival of interest in: methodical support of languages, methodical embedding and integration of languages and quantitative & qualitative assessment of the development process, also with respect to the economical effectiveness of methods and techniques used. Important lessons can be learned from measured parallel development using different methods or techniques, A good example of this approach is discussed in [69].

An item for further study are rules that specify the circumstances in which a certain development deliverable should be produced, and that also specify the properties of this deliverable, A lot of work has been done here already, typically the work on process models. The design rules for data types as proposed in [14] are an example, albeit on a smaller scale. Next, one can specify guidelines that say which specification languages are best suited for which type of deliverable. It is important that the rules and guidelines reckon with the need for information transfer of one deliverable to its successor in development. Demands on these 'interfaces' are a part of the study. From these rules and guidelines, it may be possible to come to packages of languages

(at various levels of integration), I expect that loosely integrated packages are already sufficient for a competitive software development process, and also that the majority of languages is available. In other words, there is no urgent need for new languages. The possibilities of the currently available set of means from the realm of formal specification technique is sufficient to make an effective start.

In terms of technology marketing as championed by Moore [77], what is proposed on methodical embedding above can be seen as follows. For a long time, formal specification technique has been promoted as a general means in a market dominated by other paradigms, e.g. client/server architecture and object orientation. Now it has become clear that the scope of formal specification technique is not that general. Given the existing dominating forces, one should look for market niches. The methodical frameworks must be studied in order to determine and take advantage of the proper niches.

The renewed methodical focus is important, I expect, however, that it is at least as important to emphasize the focus on the themes and the problems of carefully selected domains, and to lessen the focus on the proof of the beneficial role of formal specification technique in these domains, A focus on the problems and questions of a domain will lead to a faster accumulation of domain knowledge and recognition of that by the industrial partners. After all, you will not lose time attempting to convince people of things that are not at issue from their point of view. Furthermore, by adopting a domain, one becomes less dependent on specific partners (Observation VII), Scientists involved should strive towards the enhancement of the productivity and quality of the software engineering process; the approach is characterized by consolidation and well-defined increments rather than overambitious targets. To make results really concrete, I think it is important that cooperation leads to products with a commercial value. To summarize this: in order to test the methodical results and to reach concrete, measurable results, well-defined development processes delivering real products in delineated domains must be set-up in close cooperation with industrial partners. The work on Cobol programs in the banking world, as reported on in [21], could well be seen as an endorsement of the feasibility of the 'domain approach' just proposed, Brov positions formal specification technique as a significant means to relate the "world of the application" (domain specific knowledge) and "the world of programming" [24],

Means from the realm of formal specification technique will often be used in the cooperations envisioned above. However, the choices are pragmatic, targeted and opportunistic, i.e. not dogmatic and not aimed at solving all problems in the world (Observation X), Together with the methodical embedding, the cooperations sketched above may lead to co-development of targeted products based on formal specification technique, conform the incubating phase as suggested by Jolly in [61],

Finally, management tasks, acquisition and lobbying must be recognized as separate tasks in projects (see Observations VIII and IX), Once the project is acquired, lobby and acquisition should continue. The team that works on applied research in formal specification technique will need considerable resources, a high level of organization and devotion. Maybe the project should be set-up by a consortium of academia (Observation XI),

This section finishes with remarks, ideas and observations from the literature that endorse the line of thought in the above, Craigen, Gerhart and Ralston recommend that "formal methods need to evolve with other computer science trends, such as visualization, multi-media, object-oriented programming and CASE", This corresponds well with the bridgehead approach as was followed, and the domain adoption as proposed above. In [71], Mandrioli stresses the need for what he refers to as a 'balanced' cooperation between academic and industrial partners and the need for an incremental approach. In the words of Glass, this balance can be phrased as a situation wherein there is "an absence of preaching and a great deal of listening" [84], Most other contributors to [84] follow the same line of thought, Hollowav and Butler put it this way: "More formal methods researchers must become knowledgeable about the problem domains relevant to industry, and develop examples, models, techniques and tools appropriate for those domains". In same article, Dill & Rushbv, Lutz and Zave state that in these domains, a pragmatic and targeted use of formal specification is appropriate, to the point of special languages and tools specifically targeted at the domain problems. This is also the approach followed by Odyssey Research Associates, a firm that has been active for years, with success, in the exploitation of formal specification technique [81],

With respect to the need for continuous lobby and acquisition, Hallowav and Butler remark that "industry rarely has the time and resources to keep up with and distill the vast number of ideas and tools that emerge from the research community" [84],

The proposed shift from 'language' to its embedding was already envisioned in [13], There is stated that when the basic value and benefit of a technique has been identified (my work falls in this category), the research and development effort should be directed to further facilitation and integration. Hall stresses the importance of an overall engineering approach in which formal specification technique plays a role [84], I expect that all ingredients are now available to do just that.

[1] J.-R. Abrial, E. Borger, and H. Langmaack, editors. Formal methods for industrial applications, volume 1165 of LNCS. Springer-Verlag, 1996.

[2] S. Aujla, T. Bryant, and L. Semmens. Applying formal methods within

structured development. IEEE journal on selected areas in communications, 12(2):258-264, 1994.

[3] S. Austin and G.I. Parkin. Formal methods: A survey. Technical report, National Physical Laboratory, Teddington, Middlesex, United Kingdom, 1993.

[4] J.C.M. Baeten and W.P. Weijland. Process algebra, volume 18 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.

[5] T. Basten, R. Bol, and M. Voorhoeve. Simulating and analyzing railway interlockings in ExSpect. Technical Report 94-37, Eindhoven University of Technology, Department of Mathematics and Computing Science, 1994.

[6] T. Basten, R. Bol, and M. Voorhoeve. Simulating and analyzing railway interlockings in ExSpect. IEEE Parallel & Distributed Technology, Systems & Applications, 3(3):50-62, 1995.

[7] J.A. Bergstra, W.J. Fokkink, W.M.I". Mennen, and S.F.M. van Vlijmen. Spoorweglogica via EURIS, volume 22 of Quaestiones infinitae. Universiteit Utrecht, Faculteit Wijsbegeerte, 1997. In Dutch.

[8] J.A. Bergstra, J. Heering, and P. Klint. Module algebra. Journal of the ACM, 37(2):335 372. 1990.

[9] J.A. Bergstra and P. Klint. The discrete time ToolBus. In M. Wirsing and M. Nivat, editors, Algebraic methodology and software technology AMAST'96, volume 1101 of INCS, pages 286-305. Springer-Verlag, 1996.

[10] J.A. Bergstra and P. Klint. The ToolBus coordination architecture. In P. Ciancarini and C. Hankin, editors, Coordination languages and Models COORDINATION '96, volume 1061 of INCS, pages 75-88. Springer-Verlag, 1996.

[11] J. A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Computation, 60(1/3):109-137, 1984.

[12] J.A. Bergstra and G.R. Renardel de Lavalette. De plaats van formele specificaties in de softwaretechnologie. Informatie, 31(6):477-556, 1989. In Dutch.

[13] J.A. Bergstra and G.R. Renardel de Lavalette. Onderzoek en ontwikkeling op het gebied van formele specificatietalen. Informatie, 32(l):73-83, 1990. In Dutch.

[14] J.A. Bergstra and M.P.A. Sellink. Sequential data algebra primitives. Technical Report P9602b, University of Amsterdam, Programming Research Group, 1996.

[15] J.A. Bergstra and J.V. Tucker. Equational specifications, complete term rewriting systems, and computable and semicomputable algebras. Journal of the ACM, 42(6):1194-1230, 1995.

[16] M. Bidoit, M.-C. Gaudel, and A. Mauboussin. How to make algebraic specifications more understandable: an experiment with the PLUSS specification language. Science of computer programming, 12(1):1—38, 1989.

[17] M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas, and D. Sannella, editors. Algebraic system, specification and development, volume 501 of LNCS. Springer-Ver lag, 1991.

[18] R.N. Bol, J.W.C. Koorn, L.H. Oei, and S.F.M. van Vlijmen. Syntax and static semantics of the interlocking design and application language. Technical Report P9422, University of Amsterdam, Programming Research Group, 1994.

[19] D. Bosscher, A.S. Klusener, and J.W.C. Koorn. A simulator for process algebra specifications with the ToolBus. University of Amsterdam & National Research Institute for Mathematics and Computer Science (CWI), unpublished.

[20] J. Bowen. Formal specification and documentation using Z, a case study approach. International Thompson Computer Press, 1996.

[21] M.G.J, van den Brand, A. van Deursen, P. Klint, A.S. Klusener, and E. van der Meulen. Industrial applications of ASF+SDF. In M. Wirsing and M. Nivat, editors, Algebraic methodology and software technology AMAST'96, volume 1101 of LNCS, pages 9-18. Springer-Verlag, 1996.

[22] M.G.J, van den Brand, M.P.A. Sellink, and C. Verhoef. Generation of components for software renovation factories from context-free grammars. In I.D. Baxter, A. Quilici, and C. Verhoef, editors, Proceedings of the fourth working conference on reverse engineering, pages 144-153, 1997.

[23] E. Brinksma. Tussen droom en daad: formele methoden en gereedschappen bij specificatie en implementatie van open svstemen. Informatie, 35(9):537-546, 1993.

[24] M. Brov. Experiences with software specification and verification using LP, the Larch Proof Assistant. Formal Methods in System Design, 8:221-272, 1996.

[25] J.J. Brunekreef. On modular algebraic protocol specification. PhD thesis, University of Amsterdam, 1995.

[26] J.J. Brunekreef and A. Ponse. An algebraic specification of a model factory, part 4. Technical Report P9316, University of Amsterdam, Programming Research Group, 1993.

[27] T.H.P.F. Bullens. Algebraic specification of a distributed traffic regulation system. Work placement report, 1994.

[28] T.H.P.F. Bullens. Implementing the intelligent network model on the ToolBus. Master's thesis, Utrecht University, Dept. of Philosophy, 1994.

[29] E.M. Clarke and J.M. Wing. Formal methods: state of the art and future directions. A CM Computing Surveys, 28(4):626-643, December 1996.

[30] CoFI: The common framework initiative for algebraic specification and development. http://www.brics.dk/Projects/CoFI.

[31] B. Cohen, W.T. Harwood, and M.I. Jackson. The specification of complex systems. Addison-Wesley, 1986.

[32] D. Craigen, S. Gerhart, and T. Ralston. An international survey of industrial applications of formal methods. Technical Report NISTGCR 93/626, U.S. Department of Commerce, Technology Administration, National Institute of Standards and Technology, Gaithersburg, MD 20899, U.S.A., 1993. Consists of two volumes. 1: Purpose, Approach, Analysis and Conclusions; and 2: Case Studies.

[33] D. Craigen and T. Ralston. Formal methods technology transfer: impediments and innovation. In Monterey workshop on software evolution, pages 74-84. U.S. Naval Postgraduate School, Monterey, California, 1994.

[34] D. van Dalen. Logic and structure. Springer-Verlag, 1989.

[35] D. Dams and J.F. Groote. Specification and implementation of components of a piCRL toolbox. Technical Report 152, Utrecht University, Logic Group Preprint Series of the Department of Philosophy, 1995.

[36] A. van Delft and L. Stolk. A simulation of a CIM factory using a parallel object oriented language. In A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors, Proceedings of ACP'95, pages 229-244. Eindhoven University of Technology, 1995. Report 95-14.

[37] A. van Deursen, J. Heering, and P. Klint, editors. Language prototyping, an algebraic approach, volume 5 of AMAST Series in Computing. World Scientific, 1996.

[38] F. van Dijk, W.J. Fokkink, G.P. Kolk, P. van de Ven, and S.F.M. van Vlijmen. EURIS: a specification method for distributed interlockings (extended abstract). In Proceedings of SAFECOMP '98, LNCS. SpringerVerlag, 1998. To appear.

[39] F.A. van der Duvn Schouten, A.S. Klusener, S.F.M. van Vlijmen, and S.L.E. Vos de Wael. A decision support system for the maintenance of lights of traffic regulation systems. Technical Report 159, Utrecht University, Logic Group Preprint Series of the Department of Philosophy, 1996. In Dutch.

[40] F.A. van der Duvn Schouten, A.S. Klusener, S.F.M. van Vlijmen, and S.L.E. Vos de Wael. Een beslissingsondersteunend svsteem voor lampremplace. Technical report, Utrecht University, Logic Group Preprint Series of the Department of Philosophy, 1996. In Dutch, confidential.

[41] Frank van der Duvn Schouten, Bas van Vlijmen, and Stefan Vos de Wael. Replacement policies for traffic control systems. IMA Journal of Mathematics Applied in Business and Industry, 9(4), 1998.

[42] A.S. Fisher. CASE, using software development tools. John Wiley & Sons, 1991.

[43] Formal Methods site by Jonathan Bowen. http://www.comlab.ox.ac.uk/archive/formal-methods.html.

[44] Formal Methods Europe. http://www.cs.tcd.ie/FME/PROJECTS/Master.html.

[45] W.J. Fokkink. Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd. Technical Report 135, Utrecht University, Logic Group Preprint Series of the Department of Philosophy, 1995.

[46] W.J. Fokkink. Safety criteria for the vital processor interlocking at Hoorn-Kersenboogerd. In Proceedings of the 5th Conference on Computers in Railways, COMPRAIL'96, Part P Railway Systems and Management, pages 101-110, Berlin, 1996. Computational Mechanics Publications. Extended version is available as: technical report 135, Logic Group Preprint Series of the Department of Philosophy, Utrecht University.

[47] M.D. Eraser, K. Kumar, and V.K. Vaishnavi. Strategies for incorporating formal specifications in software development. Communications of the ACM, 37(10):74-85, 1994.

[48] C. George, A.E. Haxthausen, S. Hughes, R. Milne, S. Prehn, and J. Storbank Pedersen. The RAISE development method. Prentice-Hall, 1995.

[49] J.F. Groote, M. Hollenberg, and S.F.M. van Vlijmen. Laris 1.0: LAnguage for Railway Interlocking Specification, 1997. Publication in preparation.

[50] J.F. Groote, J.W.C. Koorn, and S.F.M. van Vlijmen. The safety guaranteeing system at station Hoorn-Kersenboogerd. Technical Report 121, Utrecht University, Logic Group Preprint Series of the Department of Philosophy, 1994.

[51] J.F. Groote, J.W.C. Koorn, and S.F.M. van Vlijmen. Formele analyse van het veiligheidssvsteem op het station van Hoorn-Kersenboogerd. Informatie, pages 397-404, June 1995. In Dutch.

[52] J.F. Groote, J.W.C. Koorn, and S.F.M. van Vlijmen. The safety guaranteeing system at station Hoorn-Kersenboogerd. In Proceedings of the Tenth Annual Conference on Computer Assurance, Compass'95, pages 57-68. IEEE, 1995. IEEE catalog number: 95CH35802.

[53] J.F. Groote and A. Ponse. Proof theory for psCRL: a language for processes with data. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors, Proceedings of the International Workshop on Semantics of Specification Languages, pages 232-251. Springer-Verlag, 1994. WICS.

[54] J.F. Groote and A. Ponse. Syntax and semantics of piCRL. In A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors, Algebra of communicating processes, Utrecht 1994; pages 26-62. Springer-Verlag, 1995. WICS.

[55] J.F. Groote and S.F.M. van Vlijmen. A modal logic for piCRL. In A. Ponse, M. de Rijke, and Y. Venema, editors, Modal logic and process algebra, a bisimulation perspective, volume 53 of CSLI lecture notes, pages 131-150, Stanford, California, 1995. CSLI.

[56] A. Hall. Is software engineering. In C. Sladge, editor, Proceedings of the SEI conference, volume 640 of LNCS. Springer-Verlag, 1992.

[57] I. Hayes, editor. Specification case studies. Prentice-Hall International, 1993.

[58] J.A. Hillebrand and A. Ponse. An algebraic specification of a model factory, part 2. Technical Report P9214, University of Amsterdam, Programming Research Group, 1992.

[59] I. van Horebeek and J. Levi. Algebraic specifications in software engineering. Springer-Verlag, 1989.

[60] W.L. Johnson. Deriving specifications from requirements. In 10th International Conference of Software Engineering, pages 428-438. IEEE Computer Society Press, 1988.

[61] V.K. Jolly. Commercializing new technologies: getting from, minds to markets. Harvard Business School Press, 1997.

[62] H.B.M. Jonkers. An overview of the SPRINT method. In J.P.C. Woodcock and P.G. Larsen, editors, FME'93: Industrial strength formal methods, volume 670 of LNCS, pages 403-427. Springer-Verlag, 1993.

[63] P. Klint. A meta-environment for generating programming environments. ACM Transactions on Software Engineering and Methodology, 2(2):176-201, 1993.

[64] P. Klint, 1998. Personal communication.

[65] A.S. Klusener, S.F.M. van Vlijmen, and A. Schrijver. Compact dvnamisch busstation. Technical Report CS-N9601, National Research Institute for Mathematics and Computer Science (CWI), 1996. In Dutch.

[66] A.S. Klusener, S.F.M. van Vlijmen, and A. van Waveren. Service independent building blocks-I; concepts, examples and formal specifications. Technical Report P9310, University of Amsterdam, Programming Research Group, 1993. Also available as CWI report CS-R9326.

[67] D. Knuth. Literate programming, volume 27 of CSLI lecture notes. CSLI, Stanford, California, 1991.

[68] M.J. Koens and L.H. Oei. A real time piCRL specification of a system for traffic regulation at signalized intersections. In A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors, Algebra of communicating processes, Utrecht 1994, pages 252268. Springer-Verlag, 1995. WICS.

[69] P.G. Larsen, J. Fitzgerald, and T. Brookes. Applying formal specification in industry. IEEE software, pages 48-56, May 1996.

[70] C. Lewerentz and T. Lindner, editors. Formal development of reactive system,s: case study production cell, volume 891 of LNCS. Springer-Verlag, 1995.

[71] D. Mandrioli. Applying research results in the industrial environment: the case of the TRIO specification language. In M. Wirsing and M. Nivat, editors, Algebraic methodology and software technology AMAST'96, volume 1101 of LNCS, pages 33-42. Springer-Verlag, 1996.

[72] S. Mauw and G.J. Veltink. An introduction to PSFd. In J. Diaz and F. Orejas, editors, Proc. International Joint Conference on Theory and Practice of Software Development TAPSOFT '89, volume 352 of LNCS, pages 272-285. Springer-Verlag, 1989.

[73] S. Mauw and G.J. Veltink. A process specification formalism. Fundamenta Informaticae, XIIL85-139, 1990.

[74] S. Mauw and G.J. Veltink, editors. Algebraic specification of communication protocols, volume 36 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1993.

[75] S. Mauw, M. van Wijk, and T. Winter. A formal semantics of synchronous Interworkings. In O. Faergemand and A. Sarma, editors, SDL'93: Using Objects, Proceedings of the Sixth SDL Forum, pages 167-178, Darmstadt, 1993. Amsterdam, North-Holland.

[76] J. Mertens. Verifying the safety guaranteeing system at railway station Heerhugowaard. Master's thesis, Utrecht University, Department of Philosophy, August 1996.

[77] G.A. Moore. Inside the tornado. Capstone Publishing Ltd., Oxford, UK., 1998.

[78] L.H. Oei. Pruning the search tree of interlocking design and application language operational semantics. Technical Report P9418, University of Amsterdam, Programming Research Group, 1994.

[79] H. Partsch. Algebraic specification: a step towards future software engineering. In J.A. Bergstra and M. Wirsing, editors, Algebraic methods: theory, tools and applications, volume 394 of LNCS, pages 7-30. Springer-Verlag, 1989.

[80] S.L. Pfleeger and L. Hatton. Investigating the influence of formal methods. Computer, 30(2):33-43, 1997.

[81] R. Platek, 1994. Personal communication.

[82] A. Ponse and J.A. Verschuren. An algebraic specification of a model factory, part 3. Technical Report P9303, University of Amsterdam, Programming Research Group, 1993.

[83] P.H. Rodenburg. Module algebra for initial algebra semantics. Technical Report P9407, University of Amsterdam, Programming Research Group, 1994.

[84] H. Saiedian, J.P. Bowen, R.W. Butler, D.L. Dill, R.L. Glass, D. Gries, A. Hall, M.G. Hinchev, C.M. Hollowav, D. Jackson, C.B. Jones, M.J. Lutz, D.L. Parnas, J. Rushbv, J. Wing, and P. Zave. An invitation to formal methods. Computer, 29(4):16-30, 1996.

[85] K.J. Turner, editor. Proceedings of the first international conference on formal description techniques, FORTE 88. North-Holland, 1988.

[86] G.J. Veltink. The PSF toolkit. Computer Networks and ISDN Systems, 25:875-898, 1993. Elsevier Science Publishers.

[87] G.J. Veltink. Tools for PSF. PhD thesis, University of Amsterdam, 1995.

[88] D. Verhoef and E. van der Winden. Tool vision. ID Research B.V., 1995.

[89] E. Visser. Syntax definition for language prototyping. PhD thesis, University of Amsterdam, 1997.

[90] J.C. van Vliet. Software engineering. H.E. Stenfert Kroese B.V., 1988.

[91] S.F.M. van Vlijmen. Algebraic Specification in Action. PhD thesis, Universiteit Utrecht, dept. of Philosophy, 1998. In Quaestiones infinitae, vol. 26.

[92] S.F.M. van Vlijmen. Algebraic Specification in Action, volume 21 of Electronic Notes in Theoretical Computer Science (EN"l"('S). Elsevier Science, 1999. http://www.elsevier. ill/locate/entcs/volume21.html.

[93] S.F.M. van Vlijmen, P.N. Vriend, and A. van Waveren. Control and data transfer in the distributed editor of the ASF+SDF Meta-environment. Technical Report P9415, University of Amsterdam, Programming Research Group, 1994.

[94] S.F.M. van Vlijmen and J.J. van Wamel. A semantic approach to Protocold using process algebra. Technical Report P9317, University of Amsterdam, Programming Research Group, 1993.

[95] S.F.M. van Vlijmen and A. van Waveren. An algebraic specification of a model factory. Technical Report P9209, University of Amsterdam, Programming Research Group, 1992.

[96] S.F.M. van Vlijmen and A. van Waveren. Algebraic specification of a system for traffic regulation at signalized intersections. Technical Report P9313, University of Amsterdam, Programming Research Group, 1993.

[97] S.F.M. van Vlijmen and R.J. Wieringa. Using the tools in TRADE, I: A decision support system for traffic light maintenance. Technical Report 181, Utrecht University, Logic Group Preprint Series of the Department of Philosophy, 1998.

[98] J.J. van Wamel. A library for PSF. Technical Report P9301, University of Amsterdam, Programming Research Group, 1993.

[99] R.J. Wieringa. Requirements engineering, frameworks for understanding. John Wiley & Sons Ltd., 1996.

[100] R.J. Wieringa. A toolkit for requirements and design engineering (TRADE). Technical report, Free University, Faculty of Mathematics and Computer Science, Amsterdam, 1997. In preparation.

[101] W. van Wijk. Een simulatie van een verkeersregelsvsteem. Master's thesis, Hogeschool Rotterdam en Omstreken, 1994.

Association "Open Science"

Paper: Discussion/Conclusion

This article is about the last section that wraps up a paper – it’s often called the “Discussion” in electrical engineering and “Conclusion” in computer science. We will use “Discussion” to refer to both of these, but the article applies to both.

Criteria for Success

A strong Discussion section:

recaps the main conclusion of the paper in one or two sentences.
relates the paper’s results to the big questions posed in the Introduction.
describes how (and why) this work agrees or disagrees with other similar work.
analyzes how the limitations of this study leave the big questions unanswered.
puts the work in context – how does it relate to the rest of the literature?
looks forward at how extensions of this paper’s results will be useful for answering the big questions.

Structure Diagram

Below is one possible structure for a Discussion section.

Identify Your Purpose

The Discussion explains how your work addresses the big questions you posed in your Introduction. The Introduction and Discussion are natural partners. The Introduction tells the reader what question you are working on and your specific approach (e.g. why you did a particular experiment to investigate it, what techniques you used, etc.); the Discussion tells the reader how the results of that approach contribute to answering the bigger question. That is, the Discussion explains how your results address the main questions you set out to answer in the Introduction.

Analyze Your Audience

Different kinds of readers will expect different things from your Discussion. Readers who are not experts in your field might skip your Results and read your Discussion for a high-level description of your results and their importance. They might also be interested to know what you think the future of your field is. Readers who are more familiar with your field will generally understand your results, but they will be curious about how you interpreted confusing, conflicting, or complicated results.

As you write your Discussion, decide who will find each paragraph interesting and what you want them to take away from it. Successful Discussions can simultaneously provide the specific, nuanced information that experts want to read and the broader, more general statements that non-experts can appreciate.

The balance between expert and non-expert readers will depend on the journal or conference you submit to. High-profile, general-readership conferences and journals will have more non-expert readers, while more technical, field-specific conferences and journals can have almost exclusively expert readers.

Recap paper objectives and motivation

In the Introduction, you laid out the objectives of your work and motivated why those objectives solve an important problem. To recap, the Discussion might include a short summary of why the problem this paper addresses is impactful and how solving it with your methodology advances the field.

Set your paper apart from previous work

Weak Discussions begin with a summary of the results or a repetition of the main points of the Introduction. Strong Discussions immediately carve out a place for themselves in the large universe of papers by saying what makes this one interesting or special. For example, the Discussion might describe how the methodology in the paper is unique and useful or how the questions the paper addresses are important and have not yet been directly addressed by other papers. One way to do this is to start the Discussion with one or two sentences that relate the results to the existing literature.

Relate your results to existing results

In the Introduction, you probably helped motivate your study by citing previous results in your field. Now that you’ve laid out your results, you should tell whether your results agree or disagree with prior work and why. You might have extended previous work, showed how apparently conflicting results are actually harmonious, or exposed a contradiction that currently has no explanation. Another strategy is to bring up additional related work in the conclusion and explain how your results might fit into their broader context.

Tell how your study’s limitations leave open the big questions

Every study is finite—you did some things and not others, and you used methods that can explain some phenomena but not others. What bigger questions does your study bring up, and how might those get resolved? Do you just need to do more of the same kind of work? Have you shown that current methods are inadequate to answer the big question, and what more is needed to answer it?

Every paper is a contribution to a larger scientific conversation. To explain this contribution, many Discussions end by placing the paper in an expected future of research in that field. Depending on how much there is to say about future work, this forward-looking description of future work might be a statement or even its own subsection. The discussion of future work might relate the new experiments or techniques in the paper to other problems in the field.

Content adapted by the MIT Electrical Engineering and Computer Science Communication Lab from an article originally created by the MIT Biological Engineering Communication Lab .

Resources and Annotated Examples

Annotated example 1.

Liu et al Nature 2013 760 KB

Annotated Example 2

Schardl et al, ACM SIGPLAN 2017 46 KB

IMAGES

(PDF) Finding Reasons and Conclusion in a Basic Computer Science Course
Writing a Conclusion for a Research: Master an A+ Paper
Computer Science Thesis Topics
Part VII Conclusion: Computer Science
️ Example of a conclusion paragraph for a research paper. Conclusion
⚡ Sample research papers in computer science. Essays on Computer

VIDEO

Computer Science Research at Ashoka
G10 Q4-Week 1: Research Paper and Its Parts #research #qualitativeresearch #quantitativeresearch
12TH COMPUTER SCIENCE QUARTERLY EXAM-2023 OFFICIAL ORIGINAL QUESTIONPAPER II 12TH QUARTERLYEXAM-2023
Step-by-step approach to starting and completing a good research paper
Research Methods: Extracting the Essentials of a Computer Science Research Paper
Top 10 Best Computer Science Research Topics

COMMENTS

What Does “conclusion” Mean in Science?
A conclusion is the final process of the basic scientific method by which scientists reveal whether the hypothesis was proven correct, according to certified math and science teacher Patricia McNerney.
What Is the Conclusion in a Science Project?
The conclusion in a science project summarizes the results of the experiment and either contradicts or supports the original hypothesis. It is a simple and straightforward answer to the question posed by the experiment. This section is clea...
How Do You Write a Research Synopsis?
To write a research synopsis, also called a research abstract, summarize the research paper without copying sentences exactly. It should provide a brief summary of the content of the paper, including a short introduction, body and conclusio...
Conclusion
Abstract of research paper on Computer and information sciences, author of scientific article — S.F.M. van Vlijmen. Abstract This document is one of the
How to Write a Conclusion for a Research Paper: Effective Tips and
Your research paper's conclusion must be concise and straightforward. Avoid dwelling on descriptions and interpretations that should have been
Paper: Discussion/Conclusion : EECS Communication Lab
This article is about the last section that wraps up a paper – it's often called the “Discussion” in electrical engineering and “Conclusion” in computer science
(PDF) How to End an Introduction in a Computer Science Article? A
the concluding sentence of the Computer Science Introductions are given here. ... computer science research article introductions [16, 24] . In
Writing a (Computer Science) Paper
• 2nd model ~ study/medical kind of papers. – Background & Purpose. – Methods. – Results. – Conclusions. 14. Page 15. 15. Background & Gab. What we did ~
The Science of Computer Science: Closing Statement
" Denning/A's conclusion was: "The old lament that computing dealt solely with
How to write a compelling introduction and conclusion for ...
Here are some tips for writing a compelling introduction and conclusion for your computer science essay: Introduction: 1. Start with a hook: Begin your
3 Stages of Computer Science Research Paper Writing: 3 Tricks to
So, be ready to work hard not only on programming languages, scientific computing or software engineering, but also in academic writing. Many research papers
A move-step analysis of the concluding chapters in computer
This paper describes how computer science doctoral writers construct the closing chapters of their PhD theses. The data are drawn from the chapters playing
Part VII Conclusion: Computer Science
As we go to press, the most recent edition is called the. The second document is
A Guide to Writing a Successful Paper
The conclusion answers the readers' question: “So what?” It