|
Abstract State Machines 2001: New Developments
and Applications
J.UCS Special Issue
Egon Börger (University of Pisa, Italy)
boerger@di.unipi.it
Uwe Glässer (University of Paderborn, Germany)
glaesser@upb.de
Abstract: From February 19-23 of this year, the 8th
International Abstract State Machines Workshop took place in Las
Palmas de Gran Canaria on the Canary Islands (Spain), organized by us
as part of Eurocast 2001. The intensive three-days program consisted
of 24 contributed papers and three invited lectures, by Yuri Gurevich
("Abstract State Machines: Theory and Applications"), Joseph Sifakis
("Some Trends in Modeling Real-Time Systems"), and Egon Börger
("Design for Reuse via Structuring Techniques for ASMs"). See the
extended abstracts in "Formal Methods and Tools for Computer Science"
(Ed. R. Moreno-Diaz and A. Quesada-Arencibia, IUCTC Universidad de Las
Palmas de Gran Canaria, ISBN 84-699-3971-8) and the revised text of
Börger's lecture in Proc. EUROCAST'2001 (Ed. R. Moreno-Diaz and
A. Quesada-Arencibia), Springer LNCS 2178 (2001).
We thank the members of the program committee of the workshop who
helped us to attract and review the papers which have been submitted
for presentation at the workshop: R. Gotzhein (University of
Kaiserslautern), S. Graf (IMAG, Grenoble), Y. Gurevich (Microsoft
Research, Redmond), P. Paeppinghaus (Siemens AG, Munich), A. Slissenko
(University of Paris 12), J. Teich (University of Paderborn),
L. Thiele (ETH Zürich), W. Zimmermann (University of Halle).
As announced in the Call for Participation, after the workshop a
reviewing process was started to select the best papers which appear
here as an ASM issue of J.UCS - the third one of its kind, see J.UCS 3.4 (April 1997) and J.UCS 3.5 (May 1997). We thank the following
colleagues who acted as reviewers:
Uri Abraham (Ben Gurion University, Beer Sheva, Israel)
Wolfgang Ahrendt (Chalmers University, Goeteborg, Sweden)
Matthias Anlauff (Kestrel Institute, Palo Alto, USA)
Richard Banach (University of Manchester, Great Britain)
Antonella Bertolino (IEI-CNR, Pisa, Italy)
Alessandra Cavarra (Oxford University, Great Britain)
Eduard Cerny (University of Montréal, Canada)
Jim Davies (University of Oxford, Great Britain)
Giuseppe Del Castillo (Siemens AG, Munich, Germany)
John Derrick (University of Kent at Canterbury, Great Britain)
Renardel de Lavalette (University of Groningen, Netherlands)
Arnaud Durand (University of Paris 12, France)
Angelo Gargantini (University of Catania, Italy)
Giorgio Ghelli (University of Pisa, Italy)
Martin Gogolla (University of Bremen, Germany)
Gerhard Goos (University of Karlsruhe, Germany)
Reinhard Gotzhein (University of Kaiserslautern, Germany)
Susanne Graf (IMAG Grenoble, France)
Jim Huggins (Kettering University, USA)
Heinrich Hussmann (Technical University Dresden, Germany)
Uwe Kastens (University of Paderborn, Germany)
Ekkart Kindler (University of Augsburg, Germany)
Alexander Knapp (Technical University of Munich, Germany)
Hans Langmaack (University of Kiel, Germany)
Luciano Lavagno (University of Udine, Italy, and University
of California at Berkeley, USA)
Angelo Morzenti (Politecnico of Milan, Italy)
Lev Nachmanson (Microsoft Research, Redmond, USA)
Ileana Ober (Telelogic Technologies Toulouse, France)
Peter Paeppinghaus (Siemens AG, Munich, Germany)
Sibylle Peuker (Software Verification Research Centre,
University of Queensland, Australia)
Mauro Pezze (University of Milan - Bicocca, Italy)
Elvinia Riccobene (University of Catania, Italy)
Willem-Paul De Roever (University of Kiel, Germany)
Dean Rosenzweig (University of Zagreb, Croatia)
Heinrich Rust (University of Cottbus, Germany)
P. Y. A. Ryan (Carnegie Mellon University, USA)
Gerhard Schellhorn (University of Augsburg, Germany)
Joachim Schmid (Siemens Research, Munich, Germany)
Peter Schmitt (University of Karlsruhe, Germany)
Klaus Schnieder (University of Karlsruhe, Germany)
Natarajan Shankar (SRI, Menlo Park, USA)
Anatol Slissenko (Université de Paris, France)
Xiaoyu Song (University of Montréal, Canada)
Maria Sorea (SRI, Menlo Park, USA)
Robert Stärk (ETH Zürich, Switzerland)
Sofiene Tahar (University of Montreal, Canada)
Juergen Teich (University of Paderborn, Germany)
Lothar Thiele (ETH Zürich, Switzerland)
Margus Veanes (Microsoft Research, Redmond, USA)
Miroslav Velev (Carnegie Mellon University, USA)
Klaus Winkelmann (Siemens Research, Munich, Germany)
Wolf Zimmermann (University of Halle, Germany)
They critically evaluated 19 papers submitted after the workshop,
providing 64 reviews which resulted in the present set of
contributions to this issue.
As has been characteristic for ASM workshops over the years, the
covered themes range from theoretical foundations to industrial
applications. On the theoretical side, the reader can find four new
conceptual developments. In "Partial Updates: Exploration" (by
Y. Gurevich and N. Tillmann) a solution is proposed for the partial
update problem for counters, sets and maps. In "Verification of ASM
Refinements Using Generalized Forward Simulation" (by K. Schellhorn) a
practical general proof principle for ASM refinements using commuting
diagrams is distilled which came out of the KIV verification of the
refinement correctness proof linking the ISO Prolog ASM to the WAM
ASM. In "A Complete Logic for Abstract State Machines" (by R.F. Stärk
and S. Nanchen) a new logic for non-distributed, deterministic,
structured ASMs with sequential composition and recursive submachines
is developed on the basis of an atomic predicate for function updates
and of a definedness predicate for the termination of the evaluation
of transition rules. In "A Neural Abstract Machine" (by E. Börger and
D. Sona) Alessandro Sperduti's question is answered whether the
fundamental features can be made explicit which are common to the
multitude of current neural network models and implementations.
On the practical side, the reader finds a discussion of fundamental
questions concerning the practicability, adequacy and maintainability
of the recent ASM definition of the International Telecommunication
Union standard for SDL-2000 in the paper "Formal Definition of
SDL-2000 - Compiling and Running SDL Specifications as ASM Models"
(by R. Eschbach, U. Glässer, R. Gotzhein, M. von Löwis,
A. Prinz). In "ASM-Based Testing:
Coverage Criteria and Automatic Test Generation" (by A. Gargantini
and E. Riccobene) ASMs are used for the first time to define and
analyze methods for the generation of test suites from high-level
specifications. In "Compiling Abstract
State Machines to C++" (by J. Schmid) a compilation scheme is
detailed which transforms algebraic data types, pattern matching,
functional expressions, dynamic functions, and simultaneous updates in
an efficient way to C++ code, describing a compiler which has been
built for, and successfully used in, a middle sized industrial project
at Siemens Corporate Technology. In "The Location Consistency
Memory Model and Cache Protocol: Specification and Verification"
(by C. Wallace, G. Tremblay, and J.N. Amaral) the reader finds an
interesting use of an appropriate ASM model for what the title of the
paper announces.
Last but not least we want to thank the J.UCS team for their perfect
technical assistance in producing this special ASM issue.
Egon Börger and Uwe Glässer
Pisa, Italy and Paderborn, Germany
November 2001
|
