Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2000 | Book

Abstract State Machines at the Cusp of the Millenium Read chapter Read first chapter

Abstract State Machines - Theory and Applications

International Workshop, ASM 2000 Monte Verità, Switzerland, March 19–24, 2000 Proceedings

Editors: Yuri Gurevich, Philipp W. Kutter, Martin Odersky, Lothar Thiele

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

Included in: Professional Book Archive

Login to get access
insite
SEARCH

About this book

The ASM 2000 workshop was held in the conference center of the Swiss Federal Institute of Technology (ETH) at Monte Verit a, Canton Ticino, March 19-24, 2000. The ASM formalism was proposed together with the thesis that it is suitable to model arbitrary computer systems on arbitrary abstraction levels. ASMs have been successfully used to analyze and specify various hardware and software systems including numerous computer languages. The aim of the workshop was to bring together domain-experts, using ASMs as a practical speci cation method, and theorists working with ASMs and related methods. In addition the workshop served as a forum on theoretical and practical topics that relate to ASMs in a broad sense. Three tutorials including hands-on experience with tools were organized by U. Gl¨asser and G. del Castillo (on the topic \Specifying Concurrent Systems with ASMs"), H. Russ ¨ and N. Shankar (on the topic \A Tutorial Introduction to PVS"), M. Anlau , P.W. Kutter, and A. Pierantonio (on the topic \Developing Domain Speci c Languages"). In response to the organization committee’s call for papers, 30 papers were submitted, each of which was independently reviewed by four members of the program committee. This volume presents a selection of 12 of the refereed papers and two reports on industrial ASM application at Siemens AG and Microsoft Research, together with contributions based on the invited talks given by A.

Table of Contents

Frontmatter

Introduction

Abstract State Machines at the Cusp of the Millenium
Abstract
The ASM’2000 Workshop marks for the ASM method the transition from its adolescence to the maturation period. The goals which have been achieved open new frontiers and put us into the position to embark on new challenges.
Egon Börger

Mathematical Foundations

Abstract State Machines and Pure Mathematics
Abstract
We discuss connections, similarities, and differences between the concepts and issues arising in the study of abstract state machines and those arising in pure mathematics, particularly in set theory and logic. Among the topics from pure mathematics are the foundational role of set theory, permutation models of set theory without the axiom of choice, and interpretations (between theories or vocabularies) regarded as transformations acting on structures.
Andreas Blass
Abstract State Machines and Computationally Complete Query Languages
Abstract
Abstract state machines (ASMs) form a relatively new computation model holding the promise that they can simulate any computational system in lockstep. In particular, an instance of the ASM model has recently been introduced for computing queries to relational databases. This model, to which we refer as the BGS model, provides a powerful query language in which all computable queries can be expressed. In this paper, we show that when one is only interested in polynomial-time computations, BGS is strictly more powerful than both QL and while new , two well-known computationally complete query languages. We then show that when a language such as while new is extended with a duplicate elimination mechanism, polynomial-time simulations between the language and BGS become possible.
Andreas Blass, Yuri Gurevich, Jan Van den Bussche
On Verification of Refinements of Timed Distributed Algorithms
Abstract
This work is an attempt to apply Gurevich Abstract State Machines methodology to the verification of refinements of real-time distributed asynchronous algorithms. We define refinements following the semantical framework of observability, however, with respect to chosen pieces of the program. The time we consider is continuous as our motivation is related to systems of control that are usually specified within continuous time framework; the same framework is valid for discrete time. We remark that refinement of timed programs is not a simple replacement of a part of a program by making it more detailed. As an example to illustrate this we take Lamport’s Bakery Algorithm with real-time constraints. However, one of the key questions related to the verification of refinements is the preservation of verification proofs for the non refined initial algorithm as much as possible when verifying the refinement. This is the case for the notion of refinement we define. We introduce a notion of asynchronous timed distributed algorithm, define its semantics and discuss in what logic can be expressed its functioning. Then we introduce notions of refinement, and consider a refinement of interprocess communication of real-time Lamport’s Bakery algorithm using parallel message exchange. Such a refinement, contrary to our intuition, demands some non evident transformation of the initial algorithm to make it correct.
J. Cohen, A. Slissenko

Abstract State Machine Languages

Objects + Views = Components?
Abstract
In support of flexible composition, components need to be adaptable and they need to have first-class plugs. Abstract state machines and object-oriented programming each satisfy one of these requirements very well but satisfy the other only incompletely. This paper describes views, a language construct which provides for both requirements in a balanced way.
Martin Odersky
XASM- An Extensible, Component-Based Abstract State Machines Language
Abstract
The Abstract State Machine (ASM) [16] approach has already proven to be suitable for large-scale specifications of realistic systems [18,9,22,34]. Due to the fact that the ASM approach defines a notion of executing specifications, it provides a perfect basis for a language, which can be used as a specification language as well as a high-level programming language. However, in order to upgrade to a realistic programming language, such a language must — besides other features — add a modularization concept to the core ASM constructs in order to provide the possibility to structure large-scale ASM-formalizations and to flexibly define reusable specification units. In this paper, the language Xasm, which stands for Extensible ASM, is presented. Xasm realizes a component-based modularization concept based on the notion of external functions as defined in ASMs. This paper also briefly describes the support environment of Xasm consisting of the Xasm-compiler translating Xasm programs to C source code, and the graphical debugging and animation tool.
Matthias Anlauff
Generic Facilities in Object-Oriented ASMs
Abstract
Facilities for defining generic object types, generic type categories, generic functions and generic procedures in an object-oriented ASM are described in the paper. These facilities permit one to specify algorithms over complex data structures abstracting both from the type of the structure components and the structure itself. The use of the facilities is demonstrated by the specifications of some important parts of Standard Template Library for C++.
A. V. Zamulin

Distribution and Concurrency

Towards an ASM Thesis for Unconventional Algorithms
Abstract
All descriptions of algorithms, be they formal or informal, employ data structures, operations on them, and some policy to cause operations be applied to data. Gurevich calls a formal description technique for algorithms algorithm universal if it allows for each informally described algorithm a formal representation that would essentially make precise the notions used in the informal description, not employing additional data, operations or steps. Gurevich’s ASM thesis claims Abstract State Machines be algorithm universal for conventional, sequential algorithms. Here we are behind properties of formal presentations that are algorithm universal for unconventional, distributed algorithms.
Wolfgang Reisig
Partially Ordered Runs: A Case Study
Abstract
We look at some sources of insecurity and dificulty in reasoning about partially ordered runs of distributed ASMs, and propose some techniques to facilitate such reasoning. As a case study, we prove in detail correctness and deadlock-freedom for general partially ordered runs of distributed ASM models of Lamport’s Bakery Algorithm.
Yuri Gurevich, Dean Rosenzweig
Investigating Java Concurrency Using Abstract State Machines
Abstract
We present a mathematically precise, platform-independent model of Java concurrency using the Abstract State Machine method. We cover all aspects of Java threads and synchronization, gradually adding details to the model in a series of steps. We motivate and explain each concurrency feature, and point out subtleties, inconsistencies and ambiguities in the official, informal Java specification.
Yuri Gurevich, Wolfram Schulte, Charles Wallace

Compilers and Semantics

Verifying Compilers and ASMs or ASMs for Uniform Description of Multistep Transformations
Abstract
A verifying compiler ensures that the compiled code is always correct but the compiler may also terminate with an error mesage and then fails to generate code. We argue that with respect to compiler correctness this is the best possible result which can be achieved in practice. Such a compiler may even include unverified code provided the results of such code can be proven correct independently from how they are generated.We then show how abstract state machines (ASMs) can be used to uniformly describe the dynamic semantics of the programs being compiled across the various intermediate transformation steps occurring within a compiler. Besides being a convenient tool for describing dynamic semantics the fact that we do not have to switch between difaerent descriptional methods is found to be extremely useful.
Gerhard Goos, Wolf Zimmermann
An ASM Dynamic Semantics for Standard ML
Abstract
The Abstract State Machines (ASM) methodology is a methodology for formally specifying computing systems. We use the ASM methodology to give the dynamic semantics of the functional programming language Standard ML. We give an operational semantics for Standard ML by means of an interpreter for (appropriately pre-processed) Standard ML programs; the effect of a Standard ML instruction can be seen in terms of the corresponding actions performed by the ASM.
Steven C. Cater, James K. Huggins
Modeling the Dynamics of UML State Machines
Abstract
We define the dynamic semantics of UML State Machines which integrate statecharts with the UML object model. The use of ASMs allows us (a) to rigorously model the event driven run to completion scheme, including the sequential execution of entry/exit actions (along the structure of state nesting) and the concurrent execution of internal activities; (b) to formalize the object interaction, by combining control and data flow features in a seamless way; and (c) to provide a precise but nevertheless provably most general computational meaning to the UML terms of atomic and durative actions/activities. We borrow some features from the rigorous description of UML Activity Diagrams by ASMs in [7].
Egon Börger, Alessandra Cavarra, Elvinia Riccobene
On the Formal Semantics of SDL-2000:A Compilation Approach Based on an Abstract SDL Machine
Abstract
In November 1999, a new version of SDL (Specification and Description Language) called SDL-2000 has passed ITU, an international standardization body for telecommunication. SDL is a fairly complex, graphical formal description technique for the development of distributed systems, and has been broadly used in industry for many years. Efforts to define the semantics of SDL-2000 formally have started early in 1998. By now, a draft formal semantics is available, which is determined to become the official formal SDL semantics after its approval in 2000. It is based on the formalism of Abstract State Machines (ASMs), which has been selected for several reasons including intelligibility and executability. The formal semantics of SDL addresses the static semantics, transformation rules, and the dynamic semantics. The approach taken to define the dynamic semantics is particularly interesting. Although basically being operational, it differs from existing approaches in several ways. In this paper, we address and highlight some of these differences, using a simplified specification language called SSL instead of SDL. In defining a formal dynamic semantics for SSL, we formally describe an abstract machine, a compilation function mapping SSL specifications to code of this machine, and an operational definition of the set of initial states, using ASM as the underlying formalism. Furthermore, we present in some detail the semantics of SSL procedure calls.
Robert Eschbach, Uwe Glässer, Reinhard Gotzhein, Andreas Prinz
Description and Simulation of Microprocessor Instruction Sets Using ASMs
Abstract
In this paper, we describe how cycle-accurate processor behavior may be efficiently described using Abstract State Machines (ASMs). Given a register transfer description of the target processor, an extraction mechanism is described following the approach in [26] that extracts so called guarded register transfer patterns from the processor description. It will be shown that these may be directly transformed into a set of ASM rules which in turn provide an executable model of the processor for simulation purposes. Here, we use the ASM description language XASM from which the Gem-Mex tool [2] automatically generates a graphical simulator of a given architecture. The feasibility of this approach is demonstrated for an ARM microprocessor.
Jürgen Teich, Kutter Philipp W., Ralph Weper

Automatic Verication and Model Checking

Symbolic Analysis of Transition Systems?
Abstract
We give a brief overview of the Symbolic Analysis Laboratory (SAL) project. SAL is a verification framework that is directed at analyzing properties of transition systems by combining tools for program analysis, model checking, and theorem proving. SAL is built around a small intermediate language that serves as a semantic representation for transition systems that can be used to drive the various analysis tools.
Natarajan Shankar
Encoding Abstract State Machines in PVS
Abstract
In this paper we show how the specifcation and verifcation system PVS (Prototype Verifcation System) can provide tool support for Abstract State Machines (ASMs), especially oriented towards automatic proof checking and mechanized proving of properties. Useful templates are presented which allow encoding of ASM models into PVS without any extra user’s skill. We prove the transformation preserves the ASM semantics and provide a framework for an automatic tool, prototypically implemented, which translates ASM specifcations in PVS. The ASM specifcation of the Production Cell given in [4] is taken as case study to show how to formalize multi-agent ASMs in PVS and prove properties.
Angelo Gargantini, Elvinia Riccobene
Model Checking Abstract State Machines and Beyond
Abstract
We propose a systematic investigation of the (semi-) automatic verifiability of ASMs. As a first step, we put forward two verification problems concerning the correctness of ASMs and investigate the decidability and complexity of both problems.
Marc Spielmann
Towards a Methodology for Model Checking ASM: Lessons Learned from the FLASH Case Study
Abstract
Gurevich’s Abstract State Machines (ASM) constitute a high-level specification language for a wide range of applications. The existing tool support for ASM was extended, in a previous work, to provide computer-aided verification, in particular by model checking. In this paper, we discuss the applicability of the model checking approach in general and describe the steps that are necessary tofit different kinds of ASM models for the model checking process. Along the example of the FLASH cache coherence protocol, we show how model checking can support development and debugging of ASM models. We show the necessary refinement for the message passing behaviour in the protocol and give examples for errors found by model checking the resulting model. We conclude with some general remarks on the existing transformation algorithm.
Kirsten Winter

Industrial Applications

Report on a Practical Application of ASMs in Software Design
Abstract
ASMs have been used at Siemens Corporate Technology to design a component in a software package called FALKO. Main purpose of FALKO is the construction and validation of timetables for railway systems. For simulation the whole closed-loop trafic control system is modelled within FALKO. The railway process model part of FALKO was formally specified using the ASM approach. C++ code is generated from the formal specification and compiled together with the handwritten C++ code of the other components to obtain the FALKO executable. The project started in May 1998 and was finished in March 1999. Since then FALKO is used by the Vienna Subway Operator for the validation of the whole subway operational service.
Egon Börger, Peter Päppinghaus, Joachim Schmid
Using Abstract State Machines at Microsoft: A Case Study
Abstract
Our goal is to provide a rigorous method, clear notation and convenient tool support for high-level system design and analysis. For this purpose we use abstract state machines (ASMs). Here we describe a particular case study: modeling a debugger of a stack based runtime environment. 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. High level ASM models of proposed or existing programs can be used throughout the software development cycle. In particular, ASMs can be used to model inter component behavior on any desired level of detail. This allows one to specify application programming interfaces more precisely than it is done currently.
Mike Barnett, Egon Börger, Yuri Gurevich, Wolfram Schulte, Margus Veanes
Backmatter
Metadata
Title
Abstract State Machines - Theory and Applications
Editors
Yuri Gurevich
Philipp W. Kutter
Martin Odersky
Lothar Thiele
Copyright Year
2000
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-540-44518-0
Print ISBN
978-3-540-67959-2
DOI
https://doi.org/10.1007/3-540-44518-8