Abstrakte Zustandsmaschine

Eine abstrakte Zustandsmaschine (englisch Abstract State Machine (ASM), nicht zu verwechseln mit Algorithmic state machines, ehemals auch Evolving Algebra (EVA) genannt), ist in der Informatik ein Modell zur formalen, operationellen Beschreibung von Algorithmen. Anders als bei endlichen Automaten, deren Zustände lediglich Namen haben, sind die Zustände einer abstrakten Zustandsmaschine allgemeine mathematische Strukturen.

Im Gebiet des Übersetzerbaus dient das Modell der Beschreibung der Semantik des zu übersetzenden Programms, und es hilft sicherzustellen, dass die Semantik des zu übersetzenden Programms erhalten bleibt (Verifizierung). Bei der Entwicklung von Software im Allgemeinen erlaubt das Modell in der Analyse- und Entwurfsphase eine formale Beschreibung der funktionalen Anforderungen. Diese mathematische Herangehensweise verbessert beispielsweise Verifizierbarkeit und Wiederverwendbarkeit.

Beim Entwurf komplexer Schaltwerke wird auch auf die Formalisierung mit abstrakten Zustandsmaschinen zurückgegriffen.

Ursprung

Der Erfinder des Modells ist Yuri Gurevich von Microsoft.[1] Der in Italien an der Universität Pisa ansässige Informatiker Egon Börger erforscht Methoden zur Anwendung abstrakter Zustandsmaschinen bei Entwurf und Analyse von Hardware- und Softwaresystemen.[2]

Mittlerweile gibt es unterschiedliche Implementierungen des Modells, sodass Entwurf und Interpretation von Programmen für die abstrakten Maschine rechnergestützt erfolgen kann.

Literatur

  • Yuri Gurevich, Philipp W. Kutter, Martin Odersky, Lothar Thiele (Hrsg.): Abstract State Machines. Theory and Applications. Springer, Berlin u. a. 2000, ISBN 3-540-67959-6 (Lecture Notes in Computer Science 1912).

Quellen

  1. ↑ A New Thesis, Abstracts, American Mathematical Society, Vol. 6, No. 4 (August 1985), page 317, abstract 85T-68-203
  2. ↑ E. Börger, R. Stärk: Abstract State Machines: A Method for High-Level System Design and Analysis, Springer-Verlag, 2003. (ISBN 3-540-00702-4)

Weblinks

Informationen

  • Abstract State Machines – Definition, Beispiele und Gegenbeispiele (19 Seiten PDF; 166 kB)
  • Abstract State Machines – kurze Erklärung, ausführliche Definition (englisch, 12 Seiten PDF; 372 kB)
  • Verifikation von Übersetzern mit ASMs – Folien (165 Seiten PDF; 2,2 MB)
  • Verifikation von Übersetzern mit ASMs – Textversion (16 Seiten PDF; 237 kB)
  • Abstract State Machines – sortierte Materialien (englisch)
  • ASM Workshops – Veranstaltungen zum Thema (englisch)

Implementierungen

  • (Abstract State Machine Language) – von Yuri Gurevich entworfene Sprache
  • XASM (Anlauff's eXtensible ASMs) – erweiterbare, minimale Sprache (englisch)
  • Das CoreASM Projekt – Verifikation verteilter und eingebetteter Systeme (englisch)
  • TASM (Timed Abstract State Machine Language and Toolset) (Memento vom 17. April 2009 im Internet Archive) – Erweiterungen zur Beschreibung nicht-funktionaler Eigenschaften (englisch)
  • ASMETA Projekt – ASM-Metamodell nach den Richtlinien der modellgetriebenen Softwareentwicklung für Interoperabilität zwischen ASM-Sprachen (englisch)