The Origins and the Development of the ASM Method for High Level System Design and Analysis

Abstract: The research belonging to the Abstract State Machines approach to system design and analysis is surveyed and documented in an annotated ASM bibliography. The survey covers the period from 1984, when the idea for the concept of ASMs (under the name dynamic or evolving algebras or structures) appears for the first time in a foundational context, to the year 2001 where a mathematically well-founded, practical system development method based upon the notion of ASMs is in place and ready to be industrially deployed. Some lessons for the future of ASMs are drawn.

Key Words: System design, specification methods, system analysis, abstract state machines, models of computation.

Category: D.1, D.2, D.3, C.1, C.3, I.6, H.1, G.0, F.1.1, F.1.2, F.3.1, F.3.2, F.4.2, F.4.3

1 Introduction

The ASM method for high-level design and analysis of computing systems naturally grew out of the foundational concern which led to the discovery of the notion of ASMs, although it took some time for the concept to sink in. Indeed as often happens with ideas which change the way we look at things, its "real"ization |through becoming the basis for an intellectual, machine supported instrument for practical system design and analysis|encountered significant resistance in the scientific community. In this paper we survey the already rich ASM literature and the salient steps of the development of the ASM method out of its origins. This reflexion, upon where we came from and upon the way we went, helps to bring into focus some risks and challenges for the future of the ASM approach to industrial system development. We discuss these lessons for the future in the concluding section.

From 1984 to today one can distinguish four phases which we are going to survey in the following sections:

• the start in 1984 with the idea of an improved Church-Turing thesis for a "general kind of abstract computational device, called dynamic structures" [175],
• the recognition of the practical potential of the abstract machine concept for building and analysing reliable ground models and their controllable

refinements to executable code, an insight which came through the experience gained at the beginning of the 90'ies by extensive modeling of the dynamic semantics of various programming languages and their implementation [49],

• the broadband experimental practicability test for the ASM concept in complex real-life applications, an effort which shaped the ASM design and analysis method through numerous modeling and verification projects for real-life architectures, virtual machines, protocols, and control software, carried out in the years 1993-1995 [53] preceding the final definition of ASMs in [181],
• the systematic integration of the ASM method into established soft-ware development environments which created the practical ASM approach to high-level system design and analysis as one sees it nowadays, ready to be deployed in industrial settings [59], and the completion in 2000/01 of the first part of the original foundational goal, namely by the proof of the sequential ASM thesis from three basic postulates [183] and of its extension to synchronous parallel algorithms [40].

For the references, with few exceptions we stick to list only work which is directly related to ASMs. We revise and complete the annotated bibliography which appeared in [52], was updated in [85] and since then is maintained by Huggins on the ASM website¹. This paper is based upon and elaborates the historical accounts [55, 57, 60]. It is not an introduction to ASMs, see [181, 59] and for a textbook introduction [291, Ch.2].

2 The Idea of the New Thesis

It was an epistemological concern which led Gurevich to the idea of Abstract State Machines, namely the goal to sharpen the Church-Turing thesis by including the consideration of resource bounds. The problem is stated for the first time in 1984 in a technical report [174], where ASMs appear in embryo under the name of dynamic structures, later also called evolving structures or algebras. A year later the program is formulated in a note to the American Mathematical Society [175] from where we quote the central part:

First, we adapt Turing's thesis to the case when only devices with bounded resources are considered. Second, we de ne a more general kind of abstract computational device, called dynamic structures, and put forward the following new thesis: Every computational device can be simulated

¹ http://www.eecs.umich.edu/gasm

by an appropriate dynamic structure|of appropriately the same size| in real time; a uniform family of computational devices can be uniformly simulated by an appropriate family of dynamic structures in real time.In particular, every sequential computational device can be simulated by an appropriate sequential dynamic structure.

In 1988 a more detailed exposition of this primarily complexity theoretic program appears [177], but again without any concrete definition of the abstract machine concept. Apparently at that time there was still some hesitation on "different classes of dynamic structures" which "may be defined by imposing syntactical restrictions on transition rules, by allowing or forbidding the evolution of the signature (the language) of the current configuration, by allowing or forbidding the creation of new universes (sorts, types) and the elimination of old ones, and so on" (op.cit., pg.413). Into this period falls also the formulation of the Kolmogorov-Uspenskii thesis [221] as stating that "every computation, performing only one restricted local action at a time, can be viewed as the computation of an appropriate Kolmogorov-Uspenskii machine" [178], a subclass of what became known as Schönhage's storage modification machines [283] which later could be characterized as a class of unary sequential ASMs [129].

In a series of lectures on Semantics of Programming Languages, delivered to the computer science PhD program in Pisa in the Spring of 1987, Gurevich explained the concept of ASMs by examples, namely Turing machines, stack machines, and some Pascal programs. Börger learnt ASMs from these lectures and suggested to add the course material to [176] (see sections 10 and 11)². There the proposal appears to use "dynamic structures" for an operational semantics of imperative programming languages, a project tried out for the core of Modula-2 in Morris' PhD thesis [239]. During the winter of 1988/89 ASMs were tried out to define the semantics of Prolog by an execution oriented yet abstract model, which was intended to become complete and precise, but nevertheless of manageable size and re ecting the logical content of Prolog programs in a transparent way, to be useful to programmers [44, 45, 46]. The goal was achieved by introducing the stepwise refinement method into modeling with ASMs, exploiting the possibilities for abstraction that are inherent in the ASM concept. Stepwise refinements allowed to separate orthogonal language features by modules of rule sets (horizontal refinement) and to deal with them at different levels of detail (vertical refinement), supported by an appropriate classification of functions (which was later refined [53, 59]).

²The stack machine and the Turing machine ASMs went into sections 4 and 6 of [179].

3 Recognizing the Practical Relevance of ASMs

Through his sabbatical work at IBM Germany in 1989/1990 Börger realized that his ASM model for Prolog solved some central problems the ISO Prolog stan- dardization committee had faced for years [69], in particular the database update view problem [72, 95] and the semantical problems related to Prolog's solution-collecting predicates [99]. In fact a version of this model became the standard definition of the dynamic semantics of Prolog [211], after many unsuccessful attempts documented in the literature to provide such a definition using traditional approaches (see the detailed discussion in section 4 of [44]). Through the work with the software engineers from IBM, Quintus, Bim, Interface, Siemens, which at the time were developing commercial implementations of Prolog, the usefulness of the ASM concept became apparent for supporting changing designs in an industrial standardization and development process. The exibility was recognized which is gained by using ASMs for modeling and for prototypical (mental or machine supported) simulations. This showed up through the ease with which ASMs allowed the practitioners to perform the following three of their daily duties:

• to rigorously model and document design decisions, building ground models³ in a faithful and objectively checkable manner. This means to turn descriptions expressed in application domain (typically natural language) terms into precise abstract definitions, which the software engineers were comfortable to manipulate as a semantically well-founded form of pseudo-code over abstract data,
• to adapt abstract models to changing requirements, and to refine them in successive steps - in a controllable and well documentable way - to their implementation, thus providing practical forms of refinement for linking ground models by hierarchies of intermediate models (modules) to executable code,
• to turn such precise abstract pseudo-code models into prototypical executable versions which can be used for simulations prior to coding of the system under development.

Unfolding the potential of the concept of ASMs for such a method of modeling-for-change, at the desired level of abstraction, to be used together with an appropriately chosen mathematical verification and experimental validation technique, was the result of extensive experimentation during the years 1990{1992. It was focussed on the following three issues:

³The originally chosen term primary model [49, Section 3] was replaced later by ground model [53].

1. adaptations and extensions of models via horizontal refinements, realized by re ning the basic ASM model for Prolog to some of the major extensions of the language and their implementations, to be precise the following seven ones:
• Colmerauer's Prolog III, obtained by adding to the unifiability check of the Prolog model a solvability test for general constraints [104],
• IBM's Protos-L, developed and implemented on the Protos Abstract Machine at IBM Germany, obtained from the Prolog model by adding to it type constraints and a solvability predicate [26, 27, 28],
• the functional-logical language Babel and its implementation on the Narrowing Machine [87], obtained by adding to the backtracking rules of the Prolog model rules for the reduction of functional expressions to normal form,
• Lloyd's and Hill's logic programming language Gödel, obtained by abstracting in the Prolog model from the deterministic and sequential execution strategy of ISO Prolog [93],
• B. Müller's object-oriented Prolog [243, 244], obtained by enriching the four ASM rules for the user­defined core of Prolog [47] with rules for object creation and deletion, data encapsulation, inheritance, messages, polymorphism, and dynamic binding,
• Sauer's adaption of the Prolog model to an ASM defining the semantics of the domain-specific language HERA, tailored for programming scheduling algorithms for business processes on the basis of given heuristics [273, Ch.3.3],
• the main parallel extensions of Prolog (see below),
2. 2. stepwise detailing of models by vertical refinements, realized for the WAM implementation of Prolog by de ning a chain of 12 proven to be correct refinement steps which link the high-level Prolog model (in fact its streamlined version in [101]) to its implementation by Warren Abstract Machine code [96, 98, 100]. It turned out that the models and the proofs could be reused and extended to derive the correctness also for the following four implementations:
3. { the implementation of a high-level CLP(R) model on the Constrained Logic Arithmetical Machine, developed at IBM Yorktown Heights [102], { the implementation of a high-level Protos-L model on the Protos Ab- stract Machine [27, 28] 4 ,

{ the parallel execution of Prolog on distributed memory [13], see also the related later work [249], { the implementation of scoping of procedure definitions in a sublanguage of Lambda-Prolog where implications are allowed in the goals [227], 3. making abstract models executable for their experimental validation, realized during the academic year 1989/90 in Kappel's Diplom thesis at the University of Dortmund [219, 220], and a year later at Quintus [112], allowing to simulate the ASM Prolog models defined in [44, 45]. The method of successive refinements of ASMs was applied in [184] to provide a transparent ASM model for the dynamic semantics of C. An earlier version of this work had inspired a similar project for Cobol which was started in [301] (though not continued). Before that, in Blakley's PhD thesis [33] an unstruc- tured ASM model for a subset of Smalltalk had been defined. Inspired by [239], ASMs are used in [166] to provide a succinct operational description of typical object-oriented features like object creation, overriding, dynamic binding, inheritance in the context of data models. In [284] an ASM rule is added to define cooperative message handling, by describing the run-time search of the most specific cooperation contract in the inheritance hierarchy which implements a cooperative message, i.e. a message which involves several objects on the basis of cooperation contracts. Later the modeling of object-oriented programming language features is taken up once more in Ann Arbor, this time using the refinement method to extend the ASM model for C to one for C++ [303]. In 1991 Gurevich writes for his column on Logic in Computer Science in the Bulletin of the EATCS the so-called ASM tutorial [179], which is based on lecture notes from his Fall 1990 course on Principles of Programming Languages at the University of Michigan, containing most notably the first definition of sequential ASMs. The same year a textbook introduction to ASMs is written [48] coming with an illustration by machines which operate on standard data structures and by the tree based core Prolog machine [47], drawn from notes of lectures on Semantics of Programming Languages in a summer school held in 1989 in Cortona/Italy which triggered the first European PhD project on ASMs [264]. Gurevich completed the tutorial definition in the so-called Lipari guide [181], lecture notes of a course delivered in 1993 at the Lipari/Sicily summer school on specification and Validation Methods for Programming Languages and Systems [51]. The definition essentially remained stable since then 5 , in fact it constitutes the basis for the proof established five years later for the sequential version of the 4 Beierle [25] turned this construction into a general implementation scheme for CLP(X) over an unspecified constraint domain X, by designing a generic extension WAM(X) of the Warren Abstract Machine and a corresponding generic compilation scheme of CLP(X) programs to WAM(X) code.

ASM thesis from three fundamental postulates [183]. As has been observed by Blass [34, Section 2], the computationally natural subclass of sequential ASMs is natural also from a logical point of view, corresponding to the class of quanti er free interpretations in logic. The tutorial and the Lipari guide incorporate the experience which had been gained through the early applications of ASMs, those described above and those reported in the contributions to the first international ASM workshop which was organized as part of the 13th World Computer Congress in Hamburg in 1994 [255], see below. The major addition of the Lipari guide to the tutorial concerns the notion of distributed ASM runs. In [190] an ASM model had been developed for the parallelism of Occam. It was presented by Gurevich in May 1990 in another series of lectures in Pisa, which inspired the concrete theme for Riccobene's PhD thesis [264] to refine the ASM model for Prolog by the different forms of parallelism encountered in Parlog, Concurrent Prolog, Guarded Horn Clauses, and Pandora [91, 92, 265]. Later another instance of refinement and parallelization of Prolog to a semi-ring based constraint system appears [32], replacing the Call and Select Rules of [44] by a Reduction Rule which activates a child process simultaneously for each alternative of the current process. The notion of parallelism in these models was generalized in [162] where ASM models appear for the Chemical Abstract Machine and the -calculus. Eventually in 1995, the Lipari guide definition of distributed ASM runs supersedes these more restricted definitions of concurrency for ASMs. 4 Testing the Practicability of ASMs

Once the practical potential of the ASM notion had been understood, a natural next step was to test its practical impact by trying out ASMs for the modeling and a rigorous mathematical and experimental analysis of a variety of complex real-life computing devices, looking for relevant problems beyond those of the semantics of programming languages. In the Fall of 1992 Börger defined this program and started it with his students by systematically extending the application of ASMs to the specification and analysis of virtual machines, processor architectures, protocols, embedded control software and requirements capture. As part of this effort the 1993 Lipari Summer School on specification and Validation Methods [51] was organized wich triggered the fundamental Lipari Guide [181] and a series of papers on applications of ASMs [102, 303, 83, 204, 189] 6 . The endeavor attracted many researchers and resulted in the elaboration of a 5 The initially present construct to shrink domains, which was motivated by con- cerns about resource bounds, was abandoned because it belongs to garbage collection rather than to high-level specification. Some technical variation was later introduced concerning the treatment of non-determinism and of inconsistent update sets. For a more substantial recent extension see [196].

full-fledged system design and anlysis method built upon the notion of ASMs, pragmatically con rming the ASM thesis and the choices Gurevich made for the definition of ASMs in the Lipari guide. 4.1 Architecture Design and Virtual Machines

For computer architectures, the work on the program started during the win- ter term 1992/93 with a reverse engineering study, commissioned by a group of physicists in Pisa and Rome for the massively parallel APE100 architecture, a rather successful dedicated machine which had been developed for oating point intensive numerical simulations in Lattice Gauge Theory [19, 20]. As part of the work for Del Castillo's Tesi di Laurea, a programmer's view ground model has been defined in [71] and refined in [70] to a provably correct decomposition of the control unit processor zCPU, a VLSI implemented microprocessor with pipelining and VLIW parallelism, built from formally speci ed basic architectural components. The intermediate models, obtained by stepwise refinement, correspond to views of the architecture provided by different languages used within the APE100 compilation chain, a crucial part of the software environment of the machine. A companion Tesi di Laurea [88] had the goal to isolate the underlying pipelining scheme and to prove its correctness via stepwise refined models. Hennessy and Patterson's RISC machine DLX was chosen as reference architecture to deal with the standard pipelining methods which handle structural hazards, data hazards, and control hazards respectively. Starting from the one-instruction-at-a-time view of the processor, each hazard is dealt with in one dedicated refinement step which concentrates on the corresponding machine property. This ASM based architecture verification method was taken up by other research projects which are mentioned below.

For virtual machines, the program to extend the WAM work [100] beyond issues concerning the implementation of programming languages started with modeling the well known Oak National Laboratory public domain software sys- tem PVM [151], a general purpose environment for heterogeneous distributed computing. The virtual machine appears there logically as a single distributed- memory computer, "created" by PVM out of a dynamic heterogeneous set of physically interconnected and concurrently operating machines, namely host computers which can be dynamically added to or deleted from the virtual machine and may belong to a variety of architectures (including serial, parallel, and vector computers). Glasser suggested to try out the notion of distributed ASMs for modeling PVM. In [75, 76] a ground model for the Parallel Virtual Machine is defined at the C-interface level, where it appears as a distributed ASM with a

6 A companion Lipari Summer School on Architecture Design and Validation Methods followed in 1997 [61]. Another one is forthcoming in 2002 on Software Engineering, with ASM based courses held by Riccobene, Gurevich, Börger.

characteristic event handling mechanism and message-passing interface (reflecting the uniform access the PVM agents ("daemons") have to daemons on other host machines, whether multicast or point-to-point between single tasks).

The cooperation on modeling the PVM triggered the project to provide a ground model for the at the time new IEEE standard VHDL'93 [208] of the hardware design language VHDL. The models defined in [79, 80] come as a dis- tributed ASM and cover the entire language with the new features of the 1993 standard, in particular the complete signal behavior and the time model, includ- ing pulse rejection limits and the various wait and signal assignment statements involved in the subtle issues related to postponed processes. Later these ASM models have been used in W. Muller's PhD thesis at the University of Pader- born [245] for de ning the semantics of a pictorial extension PHDL of VHDL'93, by a group of Toshiba engineers for an extension to analog VHDL and Verilog [271, 272, 268, 269, 270], and recently for an adaptation to SystemC [247] and to SpecC [246].

Conversations with Langmaack since 1991 on the relations between the ASM based method used for proving the correctness of Prolog-to-Wam compilation [100] and the European ProCoS project on provably correct systems [230], which aimed in particular at a correctness proof for executing compiled Occam pro- grams [248] on the Transputer architecture [170], have led to the Transputer verification ASM case study. In [73] the Transputer instruction set architecture has been modeled by a hierarchy of stepwise refined ASMs to support the cor- rectness and completeness proof for the general compilation scheme of Occam programs to Transputer code proposed in [209, 210]. As basis for the seman- tics of truly concurrent and non-deterministic Occam programs an appropriate ground model ASM has been used, which was defined in [74]. It leads from the programmer level by various proven to be correct refinement steps to the starting point of the hierarchy of Transputer models, namely a machine which appears as an abstract processor running a high and a low priority queue of Occam processes. This ASM based method for a mathematical verification of real-life compilation schemes with respect to a rigorous semantics of source and target languages has been taken up again in the Veri x project discussed below, based upon the recognition in the ProCoS project that to establish the correctness of (modulo hardware correctness) reliable initial compilers, in addition to verify- ing the compiling function also the verification of a compiler implementation is needed. 4.2 Protocols

Using ASMs for modeling and verifying protocols has been started in three pa- pers which were published in [51]. The work in [83] is an answer to one of the at the time frequent public challenges of ASMs: Abraham and Magidor at a

Dagstuhl seminar in June 1993 expressed doubt that the atomic character of function updates in ASM transitions would prevent these machines from nat- urally reflecting complex combinations of low level durative actions. The discussion in the seminar focussed on the concrete example of Lamport's mutual exclusion protocol known as bakery algorithm [228, 229] for which Abraham had presented a new proof method, relying on a distinction between a lower and a higher view of the algorithm [2, 3]. In [83] three ASMs are built. The first one serves as a ground model to faithfully reflect Lamport's protocol. By abstracting from the low-level read and write operations of the ground model, a high-level model with atomic actions (non-overlapping reads and writes) is defined and then { proven to have the desired correctness and liveness properties (under four natural assumptions on the abstract functions that were used), { proven to be correctly refined by the ground model (proving that the as- sumptions made for the abstract model hold for the implementation). In the third ASM, the state of the abstract machine is refined by replacing atomic actions with durative ones, allowing overlapping of reads and writes to shared registers. It is proved that this refined notion of state satis es the corre- sponding assumptions made for the machine with atomic actions. The resulting correctness and liveness proofs for the bakery algorithm considerably shorten numerous other proofs in the literature. The arguments are expressed using a mapping of ASM moves to moments of continuous and linear real-time, but they can and have been rephrased in the more general terms of partial orders [195] which characterize the notion of distributed ASM runs in the Lipari guide. A further analysis of the role of timing constraints on distributed ASM runs for proving the correctness of refinements of distributed asynchronous algorithms with continuous time appears in [118]. In [204] the technique of successive refinements of ASMs is applied to show how one can provide for a real-world protocol a faithful readable specification together with an understandable correctness proof. The Kermit le-transfer pro- tocol chosen as object of the study had been presented by Knuth in his foreward to the Kermit book [120] by expressing the hope that many readers of this book will be challenged to nd high-level concepts and invariant relations by which various versions of the Kermit protocol can be proved correct in a mathematical sense. In fact Huggins deals with a complete version of Kermit, showing how this pro- tocol combines the underlying alternating bit protocol and its sliding windows extensions, thus di ering from numerous earlier verification studies in the liter- ature which had focussed on these two simple protocols in isolation. Later two

other ASM formalizations of the alternating bit protocol alone appear, one in [235, Ch.5] as an illustration of a modularization and communication concept implemented on top of ASMs, the other one in [173] to illustrate the application of algebraic-categorical composition schemes to ASMs.

In [189] a processor group membership protocol is modeled as distributed ASM, a typical protocol of the kind used to achieve fault tolerance for distributed computing services. The underlying assumptions for the well-functioning of the protocol are made explicit, such as the reliability of the message passing mechanism, lower bounds for processor recovery, upper bounds for message exchange time, etc. These assumptions are then proved to imply the correctness of the protocol, namely that despite of delays in message passing and server failures, the protocol achieves a global agreement about the set of all correctly functioning processors in a synchronous system.

This debut of ASMs for protocol verification triggered numerous other ASM projects in the area which are discussed below. 4.3 Why use ASMs for Hw/Sw Engineering?

In the first half of the 90'ies, the concept of ASMs encountered considerable scepticism and not seldom strong opposition in the scienti c community, even in Europe. Interestingly enough the criticism came from two directions, on the one side from researchers whose longstanding trust in purely declarative logico- algebraic methods made them view ASMs as nothing else than yet another form of an old fashioned low-level operational method, on the other side from researchers who claimed earlier fathership for the notion in a variety of forms. Both objections contain a grain of truth. They motivated the attempt, made in 1995 [53] and again in 1998 [59], to better understand the relation between ASMs and established formal methods and to formulate the stringent scientific reasons why after decades of intensive research in the area, an apparently new concept is proposed as basis for a practical high level system design and analysis method. The articles explain that although a logician discovered the concept of ASMs, as an outsider driven by a foundational concern 7 , the notion triggered the development of a method which allows one to really "complete the longstanding structural programming endeavour (see [121]) by lifting it from particular machine or programming notation to truly abstract programming on arbitrary structures" [59, Section 3.1]. As a matter of fact the notion is made up of two ingredients which had been there already for a long time but with no Columbus to bring them together for further exploration of the New World, namely Dijkstra's basic concept of abstract machines [134] and the fundamental idea to use Tarski structures as most general notion of abstract states, an idea which pervaded the area of abstract data types and algebraic specifications [254, 146]:

ASM = Abstract State + Abstract Machine.

5 Making ASMs fitt for their Industrial Deployment

The positive experience gained through the multitude and diversity of successful ASM-based modeling and verification projects convinced Börger of the potential of ASMs for industrial system development and brought him to the decision, in the Spring of 1994, to apply ASMs to down-to-earth software engineering problems and to pave the way for their industrial deployment. At the time it was hard to find support for projects directed towards this goal, the effort was judged even by some leading peers to be a waste of time. Nevertheless it attracted more and more researchers and eventually led to an industrially viable, theoretically well-founded system development method built around the concept of ASM, an approach which supports practical system design and analysis by application- tailored high-level modeling that is seamlessly linked to executable code, going through mathematically verifiable, experimentally validatable, and objectively documentable refinement steps.

The program was articulated through the following three major themes sur- veyed below: { investigation of practically relevant case studies and system development problems, to identify the strengths and weaknesses of ASMs for software development, and to compare ASMs with established formal methods, { application of ASMs in challenging industrial software engineering projects, { integration of tools for simulation, verification, documentation, and mainte- nance of ASMs during the software development process. 5.1 Practical Case Studies

In the Spring of 1994 the preparation of a research competition among methods for semantics and specification was started with the declared goal to "contribute to a realistic comparison, from the point of view of practicality for applica- tions under industrial constraints, of the major techniques which are currently available for formally supported specification, design, and verification of large programs and complex systems" [7, pg.1]. This developed into the Steam Boiler Dagstuhl Seminar [5]|by the name of the industrial case study the participants were asked to solve|and into the Steam Boiler Case Study Book [6] which came out of a subsequent international call for participation. Although only a quarter of the numerous solutions came up with a validatable executable model, to

7 In an e-mail of September 13, 1996, addressed to the ASM community at ea@ira.uka.de, Gurevich stresses the epistemological point that "the core of evolving algebras is an observation (or discovery if you will) and not invention. That is what the EA thesis is all about."

provide a complete ASM solution turned out to be a relatively easy task. In [29] first a ground model ASM is defined|a rigorous form of the given problem description which is phrased in such a way that it can be checked by the domain expert to be faithful to the intended requirements. Then the ground model is stepwise refined to C++ code, each intermediate model reflecting some design decision 8 . Proofs for some of the required system properties are reported, and during a demo to the seminar, Durdanovic showed his C++ program to successfully control the simulator [233] Lötzbeyr had built at FZI in Karlsruhe for an experimental evaluation of the problem solutions.

Mearelli's Tesi di Laurea, started at the beginning of 1995, had the goal to extend the positive experience made with the development of the steam boiler control software by a test of the integratability of the ASM method into the various phases of the software development cycle. As experimental guide an ASM ground model for the at the time freshly published Production Cell Case Study [231] was developed and stepwise refined to C++ code (see [89, 237]), with particular attention to the following two features: { the modularity of the specification and the code and their structural similar- ity (to support code inspection), together with their complete documentation as support for inexpensive changes and easy maintenance, { the applicability of standard verification and validation methods to prove the desired properties stated in the requirements. In fact in [89] all the required correctness, safety, performance, and liveness conditions are proved by mathematical argument|typically for the high-level model under appropriate assumptions, proving these assumptions to hold at the refined level. The C++ code produced by implementing the final refined ASM model [237], taking care that the specification can be traced through the structure of the code, has been validated by extensive experimentation with the simulator built at the FZI in Karlsruhe. It has also been submitted for an in- spection process to another software engineering Dagstuhl Seminar, organized in 1997 and focused on "Practical Methods for Code Documentation and Inspec- tion" [86]. To test the integratability of mechanical verification methods into the software development with ASMs, the Production Cell models were used for model checking experiments [306, 256] and for theorem proving with PVS [147]. As one of the first test examples for his code generator from ASM specifications (see below), Schmid has used the Production Cell ASM for generating eÆcient C++ code whose structure allows one to trace the specification to support the reliability of code inspection [278].

8 One can view it also the other way round as lifting the C++ code to a more ab- stract level with simultaneous updates, access to historical function values, etc., a methodological view which was held by Durdanovic and has been further elaborated in [124].

In 1999, through another software engineering Dagstuhl seminar, it has been tried to bring together once more researchers from academia and practitioners from the software industry to evaluate the contribution of so-called formal and informal methods for solving practical system engineering problems. The seminar was focused on problems encountered in industrial software development processes to capture, document, and validate requirements in a principled manner [84]. This seminar, too, was centered around a practical case study which triggered some complete solutions published in [81]. The ASM solution of this Light Control Case Study [94] showed that building and simulating ASM ground models is an efficient method to capture, validate and document requirements for a precise reason: it allows one to document in a traceable way the desired mix of rigorous, explicit ("formal") elements of description and of others intended to remain vague, implicit ("informal"). Such a mix is needed to bridge the gap between the views of the application domain expert and of the system designer, persons who speak different languages but nevertheless have to understand each other to be able to agree on the definite characteristics of the system to be developed. This observation has led to Cavarra's PhD project [116] where an attempt is made to link ASMs to so-called semi-formal specification techniques as they are used in industrial practice. The formal versus semi-formal issue is an instance of the more general need for an encompassing framework to combine heterogeneous specification elements, which is discussed in [155, 9, 125]. The 1999 Dagstuhl Seminar [84] brought out this requirements engineering aspect of the systematic separation of different concerns which has been advocated in [53, Sect.4] as a characteristic and major distinctive feature of the ASM method compared to other approaches to system design (see also [50, 180]). It was pointed out again in [60, Sect.1] that such a separation of orthogonal system features, and of different methods to model and analyze them, is necessary for a successful combination of multiple ways to construct and relate different system views| - by modeling, simulating, and verifying the system with different degrees of precision. Indeed it is one of the reasons for the success of the ASM method that the mathematical "openness" of the basic ASM concept allows fine-tuning this separation-for-integration strategy - a classical divide-et-impera approach - to the needs of the system to be developed or investigated.

Also other case studies which had been presented during this period as challenges to the scientific community have been elaborated using ASMs. See the ASM solution [205] to the Broy-Lamport specification problem [113] which had been formulated in 1994 for the Dagstuhl seminar on reactive systems. Another example is the real-time based ASM modeling and verification in [186, 21, 22] of the Railroad Crossing Problem to which Heitmeyer and Mandrioli's book [202] was dedicated.

5.2 Industrial Pilot Projects and Further Applications

ASMs at Siemens/Munich. For his sabbatical year 1995/96 Börger chose the goal to find out whether the above described applications of ASMs to require- ments capture and to design and analysis of control software scale to the needs of industrial design environments. This developed into a fruitful cooperation during the years 1996-1999 with Pappinghaus at Siemens in Munich, largely focussed on design methods for railway-related software [65]. It led to a rather successful application of ASMs in a middle-sized industrial software development project (FALKO, May 1998{March 1999, reported in [90]). The salient methodological outcome of this cooperation was the creation of a prototypical ASM based industrial development environment which supports a seamless ow from the definition of an ASM ground model to compilable (in the specific case C++) code and its maintenance.

Obviously, to make this project succeed, appropriate ASM tools had to be created and used extensively. In the Spring of 1995 Del Castillo had started his PhD work, located at the university of Paderborn, to build a tool environment for the specification and simulation of ASMs. The FALKO ground model was formulated in the ASM-SL language Del Castillo meanwhile had defined for the ASM Workbench [123], so that in the FALKO design phase early versions of this machine could be used for extensive testing of the high-level FALKO models, prior to coding. At the end of the design phase, as part of his PhD project started in the summer of 1998 at Siemens Corporate Research in Munich, Schmid developed a compiler from ASM-SL to C++ [278]|it generated the program which since March 1999 is in daily, failure-free use by the Vienna Subway Operator for the validation of subway operational services. For documentation and maintenance purposes Schmid developed a literate programming tool allowing to keep a single collection of consistent HTML documents from which the ASM-SL code can be extracted as input to the ASM Workbench or to the compiler, but also in pretty-printed form for the human reader.

In the third part of his PhD work [279, Ch.2], Schmid successfully applied this tool-supported structured ASM modeling and refinement technique also in a large ASIC design and verification project at Siemens München. This includes the definition of a notion of ASM components which was used for the behavioral specification of digital hardware circuits, and of the development of a compiler from ASM components to VHDL.

CO-Monitoring System. Another early industrial application of tool sup- ported ASMs, namely for an automated fire detection system adopted by three major German coal mines, is reported in [114]. Kappel's Prolog based interpreter for sequential ASMs [219] has been extended for this project to support the parallel execution of independent modules, representing distributed processes which are synchronized via stream based communication. The extension comes with a visualization mechanism for run data.

DFG Projects Deduktion/Verifix. In 1994 Börger suggested to the German Research Council project "Deduktion" to apply mechanical proof verification for proving properties of ASM models of real-life programs [280]. In particular, some of the refinement steps in the above mentioned WAM correctness proof have been mechanically verified using Isabelle [262], whereas using KIV the entire proof has been elaborated for a mechanical check, using not only all the 12 refinement steps from [100], but adding one more intermediate model to make the proof feasible for the machine [276, 274]. In [275] a scheme is ex- tracted from that work for proving the correctness of ASM refinements using generalized forward simulation. This use of ASMs for proving the correctness of compilation schemes has been further developed in a part of the Veri x project [164] of the German Research Council where instead of schemes for compila- tion into virtual machine code the correctness of concrete compilers compiling into real-life machine languages is investigated. To mention only a few examples from the subpart of the Veri x project where ASMs are used, which appeared in [149, 318, 136, 150, 200, 201, 167, 199]: a ground model ASM for the DEC- Alpha processor family has been extracted from the manufacturer's handbook; compiler back-ends have been built based on realistic intermediate languages to prove their correctness, using generic PVS theories developed in [135] to define refinement relations between ASMs; ASMs have been used to describe compilers which verify the correctness of the code they generate, etc. For the specification of source languages also Montages (see below) has been used, adopting however attribute grammars to formulate static semantics features. In [238] appropriate ASM models are defined to prove the correctness for the static link technique.

Montages at ETH Zürich. A related research effort has been undertaken at ETH Zürich, triggered by Gurevich's ASM-lectures delivered there in the Spring of 1995. It was driven by the Montages project [224, 11], geared to support, by an appropriate combination of graphical and textual elements, the simultaneous specification of the static and dynamic semantics of programming languages, exploiting the syntax-driven modularity which is typical for sequential languages where instructions are executed one after the other and one per step. The method is illustrated by a complete definition of syntax, static and dynamic semantics of Oberon in [225] and of C in [207]. In [10] a development tool (Gem-Mex) for creating Montages is presented which has been applied to provide an executable semantics for Mosses' Action Notation [9]. A successful application of Montages to the design and specification of a domain-specific language for a Swiss bank is reported in [226].

SDL-2000 Standard. Another remarkable industrial exploitation of ASMs comes with the abstract operational ASM definition of the new industrial standard for the design language SDL, widely used for over 20 years to develop distributed systems.

In November 2000, the international standardization body ITU-T for telecommunications accepted the ASM model as official definition of the 2000 standard of the language. The project of modeling the intricate static and dynamic semantics of the distributed real-time features of SDL as executable ASMs, in the context of rich data and hierarchical control structures together with advanced object-oriented and exception handling features, was started in [160], proposed to the SDL Forum in [156], and led through three years of intensive work of a body of experts [157, 158, 140, 261] to the complete standard definition [212]. It covers the static and the dynamic part of the semantics, currently an SDL-to-ASM compiler and further tool support of the ASM model for the standard are in development [141].

ASM Analysis of Java and the JVM. The project to apply ASMs to a systematic investigation of Java and its implementation on the Java Virtual Machine was born from a debate, in March 1997 in Dagstuhl, on How to use Abstract State Machines in Software Engineering [56]. The modeling experiments during the first two years [106, 107, 108, 109, 110] were geared to establish through this concrete real-life case study the respective merits of functional, axiomatic, and operational abstract state-based specification features. They were followed by two more years of mathematical and experimental analysis, stream-lining and structuring the ASM models of Java and of the Java Virtual Machine, and adding correctness and completeness proofs for a standard compiler of Java programs to JVM code and for the security critical bytecode veri er component of the JVM [291]. The technique of structuring the ASM models into language layers and machine components [62] is based upon the composition concepts which were developed in [103]. It led to a natural refinement of the high-level Java/JVM models to AsmGofer executable models [277] which can be used for code testing purposes. In a recent evaluation of about 40 Java/JVM research projects worldwide it is stated that "the Jbook (i.e. [291]) ... gives the most comprehensive and consistent formal account of the combination of Java and the JVM, to date"[198].

Architecture Projects. Mention has been made already above of the in- dustrial extensions of the ASM models for VHDL [79, 80] to analog VHDL and Verilog [271, 272, 268, 269, 270], to PHDL [245], to SystemC [247] and to SpecC [246], as well as of Schmid's compiler from ASM components to VHDL [279, Ch.2]. The ASM modeling method for instruction set architectures developed in the APE100 project [70] has been enhanced in [126, 127] to instrument models to collect data for evaluating design alternatives.

In [153, 292] some steps were taken to mechanically verify the pipelining correctness proof using the KIV system and PVS, but unfortunately without covering the complete hierarchy of four models in [88], so that an omission of a hazard case in the last refinement step remained undetected until Hinrichsen found it during his work on generating pipelined systems from sequential processor specifications [203].

The design and verification method of [88] has been applied in [206] to an advanced commercial RISC processor with a simpler pipelining scheme. It is reused in [297] to illustrate an approach to automatically transform register transfer descriptions of microprocessors into XASM-executable ASMs [8], thus allowing to generate a simulator for a processor architecture from its netlist description or from a graphical description of its data-path. In the same spirit, in [298] an ASM model is developed for a VLIW digital signal processor of the Texas Instruments TMS3200 C6200 family. These papers are part of an architecture and compiler co-generation project, led by Teich at the University of Paderborn, where ASMs and their execution in XASM [8] are systematically applied for hierarchical modeling of application specific instruction set processors [296].

Further ASM Applications. Since 1994 numerous advanced applications of ASMs appeared for protocol verification and in other fields of computer science, namely formal grammars, databases, electronic commerce, software architecture, finite model theory, complexity theory. In [217, 241, 242] distributed ASMs are used to model various formal and natural language grammars. In [193] the database undo-redo recovery algorithm is modeled at several levels of abstraction, showing the ground model to be correct and proving the correctness of each of the four refinement steps, leading to a model incorporating cache and log management. In [24] ASMs are used to describe the semantics of a domaispecific language, tailored to program the control for event driven database applications. In [144] an ASM based prototype system is described for specifying electronic commerce applications. The contribution of ASMs here is to provide a rigorous transparent way for describing the state changes involved in electronic commerce negotiations, concerning the traded products, the negotiators, their orders, the laws accepted as basis for the particular negotiation, etc. This paper and its companion paper [1] triggered the recent study of decision problems for restricted classes of relational ASM-transducers [288]. In [218] ASMs are used to specify a name management model. In [14] ASMs are used to define the seman- tics of patterns and for correctness proofs for workarounds. In [148, 17, 171, 152] ASMs are exploited for dealing with testing issues, taking up a suggestion made in [59, page 36] and [60, page 6]. In [295] an interesting ASM-based approach to software architecture design is proposed, allowing to specify software systems by appropriately connecting components which are characterized abstractly in terms of the services they export or import. In [282, 235] interacting ASMs are defined. In [117] the task and data parallelism of the programming language P3L is analysed on the basis of an ASM model. In [250] the theme of modeling PVM [75, 76] is taken up again using ASMs to propose a definition for the semantics of grid systems.

The early ASM specifications and verifications of protocols have been contin- ued in [30] where the Kerberos Authentication System is modeld by a hierarchy of proven to be correct stepwise refined ASMs, disclosing the minimum assumptions to guarantee the correctness of the system as well as its security weaknesses. In [31] the Needham-Schroeder protocol is analyzed to illustrate a general ASM framework for a practical analysis of cryptographic protocols. Stroetmann defined a ground model ASM for the constrained shortest path problem and proved it to be correct from a small number of natural axioms [294]. He then refined the ground model in a proven to be correct way down to (but excluding) the level of an efficient proprietary Siemens implementation of the algorithm in C++. During his research stay in Pisa in 1997/98, Durand investigated the cache coherence protocol in the Stanford FLASH multiprocessor system. In [137] a high-level ASM specification and a correctness proof are provided which detected some in- coherent and incomplete features in the given protocol description. This model has been used in [307] as case study for a real-life application of model checking to ASMs, using the SMV model checker. In [139] a two-level ASM specification of a distributed termination detection algorithm is given together with an equivalence proof between the two machines. In [187] it is illustrated by two ASMs for an algorithm proposed by Lamport that the notion of equivalence of algorithms depends on the level of abstraction at which the algorithm is viewed.

Foundational Progress. It became characteristic for ASM workshops and collections of ASM papers [255, 51, 57, 58, 161, 188, 78, 77, 35] to contain both theoretical and practical contributions. In fact in addition to the theoretical pa- pers mentioned already above, there have been important contributions of ASMs also in complexity and finite model theory, although the surprising observation expressed in [319] is still true, namely that the theoretical potential of ASMs has been recognized and explored to a less extent than their practical applications. In [36] ASMs are used as computation model which can reflect the practical experience that for real-life computations, constant factors matter. Based upon this model, linear-time hierarchy theorems for random access machines and ASMs are proven. In particular it is shown that there exists a sequential ASM U and a constant c such that, under honest time counting, U simulates every other sequential ASM in lock-step with log factor c.

In [168] finite model theory is extended to metafinite models, covering the mixture of finite and potentially infinite features as they appear typically in practical applications in the states of an ASM. [38] is an investigation into the notion of the reserve set of an (untyped) ASM, exploring the ideas of adding structure within the reserve and the non-determinism of importing new elements.

In [41, 39, 42] a polynomial time version of ASMs is defined and investigated which captures the portion of the complexity class PTIME where parallel algorithms (with arbitrary finite structures as inputs) are not allowed arbitrary choice.

In [43] this choiceless polynomial-time variant of ASMs is explored as a query language for relational databases. In [169, 287] a restriction is defined to capture log-space computable functions on structures. The ASM choice con- struct (choose x : F (x)) motivated also [37] where extensions of first-order logic with the choice construct are studied.

[286, 289] deal with decision problems for restricted classes of ASMs.

Recent industrial ASM applications. Since the Fall of 1998 when Gure- vich joined Microsoft Research, various applications of ASMs within Microsoft have been reported. The first one [197] is an ASM specification of the Windows Card Runtime Environment with a verification of certain safety properties. During 1999/2000, a command-line debugger of a stack-based runtime environment has been reverse engineered from the given 30k lines of C++ code, using three successive abstraction steps: one to extract the ground model which defines the same core functionality as the debugger, one to reflect the compile time structure of the underlying architecture (of modules of classes containing functions containing code) together with a restricted view of the run time structure, and eventually a control state ASM focussing on the interaction between the com- mand issuing user and the reacting runtime environment. The conclusion reads [15, pg.367]: "The study provides evidence for ASMs being a suitable tool for building executable models of software systems on various abstraction levels, with precise refinement relationships connecting the models." In [159] a distributed real-time constrained ASM has been developed to specify the Universal Plug and Play (UPnP) architecture for peer-to-peer network connectivity of intelligent devices. A refined model is derived which is executable in AsmL (see below) and can be used to inspect ASM runs at the required level of detail for conformance testing.

In [308] an ongoing industrial project in Australia is mentioned where ASMs are used to specify and model check a railway interlocking system. 5.3 Tool Integration

Already at the times of the very first industrial application of ASMs in the context of the ISO standardization of Prolog, the issue of how to turn the abstract specifications into executable ones for high-level simulations prior to coding has been recognized as crucial. Since then it has been resolved in various ways, as we are going to survey in this section. The progress made over the years in using ASMs in industrial projects for building models of software systems on various abstraction levels made it clear however that it is not enough to build simulators. They must also be linked to standard verification, testing, refinement, versioning and maintenance methods and tools as used in current development environments.

ASM Interpreters. The first interpreter for sequential ASMs was developed in 1989/90, in Kappel's Diplom thesis at the University of Dortmund [219]. During the same time at Quintus a special interpreter for Prolog ASMs was built [112] to execute the ASM models proposed in 1990 and accepted in 1995 for the ISO standardization [69]. In 1995 an elegant 9-line Prolog interpreter for sequential ASMs appeared [23]. The same year in Oslo [131] a functional ASM interpreter is implemented. As Huggins reports (see [60, footnote 3]), at the University of Michigan an interpreter for sequential ASMs was developed (in C) by Harrison and Huggins from 1991-1994. In this context Huggins also implemented an automated partial evaluator for sequential ASMs [185] which was extended in [133]. From 1994-1996 the Michigan interpreter was upgraded by Mani to distributed ASMs, and in 1996 Gurevich invites the ASM community to "Please use the new Michigan interpreter and tell us how do you like it and what features you would like to have." 9

In 1995, Glässer, Del Castillo and Durdanovic propose an abstract ASM machine (at the time called EAM for abstract evolving algebra machine). It is defined by stepwise refinement as a platform for implementing ASM tools and led to the design of a virtual machine architecture as a basis for a sequential implementation of the EAM [124]. This was the start for two PhD projects, both located at the University of Paderborn and with the goal to develop a practically useful tool support for ASMs. The first result to come out was Del Castillo's ASM Workbench [122, 123] which has been used in a methodologically interesting way in the FALKO project at Siemens [90]. The high-level ASMs of the to be developed railway process software were tested for some scenarios provided by the customers by running the scenarios on the Workbench, where upon calling an abstract function for some argument, the requested value is taken from its instance in the particular scenario (read from a le which describes the given use case). [138] continues the ideas developed in [124] by building an ASM Virtual Architecture as basis for a comprehensive ASM tool environment which comes up to industrial eÆciency standards.

In [260] the MAX tool supporting the generation of language-specific software from formal specifications is presented which uses functional algebraic attribution techniques for the static semantics and ASMs for the dynamic semantics. The development tool Gem-Mex presented in [10] for creating Montages has been extended by Anlau to the system XASM [8] for producing efficiently executable and easily reusable ASMs and coming with an XASM-compiler, a runtime system and a graphical debugging and animation interface. It contains a mechanism for structuring ASMs based on components which can be compiled separately and thus be put into a library for later reuse. Technically this is achieved by enhancing a static module concept, where submachines can be used as ASM rules or as external functions, by access/update constructs which provide information on permissions to read/write locations of submachines.

9 e-mail to ea@ira.uka.de of September 13, 1996.

An application of this component concept is presented in [12]. (For a different set of modularity concepts, geared to define and refine I/O-behavior of programs according to their abstract syntax, see [165].) XASM offers an interface to C allowing a) C-functions to be used as static or monitored ASM-functions, and b) ASMs to be called from within C-programs. In [223] one can find a denotational semantics of XASM. The applications of XASM for Montages and Teich's architecture and compiler co-generation project are described above.

The development of AsmGofer [277] was driven by the goal to provide for executability of the models for Java and the JVM defined in [291], although it represents a general interpreter for a large class of structured ASMs (see e.g. its use in the Light Control case study [94], or the use of its variant AsmHugs in [15]). It comes with GUI support, debugging facilities, and support for a literate programming technique. The structuring and composition concepts implemented in AsmGofer have been defined in [103] and have been used to decompose the Java/JVM models into language layered and functional components [62]. The definition of these concepts was driven by the double concern a) to distill some forms of standard programming constructs which are really needed in large applications, and b) to integrate them as natural standard refinements into the ASM world with simultaneous multiple updates of a global state. As a consequence these concepts are special cases of the more general algebraic concepts investigated in [236].

The MOSES tool suite in [213] is tailored for the specification and prototyp- ical implementation of visual notations for discrete-event systems. It comes with a graph editor (from visual notation), a simulator with animator, a debugger and some management tools.

Recently a new specification language AsmL developed by the Foundations of Software Engineering group headed by Gurevich at Microsoft Research has been made accessible [191, 16]. In [16, 17, 18] some applications of AsmL within Microsoft are reported. An important new feature of AsmL is the way it exploits the abstraction potential of ASMs to o er object-oriented structuring principles. The naturalness with which object oriented features can be described by ASMs had been observed and used already in [166, 33, 243, 244, 260, 225, 214, 215] and has led to Zamulin's systematic investigation of objects and generic types for ASMs [311, 312, 313, 314, 315, 316, 317]. A related effort was made in [67, 66, 216] and in Cavarra's PhD thesis [116] to exploit ASMs for a rigorous support of object-oriented UML techniques and concepts, triggered in the summer of 1999 by an evaluation of the high-level design characteristics of UML and of ASMs in an industrial software development environment [68]. This has inspired also the work in [251] where the ASM Workbench [123] is used to define an executable

semantics for UML which covers real-time aspects.

Linking ASMs to verification Tools. The successful link of ASMs to theorem proving systems like Isabelle, KIV, PVS, and to model checking [309] has been mentioned above. An interesting variation of model-checking, applied to the railroad crossing ASM of [186], appears in [21, 22]. Recently [293] KIV has been used also for checking the programs in Sun's Java manual against their ASM specification in [106]. A description of the tableau proof method in terms of ASMs at various levels of refinement leading from the textbook level to an implementation appears in [105].

Numerous logics have been developed to formalize ASMs and to support mechanical reasoning for them. See [172, 257, 259, 281, 299, 22]. In [263] the co-induction proof scheme is justified for ASMs, characterizing them as a class of Di-algebras and proposing "the Di-algebra thesis which improves the Turing thesis and which corresponds directly to the evolving algebra thesis: Real world computable algorithms coincide with algorithms specifiable by completely constraint Di-algebra specifications" [263, Section 3]. In [290] a logic for ASMs appears which unifies some of these logics and is based on an atomic predicate for function updates and on a definedness predicate for the termination of the evaluation of ASM rules. 6 Conclusion and Lessons for the Future

The notion of ASMs provides the basis for a taxonomy of discrete systems into classes of sequential and distributed systems [63]. The epistemological appropriateness of this classification of models of computation is guaranteed by the ASM thesis and strengthened by the arguments which prove the sequential ASM thesis [183] and its extension to parallel synchronous algorithms [40] from fun- damental postulates. The universality of the ASM model of computation is also pragmatically confirmed by { the naturalness with which other models of computation can be defined as ASM instances, directly, without any extraneous encoding (but typically not vice versa) [64], { the flexibility with which ASMs could be adapted to the diversity of modeling problems and techniques in different application domains and at different design levels, { the generality with which ASMs support a truly codeless form of programming, yielding programs|in fact semantically well-defined pseudo-code| which can be ported between languages and platforms in a semantically transparent way.

Through the collaborative effort described above a rigorous and practical high-level design and analysis method has been elaborated, which is mathematically underpinned by the concept of ASMs and has been successfully applied for industrial system developments. The approach offers a concrete way to turn the construction and investigation of sw/hw systems into an intellectually rewarding engineering task - a noble task of applied, experimentally backed up mathematics, or of scientifically well founded engineering of computing devices if one prefers to look at it the other way round 10 . Abrial's in various respects similar B method also shares this insight that

the task of programming (in the small as well as in the large) can be accomplished by returning to mathematics [4, page xi].

There are some risks the ASM method is facing, and numerous opportunities it can realize in the immediate future. First of all we have to continue to perform our work in the computer science core, solving real problems and not redoing ("in ASM terms") what has already been solved satisfactorily using other concepts or techniques. The ASM community must fight the tendency to isolate itself, the battlefield is computer science, not ASMs. On the other side, if we do not want the approach to fall back to a merely academic exercise, we are well adviced to capitalize the driving force computer technology had for the past development of ASMs. That is to say we should continue putting ASMs to use in cutting edge industrial applications where the interesting problems to be solved show up. 11 Our efforts in this direction have to be intensified, to permeate the research in those places where challenging hw/sw engineering problems are solved. If we want to attract talented young researchers, we have to demonstrate them that we do believe in the intellectual and practical value of unfolding the mathematical structure of complex computing devices 12 . This activity must be recognized and professed|first of all by ourselves|as not less rewarding, scientifically, than activities which are focussed on traditional mathematical themes or on tools with ever more fascinating features.

10 See the following remark by an observer of ASMs, N. Shankar (e-mail of February 12, 2002 to Börger): "The ASM model imposes a logical structure on transition systems that has inspired very capable mathematicians to construct remarkably elegant proofs. It is one of the few formal notations that appeals to both mathematicians and engineers."

11 Also the name change to Abstract State Machines was triggered by the concern to better render the practical relevance of the notion and in fact was pushed by our colleagues in industry [319]. The new name was found by Päppinghaus after two extensive community wide electronic discussions and replaced the more theoretical sounding name evolving algebras which itself already was a replacement of the original dynamic structures and later dynamic algebras. 12 See the observation by Blass [34, Section 4] that clearly there is no value in spelling out fully formalized say axiomatic set theory versions of non-trivial mathematical proofs, whereas explicitly writing out ASMs for complex algorithms may be worth-while from both the mathematical and the practical point of view, namely as a vehicle to provide a correct understanding and means of error detection and correction.

The ASM notion of distributed computation has to be elaborated and exploited more, both theoretically and practically, to provide transparent real-life patterns for communication and synchronization of multi-agent ASMs. It has to be made clear what advantage it presents over the pragmatic interleaving view of distributed computation. The stepwise refinement method has to be further developed and badly needs to be supported by tools, not only for simulation, but also for verification (relating proofs with different degrees of detail), testing (relating tests at different system levels), corrective maintenance and evolutionary system adaptation. The codeless form of programming ASMs offer has to be exploited for producing transparent software which is not only reliable| trustworthy and secure|, but can be certified (proven and checked) to have this property, all the way from its specification as a ground model to the implementation. The platform independence of abstract ASM code should be exploited for dealing with the challenges of intelligent agents, mobile code, middleware, system architectures built from components which o er and use services with heterogeneous access, typically by mobile users, and of context dependent service quality. We must aim for our tools to not replace, but enhance established tool environments so that they can meet advanced needs to capture and manipulate industrial design knowledge in a rigorous, electronically documented and reusable way. We should not rest until the use of ASMs has become current practice of professional system development and maintenance, scientifically secured to be worth the attribute professional. Acknowledgement

This survey of the ASM research at the end of the last century grew out of an attempt to answer frequently asked questions of new-comers about the reasons for this or that phenomenon they observe at their first encounter with ASMs. It is the result of a systematic study of the ASM literature, of my notes and of my ASM correspondence files which had accumulated over the years. In the retrospective it turns out that during the last 15 years we went a thorny way, full of external and internal obstacles, but we succeeded to make ASMs into what they are today. My gratitude goes to the students and colleagues|they are named in the text above and in the references|who through their work created this beautiful and promising ASM based system design and analysis method. Their trust in the endeavor and their enthousiasm reward for the negative side experiences. I also thank Schloss Dagstuhl for the ef- fective support of the three seminars in 1995, 1997, 1999 [5, 86, 84] - they helped considerably to work out how ASMs can contribute to professional software engineering practice -, for the invitations to many other seminars in the 90'ies where ASMs became the object of very helpful, often heated discussion, and last but not least for the forthcoming ASM 2002 seminar [35] which aims at bringing together ASM researchers from academia and ASM practitioners from industry.

I also thank the following colleagues for information and criticism which enabled me to complete and improve earlier versions of this bibliographical account: two referees and M. Anlauff, C. Beierle, A. Dold, I. Durdanovic, R. Gotzhein, J. Huggins, J. Janneck, A. Kappel, H. Langmaack, P. Päppinghaus, E. Riccobene, G. Schellhorn, J. Schmid, N. Shankar, A. Slissenko, A. Sunbul, J. Teich, L. Thiele, K. Winter, W. Zimmermann. References

1. S. Abiteboul, V. Vianu, B. Fordham, and Y. Yesha. Relational Transducers for Electronic Commerce. In Proceedings of 17th ACM Symposium on Principles of Database Systems (PODS 1998). ACM Press, 1998.

Relational transducers mapping sequences of input relations to sequences of out-put relations are proposed for high-level declarative specifications of business models. See [288] for a related class of ASM-transducers.

2. U. Abraham. Models for Concurrency. Gordon and Breach, 1999.

3. U. Abraham. Bakery Algorithms. Manuscript of 41 pages from University of Beer Sheva, Nov 19, 2001.

4. J-R. Abrial. The B-Book. Cambridge University Press, 1996.

5. J-R. Abrial, E. Börger, and H. Langmaack. Methods for Semantics and Specification, volume 117. Schloss Dagstuhl (Seminar No. 9523), May 1995.

6. J-R. Abrial, E. Börger, and H. Langmaack. Formal Methods for Industrial Applications. Specifying and Programming the Steam Boiler Control, volume 1165 of LNCS. Springer, 1996.

Contains the problem description for the steam boiler control competition and 22 proposed solutions obtained using the major known formal methods, with text and complete documentation on the accompanying CD.

7. J-R. Abrial, E. Börger, and H. Langmaack. The Steam Boiler Case Study: Competition of Formal Program specification and Development Methods. In J.-R. Abrial, E. Börger, and H. Langmaack, editors, Formal Methods for Industrial Applications. Specifying and Programming the Steam-Boiler Control, volume 1165 of LNCS, pages 1{12. Springer, 1996.

Motivation of the steam-boiler control competition and short characterization of the 22 problem solutions appearing in the book.

8. M. Anlauff. XASM { An Extensible, Component-Based Abstract State Machines Language. In Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, editor, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 69{90. Springer-Verlag, 2000.

The XASM (Extensible ASM) language for producing executable ASMs is pre- sented. A development environment for XASM systems is described. (XASM was formerly known as Aslan.) Also appears in TIK-Report 87, ETH Zürich, March 2000, 1{21.

9. M. Anlauff, S. Chakraborty, P.W. Kutter, A. Pierantonio, and L. Thiele. Generating an Action Notation environment from montages descriptions. Software Tools and Technology Transfer, Springer, 3:431{455, 2001.

Montages [11] are used to provide executable semantics for Action Notation. A preliminary version was published by M. Anlauff, P. Kutter, A. Pierantonio and L. Thiele under the title "Generating an Action Notation Environment from Montages Descriptions" in the Proceedings of the 2nd International Workshop on Action Semantics (AS'99), edited by P. Mosses and D. Watt, University of Aarhus, Department of Computer Science, BRICS Notes Series NS-99-3, March 1999, pages 1{42.

10. M. Anlauff, P. Kutter, and A. Pierantonio. Montages/Gem-Mex: a Meta Visual Programming Generator. TIK-Report 35, ETH Zürich, 1998.

An introduction to Montages [224] and Gem-Mex, the development tool for creating Montages (using a graphical editor) and generating language interpreters from them, supporting also debugging and animation features. A description of their use and some small examples can be found in Formal Aspects of and Development Environments for Montages by the same authors, published in M. Sellink (Ed.): 2nd International Workshop on the Theory and Practice of Algebraic Specifications, Springer Workshops in Computing 1997. Another description is in Tool Support for Language Design and Prototyping with Montages published by the same authors in Proceedings of Compiler Construction (CC'99), Springer LNCS 1999. Another illustration is in [12].

11. M. Anlauff, P. Kutter, and A. Pierantonio. Enhanced Control Flow Graphs in Montages. In D. Bjoerner and M. Broy, editors, Proceedings of Perspectives of System Informatics (PSI'99), Lecture Notes in Computer Science. Springer, 1999.

A refined definition of Montages, based on the notion of finite state machines, triggered by the use of Montages for defining the static semantics of Java in [304] which showed some shortcomings of the original formulation in [224].

12. M. Anlauff, P.W. Kutter, A. Pierantonio, and Asuman Sunbul. Using domain-specific languages for the realization of component composition. In T. Maibaum, editor, Fundamental Approaches to Software Engineering (FASE 2000), volume 1783 of Lecture Notes in Computer Science, pages 112 { 126, 2000.

An illustration of how to apply Montages [224, 11] and of its tool environment Gem-Mex [10] for the implementation of component interaction.

13. L. Araujo. Correctness proof of a Distributed Implementation of Prolog by means of Abstract State Machines. Journal of Universal Computer Science, 3(5):416{ 422, 1997.

Building upon [100], a specification and a proof of correctness for the Prolog Distributed Processor (PDP), a WAM extension for parallel execution of Prolog on distributed memory are provided. A preliminary version appeared in 1996 under the title Correctness proof of a Parallel Implementation of Prolog by means of Evolving Algebras as Technical Report DIA 21-96 of Dpto. Informatica y Automática, Universidad Complutense de Madrid.

14. U. Assmann, A. Heberle, W. Löwe, A. Ludwig, and R. Neumann. Language Concepts and Desing Patterns. Manuscript, 1999.

ASMs are used to define the semantics of patterns and for correctness proofs for workarounds.

15. M. Barnett, E. Börger, Y. Gurevich, W. Schulte, and M. Veanes. Using Abstract State Machines at Microsoft: A Case Study. In Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, editor, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 367{380. Springer-Verlag, 2000.

A descqription of a reverse engineering case study, modeling a command-line debugger of a stack-based runtime environment at three levels of abstraction.

16. M. Barnett and C. Campbell and W. Schulte and M. Veanes. specification, Simulation and Testing of COM Components using Abstract State Machines. In R. Moreno-Díaz and A. Quesada-Arencibia, editors, Formal Methods and Tools

for Computer Science (Local Proceedings of Eurocast 2001), pages 266{270, Ca- nary Islands, Spain, February 2001. Universidad de Las Palmas de Gran Canaria. A description of the use of AsmL to specify, simulate, and test the interfaces of Microsoft COM components.

17. M. Barnett, L. Nachmanson, and W. Schulte. Conformance Checking of Components Agaqinst Their Non-deterministic specifications. Technical Report MSR-TR-2001-56, Microsoft Research, June 2001.

A method for testing a Microsoft COM (Component Object Model) component against a (possibly non-deterministic) ASM specification is presented. See [171].

18. M. Barnett and W. Schulte. The ABCs of specification: AsmL, Behavior, and Components. Informatica, 17, 2002.

AsmL is shown to provide behavioral interfaces for components which allow to understand the meaning of an implementation without accessing the source code.

19. A. Bartoloni et al. A Hardware Implementation of the APE100 Architecture. International J. of Modern Phsysics, C(4):969, 1993.

The architecture which has been chosen by Börger for Del Castillo's Tesi di Laurea to try out ASMs for modeling real-world architectures, in the context of reengineering project for this machine which had been launched by a group of physicists in Pisa and Rome, see [71],[70].

20. A. Bartoloni et al. The Software of the APE100 Architecture. International J. of Modern Phsysics, C(4):955, 1993.

see comment to [19].

21. D. Beauquier and A. Slissenko. The Railroad Crossing Problem: Towards Semantics of Timed Algorithms and their Model-Checking in High-Level Languages. In M. Bidoit and M. Dauchet, editors, TAPSOFT'97: Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE, volume 1214 of LNCS, pages 201{212. Springer, 1997.

A semantics of ASMs with continuous time using infinitesimals is defined, their runs are decribed in some first order logic. The framework is used to discuss the verification of the railroad crossing problem, based upon its ASM specification in [186]. An early version appeared in 1996 as Technical Report 96-10 of Dept. of Informatics, Université Paris 12. For a continuation see [22].

22. D. Beauquier and A. Slissenko. A first order logic for specification of timed algorithms: basic properties and a decidable class. Annals of Pure and Applied Logic, 113(1-3):13{52, 2001.

A continuation of [21]. The authors define a) a class of algorithms (a modified version of ASMs) with explicit continuous time, and b) a First Order Timed Logic which suffices to write requirements specifications close to natural language, enhancing the logic in [21]. The timed logic description of the semantics of that class of ASMs can be viewed as a basic set of inductive invariants for proving properties of timed ASMs. The authors consider a decidable class of verification problems and outline a compact verification proof of the Generalized Railroad Crossing Problem [186]. A first version of this work appeared under the title On Semantics of Algorithms with Continuous Time in October 1997 as TR 97-15 of Dept. of Informatics, Université Paris 12. A survey of that TR and of [21] appears under the title verification of Timed Algorithms: Gurevich Abstract State Machines versus First Order Timed Logic in Y. Gurevich and P. Kutter and M. Odersky and L. Thiele(Eds): Abstract State Machines { ASM 2000, International Workshop on Abstract State Machines, Monte Verita, Switzerland, Local Proceedings, March 2000, ETH Zürich TIK-Report 87, pages 22{39. Continuation in TR-00-23 of June 2000, Université Paris-12, by the same authors and with the title A First Order Logic for specification of Timed Algorithms: Basic Properties and a Deciadable Class. For a set of more efficient inductive invariants for ASMs and a short formal proof of the Generalized Railroad Crossing Problem along the same lines see Technical Report TR{00{25, Université Paris 12, Department of Informatics, 2000, available at http://www.univ-paris12.fr/lacl/.

23. B. Beckert and J. Posegga. leanEA: A Lean Evolving Algebra Compiler. In H. Kleine Büning, editor, Proceedings of the Annual Conference of the European Association for Computer Science Logic (CSL'95), volume 1092 of LNCS, pages 64{85. Springer, 1996.

A 9-line Prolog interpreter for sequential ASMs, including discussion of extensions for layered ASMs. A preliminary version appeared in April 1995 under the title leanEA: A poor man's evolving algebra compiler as internal report 25/95 of Fakultat fü Informatik, Universitat Karlsruhe.

24. H. Behrends. Beschreibung ereignisgesteuerter Aktivitäten in datenbankgestützten Informationssystemen. PhD thesis, University of Oldenburg, 1995.

Uses ASMs to define the semantics of a language which is tailored to program the control of event driven database applications. The specification proceeds by stepwise refinement of event processing, rule selection among the event triggered rules, and action execution following the priorities of the selected rules. Thesis supervised by Appelrath. Issued as TR 3/95 of CS Departement of the University of Oldenburg, October 1995, 278 pages.

25. C. Beierle. Formal Design of an Abstract Machine for Constraint Logic Programming. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress, volume I: Technology/Foundations, pages 377{382, Elsevier, Amsterdam, the Netherlands, 1994.

Develops a general implementation scheme for CLP(X) over an unspecified constraint domain X, namely by designing a generic extension WAM(X) of the Warren Abstract Machine and a corresponding generic compilation scheme of CLP(X) programs to WAM(X) code. The scheme is based on the specification and correctness proof for compilation of Prolog programs in [100] and on joint work with Börger, see [26, 27, 28].

26. C. Beierle and E. Börger. Correctness Proof for the WAM With Types. In E. Börger, G. Jäger, H. Kleine Büning, and M. M. Richter, editors, Computer Science Logic, volume 626 of LNCS, pages 15{34. Springer, 1992.

The specification and correctness proof for compiling Prolog to WAM [100] is extended in modular fashion to the type-constraint logic programming language Protos-L which extends Prolog with polymorphic order-sorted (dynamic) types. In this paper, the notion of types and dynamic type constraints are kept abstract (as constraint) in order to permit applications to different constraint formalisms like Prolog III or CLP(R). The theorem is proved that for every appropriate type- constraint logic programming system L, every compiler to the WAM extension with an abstract notion of types which satisfies the specified conditions, is correct. [28] extends the specification and the correctness proof to the full Protos Abstract Machine by re ning the abstract type constraints to the polymorphic order-sorted types of PROTOS-L. Also issued as IBM Germany Science Center Research Report IWBS 205, 1991. Revised and final version published in [27].

27. C. Beierle and E. Börger. specification and correctness proof of a WAM extension with abstract type constraints. Formal Aspects of Computing, 8(4):428{462, 1996.

Revised version of [26].

28. C. Beierle and E. Börger. refinement of a typed WAM extension by polymorphic order-sorted types. Formal Aspects of Computing, 8(5):539{564, 1996.

Continuation of [27] which is extended to the full Protos Abstract Machine by refining the abstract type constraints to the polymorphic order-sorted types of PROTOS-L. Preliminary version published under the title A WAM Extension for Type-Constraint Logic Programming: specification and Correctness Proof as Research Report IWBS 200, IBM Germany Science Center, Heidelberg, December 1991.

29. C. Beierle, E. Börger, I. Durdanovic, U. Glässer, and E. Riccobene. Re ning Abstract Machine specifications of the Steam Boiler Control to Well Documented Executable Code. In J.-R. Abrial, E. Börger, and H. Langmaack, editors, Formal Methods for Industrial Applications. Specifying and Programming the Steam- Boiler Control, number 1165 in LNCS, pages 62{78. Springer, 1996.

The steam-boiler control specification problem is used to illustrate how ASMs applied to the specification and the verification of complex systems can be exploited for a reliable and well documented development of executable, but formally inspectable and systematically modi able code. A hierarchy of stepwise refined abstract machine models is developed, the ground version of which can be checked for whether it faithfully reflects the informally given problem. The sequence of machine models yields various abstract views of the system, making the various design decisions transparent, and leads to a C ++ program. This program has been demonstrated during the Dagstuhl-Meeting on Methods for Semantics and Specification, in June 1995, to control the FZI Steam-Boiler simulator satisfactorily. The proofs of properties of the ASM models provide insight into the structure of the system which supports easily maintainable extensions and modifications of both the abstract specification and the implementation. For a continuation of this use of ASMs for reliable software development see [89, 94].

30. G. Bella and E. Riccobene. Formal Analysis of the Kerberos Authentication System. Journal of Universal Computer Science, 3(12):1337{1381, 1997.

A formal model of the whole system is reached through stepwise refinements of ASMs, and is used as a basis both to discover the minimum assumptions to guarantee the correctness of the system, and to analyse its security weaknesses. Each refined model comes together with a correctness refinement theorem.

31. G. Bella and E. Riccobene. A Realistic Environment for Crypto-Protocol Analyses by ASMs. In U. Glässer and P. Schmitt, editor, Proceedings of the Fifth International Workshop on Abstract State Machines, pages 127{138. Magdeburg University, 1998.

ASMs are used to give a model of a general, realistic environment in which cryptographic protocols can be faithfully analyzed. The Needham-Schroeder protocol is investigated as an example.

32. S. Bistarelli and E. Riccobene. An Operational Model for the SCLP Language. ILPS Workshop on Tools and Environments for CLP held in Port Jefferson USA, 1997. Refinement and parallelization of the ASM model for Prolog to a semi-ring based constraint system, replacing the Call and Select rules of [44] by a Reduction rule which activates a child process simultaneously for each alternative of the current process.

33. B. Blakley. A Smalltalk Evolving Algebra and its Uses. PhD thesis, University of Michigan, Ann Arbor, Michigan, 1992.

A reduced version of Smalltalk is formalized by sequential ASMs. A Hoare-style proof system is defined for reasoning about storage allocation and deallocation in ASMs. Missing constructs concern processes, inheritance, memory allocation and deallocation. Thesis supervised by Gurevich.

34. A. Blass. Abstract State Machines and Pure Mathematics. In Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, editor, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 9{21. Springer-Verlag, 2000.

A discussion of connections, similarities, and differences between concepts and issues arising in the study of ASMs and those of set theory and logic.

35. A. Blass, E. Börger, and Y. Gurevich. Abstract State Machines , volume NN for Seminar 02101. Schloss Dagstuhl, March 2002.

36. A. Blass and Y. Gurevich. The Linear Time Hierarchy Theorems for Abstract State Machines. Journal of Universal Computer Science, 3(4):247{278, 1997. Contrary to polynomial time, linear time depends on the computation model. In 1992, N. Jones designed some computation models where the linear-speed- up theorem fails and linear-time computable functions form a proper hierarchy. The linear time of these models is restrictive. In this paper linear-time hierarchy theorems for random access machines and ASMs are proven. In particular it is shown that there exists a sequential ASM U (an allusion to "universal") and a constant c such that, under honest time counting, U simulates every other sequential ASM in lock-step with log factor c. One long-term goal of this line of research is to prove linear lower bounds for linear time problems. The result has been anounced under the title Evolving Algebras and Linear Time Hierarchy in B. Pehrson and I. Simon (Eds.), IFIP 13th World Computer Congress, vol.I: Technology/Foundations, Elsevier, Amsterdam, 1994, 383-390.

37. A. Blass and Y. Gurevich. The Logic of Choice. Journal of Symbolic Logic, 65(3):1264{1310, September 2000.

Motivated by the choice construct of ASMs, extensions of first-order logic with the choice construct (choose x : F (x)) are studied. Some results about Hilbert's operator are proven. The main part of the paper concerns the case where all choices are independent. Previously appeared as Technical Report CSE-TR-369- 98, EECS Dept., University of Michigan, 1998.

38. A. Blass and Y. Gurevich. Background, Reserve, and Gandy Machines. In P. Clote and H. Schwichtenberg, editors, Computer Science Logic (Proceedings of CSL 2000), volume 1862 of LNCS, pages 1{17. Springer, 2000. An investigation into the notion of the reserve set of an ASM, exploring the ideas of adding structure within the reserve (such as the hereditarily finite sets of [41]) and the non-determinism of importing new elements.

39. A. Blass and Y. Gurevich. New Zero-One Law and Strong Extension Axioms. Bulletin of EATCS, 72:103{122, October 2000.

A formulation of Shelah's proof of a zero-one law for the choiceless polynomial time variant of ASMs [41].

40. A. Blass and Y. Gurevich. Abstract State Machines Capture Parallel Algorithms. Technical Report MSR-TR-2001-117, Microsoft Research, November 2001.

The proof for the sequential ASM thesis [183] is extended to parallel synchronous algorithms.

41. A. Blass, Y. Gurevich, and S. Shelah. Choiceless Polynomial Time. Annals of Pure and Applied Logic, 100:141{187, 1999.

The question "Is there a computation model whose machines do not distinguish between isomorphic structures and compute exactly polynomial time properties?" became a central question of finite model theory. The negative answer was con- jectured in [176]. A related question is what portion of PTIME can be naturally captured by a computation model (when inputs are arbitrary finite structures). A PTIME version of ASMs is used to capture the portion of PTIME where al- gorithms are not allowed arbitrary choice but parallelism is allowed and, in some cases, implements choice. Earlier versions appeared as Technical Report CSE-TR- 338-97, EECS Department, University of Michigan, 1997, and Technical Report MSR-TR-99-08, Microsoft Research, February 1999. See [169].

42. A. Blass, Y. Gurevich, and S. Shelah. On Polynomial Time Computation Over Unordered Structures. Journal of Symbolic Logic, page to appear, 2001.

A consideration of several algorithmic problems near the border of the known, logically defined complexity classes contained in polynomial time, including the choiceless polynomial time defined in [41].

43. A. Blass, Y. Gurevich, and J. Van den Bussche. Abstract state machines and computationally complete query languages. In Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, editor, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 22{33. Springer-Verlag, 2000.

The use of the choiceless polynomial-time variant of ASMs [41] as a query language for relational databases is explored. Also appears in TIK-Report 87, ETH Zürich, March 2000, 40{65, and as Microsoft Research Technical Report MSR-TR-99-95.

44. E. Börger. A Logical Operational Semantics for Full Prolog. Part I: Selection Core and Control. In E. Börger, H. Kleine Büning, M. M. Richter, and W. Schönfeld, editors, CSL'89. 3rd Workshop on Computer Science Logic, volume 440 of LNCS, pages 36{64. Springer, 1990.

See Comments to [46].

45. E. Börger. A Logical Operational Semantics of Full Prolog. Part II: Built-in Predicates for Database Manipulation. In B. Rovan, editor, Mathematical Foundations of Computer Science, volume 452 of LNCS, pages 1{14. Springer, 1990.

See Comments to [46].

46. E. Börger. A Logical Operational Semantics forq Full Prolog. Part III: Built-in Predicates for Files, Terms, Arithmetic and Input-Output. In Y. Moschovakis, editor, Logic From Computer Science, volume 21 of Berkeley Mathematical Sciences Research Institute Publications, pages 17{50. Springer, 1992.

This paper, along with [44] and [45] are the original 3 papers which provide a complete ASM formalization of Prolog with all features discussed in the interna- tional Prolog standardization working group (WG17 of ISO/IEC JTCI SC22), see [69]. The specification is developed by stepwise refinement, describing orthogonal language features by modular rule sets. An improved (tree instead of stack based) version is found in [47, 48, 101]. These three papers were also published in 1990 as IBM Germany Science Center Research Reports 111, 115 and 117 respectively. The refinement technique, used in combination with corresponding methods of proof, is further developed in [100, 102, 83, 27, 28, 73, 88, 105, 89, 106, 291, 275] and became a constituent of the ASM method.

47. E. Börger. A Natural Formalization of Full Prolog. Newsletter of the Association for Logic Programming, 5(1):8{9, 1992.

The paper explains the abstract tree structure and the four ASM transition rules which govern the user-defined core of Prolog. See [46].

48. E. Börger. Dynamische Algebren und Semantik von Prolog. In E. Börger: Berechenbarkeit, Komplexitat, Logik, pages 476{499. Vieweg, 1992 (3d edition).

The first textbook definition of ASMs, elaborating notes of a series of lectures on Semantics of Programming Languages delivered to a summer school organized by Börger in Cortona in 1989. The definition is illustrated with machines operating on standard data structures and by the tree based version [47] of the core Prolog ASM in [44].

49. E. Börger. Logic Programming: The Evolving Algebra Approach. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress, volume I: Technology/Foundations, pages 391{395, Elsevier, Amsterdam, the Netherlands, 1994. Surveys the work which has been done from 1988{1994 on specifications of logic programming systems by ASMs.

50. E. Börger. Review of E.W.Dijkstra and C.S.Scholten Predicate Calculus and Program Semantics (Springer-Verlag 1989). Science of Computer Programming, 23:1{11, 1994.

Discusses the weakness of identifying the notion of proof with "formal proofs" and furthermore with "formal proofs in a strict format". Critically evaluates the authors' restricted view on the role of formal methods for program design and verification concerns. An abridged version appeared in Journal of Symbolic Logic 59 (1994) 673-678.

51. E. Börger (Ed.). specification and Validation Methods. Oxford University Press, 1995. The ASM related papers appearing in this volume are [181, 52, 102, 303, 83, 204, 189]. 52. E. Börger. Annotated Bibliography on Evolving Algebras. In E. Börger, editor, specification and Validation Methods, pages 37{51. Oxford University Press, 1995.

An annotated bibliography of papers (as of 1994) which deal with or use ASMs. For an updated version see [85]. 53. E. Börger. Why Use Evolving Algebras for Hardware and Software Engineering? In M. Bartosek, J. Staudek, and J. Wiederman, editors, Proceedings of SOF-SEM'95, 22nd Seminar on Current Trends in Theory and Practice of Informatics, volume 1012 of LNCS, pages 236{271. Springer, 1995.

A presentation of the salient features of ASMs, as part of a discussion and survey of the use of ASMs in design and analysis of hardware and software systems. The leading example is detailed and improved in [88].

54. E. Börger. Evolving Algebras and Parnas Tables. In H. Ehrig, F. von Henke, J. Meseguer, and M. Wirsing, editors, specification and Semantics. Dagstuhl Sem- inar No. 9626, July 1996.

Extended abstract showing that Parnas' approach to use function tables for precise program documentation can be generalized and gentilized in a natural way by using ASMs for well-documented program development.

55. E. Börger. Remarks on the History and some Perspectives of Abstract State Machines in Software Engineering. In W. Aspray, R. Keil-Slawik, and D. L. Parnas, editors, The History of Software Engineering , pages 12{17. Dagstuhl Seminar No. 9635, August 1996.

Survey of the development of the ASM method as of 1996. For an update in 2000 see [60]. 56. E. Börger. How to use Abstract State Machines in Software Engineering. In S. Jähnichen, J. Loeckx, D.R. Smith, and M. Wirsing, editors, Logic for Systems Engineering, volume 171, pages 5{7. Dagstuhl Seminar, March 3-7 1997.

The talk which triggered the first two years of work on the Java/JVM ASM project, as a comparative field test of purely declarative (functional or axiomatic) methods and their enhancement within an integrated abstract state-based operational (ASM) framework [106, 107, 108, 109, 110]. See preface to [291].

57. E. Börger. Ten Years of Gurevich's Abstract State Machines. In E. Börger, editor, Journal of Universal Computer Science, volume 3(4). Springer-Verlag, 1997.

Introduction to the first special ASM issue of the J. of Universal Computer Science. This April issue contains [194, 36, 129, 294, 193, 227, 276].

58. E. Börger. JUCS Special ASM Issue. Part II. In E. Börger, editor, Journal of Universal Computer Science, volume 3(5). Springer-Verlag, 1997.

Introduction to the second part of the special ASM issue of the J. of Universal Computer Science. This May issue contains [224, 225, 318, 13, 89, 237, 306].

59. E. Börger. High Level System Design and Analysis using Abstract State Ma-chines. In D. Hutter and W. Stephan and P. Traverso and M. Ullmann, editor, Current Trends in Applied Formal Methods (FM-Trends 98), number 1641 in LNCS, pages 1{43. Springer-Verlag, 1999.

A general introduction to and survey of the ASM method, including the definition of the ASM concept and an illustration of the main characteristics of the method, a comparison with other well-known system design and analysis approaches, and experimental evidence for the ASM thesis.

60. E. Börger. Abstract State Machines at the Cusp of the Millenium. In Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, editor, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 1{8. Springer-Verlag, 2000.

A brief survey of the history of the development of the ASM method and the current challenges in the field (continuation of [55]).

61. E. Börger (Ed.). Hardware Design and Validation Methods. Springer-Verlag, 2000. The ASM related paper appearing in this volume is [109].

62. E. Börger. Design for Reuse via Structuring Techniques for ASMs. In R. Moreno-Diaz and B. Buchberger and J-L. Freire, editor, Computer Aided Systems Theory{ EUROCAST 2001, volume 2178 of LNCS, pages 20{35. Springer-Verlag, 2001.

The composition and structuring concepts for sequential ASMs defined in [103] are used to illustrate a modular high-level definition of the architecture of the Java Virtual Machine, unfolding its language layering and its functional components for loader, verifier, and interpreter. Extracted from [291].

63. E. Börger. Discrete Systems Modeling. In R. A. Meyers, editor, Encyclopedia of Physical Science and Technology (Vol.4), pages 535{546. Academic Press (San Diego), 2001.

A classification of discrete systems and of methods for their mathematical verifiqcation and experimental validation, using ASMs as framework for the taxonomy.

64. E. Börger. Abstract State Machines: A Naturally Universal Computation Model. In P. Mosses, editor, Proc. FLoC'02 Workshop Action Semantics and Related Semantic Frameworks, BRICS Series. Department of Computer Science at Uni- versity of Aarhus, 2002

Continuing the work in [54, 59, 111] representative computation models in the literature are characterized as naturally arising special classes of ASMs. Classi- cal automata (Moore-Mealy, Co-Design FSM, Timed FSM, PushDown, Turing, Scott, Eilenberg, Minsky, Wegner), grammar formalisms, tree computation ma- chines, structured programs are covered, as well as system design models like UNITY, B, SCR (Parnas tables), Petri nets, Neural Nets, and logic based sys- tems including CSP, Z, VDM.

65. E. Börger, H. Busch, J. Cuellar, P. Päppinghaus, E. Tiden, and I. Wildgruber. Konzept einer hierarchischen Erweiterung von EURIS. Siemens ZFE T SE 1 Internal Report BBCPTW91-1 (pages 1-43), Summer 1996.

ASMs are proposed to extend the EURIS method for tool supported design of railway related software.

66. E. Börger, A. Cavarra, and E. Riccobene. An ASM Semantics for UML Activity Diagrams. In Teodor Rus, editor, Algebraic Methodology and Software Technol- ogy, 8th International Conference, AMAST 2000, Iowa City, Iowa, USA, May 20-27, 2000 Proceedings, volume 1816 of LNCS, pages 293{308. Springer-Verlag, 2000.

ASMs are used to disambiguate the semantics for activity diagrams in UML, defining a special subclass of ASMs appropriate to modeling such diagrams. As illustration a one-page UML activity diagram definition is given for the ASM model of Occam which appeared in [74]. For a continuation of this work to make semantic features of UML precise see [67].

67. E. Börger, A. Cavarra, and E. Riccobene. Modeling the Dynamics of UML State Machines. In Y. Gurevich and P. Kutter and M. Odersky and L. Thiele, editor, Abstract State Machines: Theory and Applications, volume 1912 of LNCS, pages 223{241. Springer-Verlag, 2000.

The work in [66] providing a rigorous semantics for basic UML features is ex- tended by an ASM definition of the dynamic semantics of UML state machines. These machines integrate statecharts with the UML object model. A rational reconstruction is given for the event driven run to completion scheme of UML (including the sequential entry/exit actions, the concurrent internal activities, and the event deferring mechanism) and for the concepts of action and durative action. The models make the semantic variation points of UML explicit, as well as various ambiguities and omissions in the official UML documents. For an executable version of these models see [116] where also various con ict situations are described which may arise through the concurrent behavior of active objects. This argument has been reconsidered by the same authors in Solving Con icts in UML State Machines Concurrent States presented to the Workshop on Concurrency Is- sues in UML - UML 2001, Toronto/Canada, and in A precise semantics of UML State Machines: Making Semantic Variation Points and Ambiguities Explicit in the Proceedings of the International Workshop on Semantic Foundations of En- gineering Design Languages (SFEDL'02) in conjunction with the 5th European Joint Conferences on Theory and Practice of Software (ETAPS'02).

68. E. Börger, M. Cesaroni, M. Falqui, and T. L. Murgi. Caso di Studio: Mail From Form System. Internal Report FST-2-1-RE-02, Fabbrica Servizi Telematici FST (Gruppo Atlantis), Uta (Cagliari), September 1999.

Feasability study of using ASMs for software analysis and design in an industrial object-oriented software development environment. Tow company internal case studies are developed. In view of a possible integration, the use of the ASM method for building ground models and re ning them to code is compared to the use of UML based tools, in particular Rational Rose.

69. E. Börger and K. Dässler. Prolog: DIN Papers for Discussion. ISO/IEC JTCI SC22 WG17 Prolog Standardization Document 58, National Physical Laboratory, Middlesex, England, 1990.

A version of [44, 45, 46] proposed to the International Prolog Standardization Committee as a complete formal semantics of Prolog. A streamlined version is in [101], representing the definition of the dynamic core of Prolog which has been accepted as the ISO standard [211].

70. E. Börger and G. Del Castillo. A formal method for provably correct composition of a real-life processor out of basic components (The APE100 Reverse Engineering Study). In B. Werner, editor, Proceedings of the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95), pages 145{148, November 1995.

Presents an ASM based technique by which a behavioural description of a processor is obtained as result of the composition of its (formally specified) basic architectural components. The technique is illustrated on the example of a subset the zCPU processor (used as control unit of the APE100 parallel architecture). A more complete version, containing the full formal description of the zCPU components, of their composition and of the whole zCPU processor, appeared in Y. Gurevich and E. Börger (Eds.), Evolving Algebras { Mini-Course, BRICS Technical Report (BRICS-NS-95-4), 195-222, University of Aarhus, Denmark, July 1995. This work is based upon G. Del Castillo's Tesi di Laurea "Descrizione Matematica dell'Architettura Parallela APE100", Universita di Pisa, academic year 1993/94.

71. E. Börger and G. Del Castillo and P. Glavan and D. Rosenzweig. Towards a Mathematical specification of the APE100 Architecture: the APESE Model. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress, volume I: Technology/Foundations, pages 396{401, Elsevier, Amsterdam, the Netherlands, 1994.

Defines an ASM model of the high-level programmer's view of the APE100 parallel architecture. This model is refined in [70] to an ASM processor model.

72. E. Börger and B. Demoen. A Framework to Specify Database Update Views for Prolog. In M. J. Maluszynski, editor, PLILP'91. Third International Symposium on Programming Languages Implementation and Logic Programming., volume 528 of LNCS, pages 147{158. Springer, 1991.

Provides a precise definition of the major Prolog database update views (immediate, logical, minimal, maximal), within a framework closely related to [44, 45, 46]. A preliminary version of this was published as The View on Database Updates in Standard Prolog: A Proposal and a Rationale in ISO/ETC JTCI SC22 WG17 Prolog Standardization Report no. 74, February 1991, pp 3-10.

73. E. Börger and I. Durdanovic. Correctness of compiling Occam to Transputer code. Computer Journal, 39(1):52{92, 1996.

The final draft version has been issued in BRICS Technical Report (BRICS-NS- 95-4), see [82]. Sharpens the refinement method of [100] to cope also with parallelism and non determinism for an imperative programming language. The paper provides a mathematical definition of the Transputer Instruction Set architecture for executing Occam together with a correctness proof for a general compilation schema of Occam programs into Transputer code.

Starting from the Occam model developed in [74], constituted by an abstract processor running a high and a low priority queue of Occam processes (which formalizes the semantics of Occam at the abstraction level of atomic Occam instructions), increasingly more refined levels of Transputer semantics are developed, proving correctness (and when possible also completeness) for each refinement step.

Along the way proof assumptions are collected, thus obtaining a set of natural conditions for compiler correctness, so that the proof is applicable to a large class of compilers. The formalization of the Transputer instruction set architecture has been the starting point for applications of the ASM refinement method to the modeling of other architectures (see [70, 88]).

74. E. Börger, I. Durdanovic, and D. Rosenzweig. Occam: specification and Compiler Correctness. Part I: Simple Mathematical Interpreters. In U. Montanari and E. R. Olderog, editors, Proc. PROCOMET'94 (IFIP Working Conference on Programming Concepts, Methods and Calculi), pages 489{508. North-Holland, 1994.

Improving upon the parse tree determined ASM in [190], a truly concurrent ASM model of Occam is defined as basis for a proven to be correct, smooth transition to the Transputer Instruction Set architecture. This model is stepwise refined, in a proven to be correct way, providing: (a) an asynchronous implementation of synchronous channel communication, (b) its optimization for internal channels, (c) the sequential implementation of processors using priority and time{slicing. See [73] for the extension of this work to cover the compilation to Transputer code.

75. E. Börger and U. Glässer. A Formal specification of the PVM Architecture. In B. Pehrson and I. Simon, editors, IFIP 13th World Computer Congress, volume I: Technology/Foundations, pages 402{409, Elsevier, Amsterdam, the Netherlands, 1994.

After Börger's lectures on ASMs at the University of Paderborn in the early summer of 1993, Glässer suggested to provide an ASM model for the Parallel Virtual machine (PVM [151], the Oak Ridge National Laboratory software system that serves as a general purpose environment for heterogeneous distributed computing). The model in this paper defines PVM at the C{interface, at the qlevel of abstraction which is tailored to the programmer's understanding. Cf. the survey An abstract model of the parallel virtual machine (PVM) presented at 7th International Conference on Parallel and Distributed Computing Systems (PDCS'94), Las Vegas/Nevada, 5.-9.10.1994. See [76] for an elaboration of this paper.

76. E. Börger and U. Glässer. Modelling and Analysis of Distributed and Reactive Systems using Evolving Algebras. In Y. Gurevich and E. Börger, editors, Evolv- ing Algebras { Mini-Course, BRICS Technical Report (BRICS-NS-95-4), pages 128{153. University of Aarhus, Denmark, July 1995.

This is a tutorial introduction into the ASM approach to design and verification of complex computing systems. The salient features of the method are explained by showing how one can develop from scratch an easily understandable and transparent ASM model for PVM [151], the widespread virtual architecture for heterogeneous distributed computing.

77. E. Börger and U. Glässer. Abstract State Machines 2001: New Developments and Applications. In Egon Börger and U. Glässer, editors, Journal of Universal Computer Science, volume 7(11), pages 914{917. Springer-Verlag, 2001.

Introduction to the third special ASM issue of JUCS, with papers selected from those submitted after the International ASM'2001 Workshop held in Las Palmas. This issue contains [196, 275, 290, 111, 141, 148, 278].

78. E. Börger and U. Glässer. Abstract State Machines Workshop 2001. In R. Moreno-Diaz and A. Quesada-Arencibia, editors, Formal Methods and Tools for Computer Science, pages 212{304. IUCTC Universidad de Las Palmas de Gran Canaria, 2001.

Abstracts of talks presented to the International ASM'2001 Workshop held in Las Palmas de Gran Canaria from February 13-19, 2001, as part of Eurocast 2001. See [77].

79. E. Börger, U. Glässer, and W. Müller. The Semantics of Behavioral VHDL'93 Descriptions. In EURO-DAC'94. European Design Automation Conference with EURO-VHDL'94, pages 500{505, Los Alamitos, California, 1994. IEEE CS Press.

Provides a transparent but precise ASM definition of the signal behavior and time model of full elaborated VHDL'93. This includes guarded signals, delta and time delays, the two main propagation delay modes transport,inertial, and the three process suspensions (wait on/until/for). Shared variables, postponed processes and rejection pulse are covered. The work is extended in [80].

80. E. Börger, U. Glässer, and W. Müller. Formal definition of an Abstract VHDL'93 Simulator by EA-Machines. In C. Delgado Kloos and P. T. Breuer, editors, Formal Semantics for VHDL, pages 107{139. Kluwer Academic Publishers, 1995.

Extends the work in [79] by including the treatment of variable assignments and of value propagation by ports. [271, 268] extend the VHDL model to analog VHDL