Publikationen zum Fachbereich ASM

Publikationen in Zeitschriften und Büchern

• Wolfgang Reisig. Abstract State Machines for the Classroom - The Basics. Logics of Specification Languages, XXII, 624 p. 69 illus., Hardcover: pp 15-46, 2008.

  Abstract: Abstract State Machines (henceforth referred to as just ASM) were introduced as \"a computation model that is more powerful and more universal than standard computation models\" by Yuri Gurevich in 1985. Here we provide some intuitive and motivating arguments, and characteristic examples for (the elementary version of) ASM. The intuition of ASM as a formal framework for \"pseudocode\" algorithms is highlightes. Generalizing variants of the fundamental \"sequential small-step\" version of ASM are also considered.

  

• Wolfgang Reisig. The computable kernel of Abstract State Machines. Theoretical Computer Science, 409: 126-136, August 2008.

  Abstract: Abstract State Machines (ASMs) were introduced as "a computation model that is more powerful and more universal than standard computation models", by Yuri Gurevich in 1985. ASMs gained much attention as a specification method. It is extremely flexible because any mathematical structure may serve as a state. Gurevich characterized the expressive power of ASMs in terms of intuitively convincing postulates. The core result of this paper shows that the next-state function M of an Abstract State Machine M can be described on a symbolic level, notwithstanding the generality of the model: The successor state M(S) of a state S is fully specified by the equivalence ~s induced by S on the terms over the signature of M. Consequently, M(S) is computable in case ~s is decidable. Furthermore, this result implies a notion of computability for general structures, e.g. for algorithms operating on real numbers.

  

• Wolfgang Reisig. On Gurevich's Theorem on Sequential Algorithms. Acta Informatica, 39(5): 273-305, 2003.

  Abstract: Abstract-State Machines have been introduced as ?a computation model that is more powerful and more universal than standard computation models?, by Yuri Gurevich in 1985 ([Gur85]). ASM gained much attention as a specification method, in particular for the description of the semantics of programming languages, communication protocols, distributed algorithms, etc. Gurevich proved recently that a sequential algorithm must only meet a few, liberal requirements, to be representable as an ASM. We re-formulate Gurevich?s requirements for sequential algorithms, as well as the semantics of ASM-programs and the proof of his main theorem. A couple of examples support and explain intuition and motivation of ASM.

  

• Wolfgang Reisig. The Expressive Power of Abstract State Machines. Computing and Informatics, 22(3): 209-219, 2003.

  Abstract: Conventional computation models assume symbolic representations of states and actions. Gurevich's "Abstract-State Machine" model takes a more liberal position: Any mathematical structure may serve as a state. This results in "a computational model that is more powerful and more universal than standard computation models". We characterize the Abstract-State Machine model as a special class of transition systems that widely extends the class of "computable" transition systems. This characterization is based on a fundamental Theorem of Y. Gurevich.

  

Konferenzbeiträge und Beiträge auf Workshops

• Andreas Glausch. A Semantic Characterization of Elementary Wide-Step ASMs. In Proceedings of the 14th International ASM Workshop, June 2007.

• Andreas Glausch and Wolfgang Reisig. A Semantic Characterization of Unbounded-Nondeterministic ASMs. In Proceedings of the 2nd Conference on Algebra and Coalgebra in Computer Science, volume 4624 of Lecture Notes in Computer Science, August 2007.

  Abstract: Universal algebra usually considers and examines algebras as static entities. In the mid 80ies Gurevich proposed Abstract State Machines (ASMs) as a computation model that regards algebras as dynamic: a state of an ASM is represented by a freely chosen algebra which may change during a computation. In 2000, Gurevich characterized the class of sequential ASMs in a purely semantical way by five amazingly general and elegant axioms. Later this result has been extended to bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among unboundedly many (sometimes infinitely many) alternatives. We characterize the class of unbounded-nondeterministic ASMs by an extension of Gurevich's original axioms for sequential ASMs. We apply this result to prove the reversibility of unbounded-nondeterministic ASMs.

  

• Andreas Glausch and Wolfgang Reisig. An ASM-Characterization of a Class of Distributed Algorithms. In Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis, Festschrift volume of Lecture Notes in Computer Science, 2007. Springer. Note: To appear.

• Andreas Glausch. Distributed Abstract State Machines - Status Report of a Doctoral Thesis. In Jörg Desel, editor, Proceedings of the Doctoral Consortium ACSD & PetriNets 2006, Turku, Finland, June 2006. Åbo Akademi.

  Abstract: In 1985, Gurevich introduced Abstract State Machines (ASMs) as a computational model more powerful and universal than classical computational models. Since then ASMs have been applied successfully both in theory and practice: On the theoretical side, ASMs evolved to a general basis for the study of different classes of algorithms and their expressive power. On the practical side, ASMs have been extended to a full-fledged design methodology, applied successfully in industry for the specification and analysis of real-world systems. In my doctoral thesis I examine the class of distributed ASMs and study their expressive power. I also intend to develop basic notions of refinement and composition for distributed ASMs.

  

• Dirk Fahland and Wolfgang Reisig. ASM-based semantics for BPEL: The negative Control Flow. In Danièle Beauquier, Egon Börger, and Anatol Slissenko, editors, Proceedings of the 12th International Workshop on Abstract State Machines (ASM'05), pages 131-151, March 2005. Paris XII.

  Abstract: BPEL is presently the most prominent language to specify and execute business processes, using Web Services as its technological basis. Particular problems arise when activities are faulty: faults have to be propagated, other activities have to be irregularly terminated, etc. We describe the formal semantics of fault handlers and event handlers, demonstrating that ASMs are most adequate for this purpose.

  

• Wolfgang Reisig. The Computable Kernel of ASM. In Egon Börger, Angelo Gargantini, and Elvinia Riccobene, editors, Abstract State Machines, Advances in Theory and Practice, 10th International Workshop, ASM 2003, Taormina, Italy, volume 2589 of Lecture Notes in Computer Science, pages 421-422, 2003.

  Abstract: A rich variety of system models for sequential, deterministic systems has been suggested during recent decades, including automata, process algebras, many versions of Petri Nets, and models to describe the semantics of Programming languages. All models for sequential, deterministic systems assume a set S of states, or configurations, and a next state function $\upsilon: S \rightarrow S$.

  

• Wolfgang Reisig. Towards an ASM Thesis for Unconventional Algorithms. In Yuri Gurevich, Philipp W. Kutter, Martin Odersky, and Lothar Thiele, editors, Abstract State Machines, volume 1912 of Lecture Notes in Computer Science, pages 112-130, 2000. Springer-Verlag.

  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.

  

Technische Berichte

• Andreas Glausch and Wolfgang Reisig. Distributed Abstract State Machines and Their Expressive Power. Informatik-Berichte 196, Humboldt-Universität zu Berlin, January 2006.

  Abstract: Gurevich's sequential Abstract State Machines (ASMs)are taken as a basis for the construction of distributed ASMs as sets of sequential ASMs. A theorem on the expressive power of distributed ASMs is proven in analogy to Gurevich's classical theorem on the expressive power of sequential ASMs.

  

• Andreas Glausch and Wolfgang Reisig. On the Expressive Power of Unbounded-Nondeterministic Abstract State Machines. Informatik-Berichte 211, Humboldt-Universität zu Berlin, December 2006.

  Abstract: Conventional computational models assume a symbolical representation of states. Gurevich's Abstract State Machines (ASMs) take a more liberal position: any mathematical structure may serve as a state. Gurevich characterizes the expressive power of sequential ASMs in a non-trivial theorem: he defines the class of \emph{sequential algorithms} by help of only a few, amazingly general requirements and proves this class to be equivalent to sequential ASMs. Later, this result has been extended to the class of bounded-nondeterministic ASMs. This paper considers the general case of unbounded-nondeterministic ASMs: in each step, an unbounded-nondeterministic ASM may choose among infinitely many alternatives. We define the class of unbounded-nondeterministic algorithms by a conservative extension of Gurevich's original requirements to sequential algorithms. We show that this class is equivalent to unbounded-nondeterministic ASMs.

  

• Dirk Fahland. Complete Abstract Operational Semantics for the Web Service Business Process Execution Language. Informatik-Berichte 190, Humboldt-Universität zu Berlin, September 2005.

  Abstract: In this technical report we present an abstract operational semantics for the Business ProcessExecution Language for Web Services, or BPEL for short. In effect, the semantics defined herein are a variation and an extension of the semantics published first in [FGV04a] and [Far04] defined by the group of Uwe Glässer the Simon Fraser University, Vancouver, Canada. We namely add semantics for correlation handling, dead path elimination and event handling; we define the data handling on a finer level; we slightly alter the basic framework of how activities are formalized in [FGV04a] in order to achieve greater robustness against changes of the informal specification. Furthermore this technical report serves as a base for a joint work with the group of Simon Fraser University.

  

• Wolfgang Reisig and A. Brade. ASM Models for Web Services. Informatik-Berichte 181, Humboldt-Universität zu Berlin, 2004.

Studien- und Diplomarbeiten

• Alexander Brade. ASMs und die Struktur und Dynamik von Web Services. Studienarbeit, Humboldt-Universität zu Berlin, January 2005.

• Alexander Brade. Übersetzung graphischer Verhaltensbeschreibungen von Services in Abstract State Machines. Diplomarbeit, Humboldt-Universität zu Berlin, September 2005.

  Abstract: Zu Beginn dieser Arbeit werden wir kurz die Begriffe Service OrientedArchitecture und Service erklären. Den Begriff der Services werden wir genauer betrachten. Im Anschluss daran werden wir die Frage behandeln, wie das dynamische Verhalten eines Services mit UML 2-Diagrammen (UML = Unified Modeling Language) graphisch beschrieben werden kann. Dazu werden wir uns besonders auf die UML 2-Verhaltensdiagramme konzentrieren. Dabei werden wir auch einige Einschränkungen an den Verhaltensdiagrammen vornehmen. Wir werden dann das dynamische Verhalten eines beispielhaften DinnerServices mit Hilfe von Verhaltensdiagrammen beschreiben. Diese Verhaltensdiagramme des DinnerServices werden wir in Abstract State Machines (ASMs) übersetzen. Zwei der so erhaltenen ASMs werden wir im Anschluss an die Verhaltensbeschreibungen des DinnerServices in die Spezifikationssprache AsmL überführen und simulieren. Abschließend betrachten wir kurz die Verfeinerungsmöglichkeiten von ASMs.

  

• Andreas Glausch. Varianten des ASM-Theorems. Diplomarbeit, Humboldt-Universität zu Berlin, June 2005.

  Abstract: Abstract-State-Machines, kurz ASMs, sind eine Methode zur formalen Beschreibung von Algorithmen. Diese Methode hebt sich dabei deutlich von klassischen Algorithmusbegriffen wie Turingmaschinen und berechenbaren Funktionen ab. So lassen sich mit ASMs unter anderem auch nicht-terminierende Algorithmen beschreiben. Genauso wie es unterschiedliche Klassen von Algorithmen gibt, existieren auch eine ganze Reihe unterschiedlicher Klassen von ASMs, so zum Beispiel die sequentiellen, die nichtdeterministischen und die verteilten ASMs. Für die Klasse der sequentiellen ASMs exisitiert eine schöne Charakterisierung durch das sogenannte ASM-Theorem. Diese Charakterisierung basiert auf natürlichen und leicht verständlichen Forderungen und erleichtert somit dass Verständnis für die Ausdrucksmächtigkeit der sequentiellen ASMs und von Algorithmen im Allgemeinen. In dieser Arbeit erweitern wir das ASM-Theorem auf die Klasse der nichtdeterministischen ASMs und auf die Klasse der verteilten ASMs.

  

• Dirk Fahland. Ein Ansatz einer formalen Semantik der Business Process Execution Language for Web Services mit Abstract State Machines. Studienarbeit, Humboldt-Universität zu Berlin, August 2004.

  Abstract: In dieser Arbeit stellen wir einen Ansatz zur Definition einer formalen Semantik für die Business Process Execution Language for Web Services (kurz BPEL4WS) von IBM, Microsoft und deren Industriepartnern vor. Zur Formalisierung wählen wir den Abstract-State-Machine-Formalismus (kurz ASM), dessen theoretische Fundierung es uns erlaubt, die Semantik von BPEL4WS auf der selben Abstraktionsebene zur formalisieren, die in der informalen BPEL4WS-Spezifikation vorgegeben ist. Wir werden den inneren Aufbau der Sprache präzise, formal abbilden und damit eine intuitiv und anschaulich nachvollziehbare Entsprechung zwischen den Abläufen eines BPEL4WSProzesses gemäß der gegebenen informalen Semantik und unserer formalen Semantik aufzeigen. Dazu analysieren wir die Struktur von BPEL4WS und zeigen mit welchen Mitteln des ASM-Formalismus diese adäquat, formal erfasst werden und wie in ASM notierte Spezifikationen zu lesen sind. Hierzu werden wir beispielhaft ausgewählte, syntaktische Konstrukte von BPEL4WS nach unserem Ansatz formalisieren. Die vorliegende Arbeit bezieht sich auf die informale BPEL4WS-Spezifikation v1.1, veröffentlicht am 5. Mai 2003.

  

• Andreas Glausch. Abstract-State Machines - Eine Sammlung didaktischer Beispiele. Studienarbeit, Humboldt-Universität zu Berlin, February 2003.

  Abstract: Diese Studienarbeit versucht durch eine Vielzahl von Beispielen den Begriff Abstract-State Machine und sequenzieller Algorithmus didaktisch sinnvoll darzustellen. Es werden dabei sowohl Beispiele als auch Gegenbeispiele angegeben, um Umfang und Grenzen dieser Begriffe aufzuzeigen.

  

zurück zur Übersicht