Abstrakte Zustandsmaschine - Abstract state machine

In der Informatik ist eine abstrakte Zustandsmaschine ( ASM ) eine Zustandsmaschine , die auf Zuständen arbeitet , die beliebige Datenstrukturen sind ( Struktur im Sinne der mathematischen Logik , also eine nichtleere Menge zusammen mit einer Reihe von Funktionen ( Operationen ) und Beziehungen über die einstellen).

Überblick

Die ASM-Methode ist eine praxisnahe und wissenschaftlich fundierte Systems-Engineering- Methode, die die Brücke zwischen den beiden Enden der Systementwicklung schlägt:

  • das menschliche Verständnis und die Formulierung von realen Problemen ( Erfassung der Anforderungen durch genaue High-Level-Modellierung auf der Abstraktionsebene, die durch die gegebene Anwendungsdomäne bestimmt wird)
  • die Bereitstellung ihrer algorithmischen Lösungen durch Code-ausführende Maschinen auf wechselnden Plattformen (Definition von Designentscheidungen, System- und Implementierungsdetails).

Die Methode baut auf drei Grundkonzepten auf:

  • ASM : eine präzise Form von Pseudocode, der Finite State Machines verallgemeinert , um über beliebige Datenstrukturen zu arbeiten
  • Bodenmodell : eine strenge Form von Blaupausen, die als maßgebliches Referenzmodell für das Design dient
  • Verfeinerung : ein sehr allgemeines Schema für die schrittweise Instanziierung von Modellabstraktionen zu konkreten Systemelementen, das kontrollierbare Verbindungen zwischen den immer detaillierteren Beschreibungen in den aufeinanderfolgenden Phasen der Systementwicklung bereitstellt.

In der ursprünglichen Konzeption von ASMs führt ein einzelner Agent ein Programm in einer Abfolge von Schritten aus und interagiert möglicherweise mit seiner Umgebung. Dieser Begriff wurde erweitert, um verteilte Berechnungen zu erfassen , bei denen mehrere Agenten ihre Programme gleichzeitig ausführen.

Da ASMs Algorithmen auf beliebigen Abstraktionsebenen modellieren, können sie High-Level-, Low-Level- und Mid-Level-Ansichten eines Hardware- oder Softwaredesigns bereitstellen. ASM-Spezifikationen bestehen oft aus einer Reihe von ASM-Modellen, die mit einem abstrakten Bodenmodell beginnen und in sukzessiven Verfeinerungen oder Vergröberungen zu höheren Detaillierungsebenen übergehen.

Aufgrund der algorithmischen und mathematischen Natur dieser drei Konzepte können ASM-Modelle und ihre interessierenden Eigenschaften mit jeder rigorosen Form der Verifikation (durch Argumentation) oder Validierung (durch Experimentieren, Testen von Modellausführungen) analysiert werden .

Geschichte

Das Konzept der ASMs ist aufgrund Yuri Gurevich , die es zuerst als eine Möglichkeit , in der Mitte der 1980er Jahre vorgeschlagen auf der Verbesserung des Turing These , dass jeder Algorithmus wird simuliert durch eine entsprechende Turing - Maschine . Er formulierte die ASM-These : Jeder noch so abstrakte Algorithmus wird Schritt für Schritt von einem geeigneten ASM emuliert . Im Jahr 2000 axiomatisierte Gurevich den Begriff der sequentiellen Algorithmen und bewies die ASM-These für sie. Grob gesagt lauten die Axiome wie folgt: Zustände sind Strukturen, der Zustandsübergang umfasst nur einen begrenzten Teil des Zustands, und alles ist unter Isomorphismen von Strukturen invariant . (Strukturen können als Algebren angesehen werden , was den ursprünglichen Namen Evolving Algebras für ASMs erklärt.) Die Axiomatisierung und Charakterisierung sequentieller Algorithmen wurde auf parallele und interaktive Algorithmen ausgedehnt .

In den 1990er Jahren wurde durch eine Gemeinschaftsarbeit die ASM-Methode entwickelt, die ASMs für die formale Spezifikation und Analyse ( Verifikation und Validierung ) von Computerhardware und -software verwendet . Umfassende ASM-Spezifikationen von Programmiersprachen (einschließlich Prolog , C und Java ) und Designsprachen ( UML und SDL ) wurden entwickelt.

Eine ausführliche historische Darstellung findet sich an anderer Stelle.

Es stehen eine Reihe von Softwaretools für die ASM-Ausführung und -Analyse zur Verfügung.

Veröffentlichungen

Bücher

Verhaltensmodelle für Industriestandards

Werkzeuge

(in historischer Reihenfolge seit 2000)

Literaturverzeichnis

  • Y. Gurevich, Evolving Algebras 1993: Lipari Guide , E. Börger (Hrsg.), Specification and Validation Methods , Oxford University Press , 1995, 9-36. ( ISBN  0-19-853854-5 )
  • Y. Gurevich, Sequential Abstract State Machines capture Sequential Algorithms , ACM Transactions on Computational Logic 1(1) (Juli 2000), 77–111.
  • R. Stärk, J. Schmid und E. Börger, Java and the Java Virtual Machine: Definition, Verification, Validation , Springer-Verlag , 2001. ( ISBN  3-540-42088-6 )
  • E. Börger und R. Stärk, Abstract State Machines: A Method for High-Level System Design and Analysis , Springer-Verlag , 2003. ( ISBN  3-540-00702-4 )
  • E. Börger und A. Raschke, Modeling Companion for Software Practitioners , Springer-Verlag , 2018. ( ISBN  978-3-662-56639-8 , doi : 10.1007/978-3-662-56641-1 )

Verweise

Externe Links