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
- AsmBook: Egon Börger , Robert Stärk. Abstrakte Zustandsautomaten: Eine Methode für das Design und die Analyse von High-Level-Systemen
- JBook: R.Stärk, J.Schmid, E.Börger. Java und die Java Virtual Machine: Definition, Verifizierung, Validierung
- Verfahren/Zeitschriftenausgaben (seit 2000)
- 2008: Springer LNCS 5238 Abstrakte Zustandsmaschinen, B und Z
- 2007: J.UCS Sonderausgabe mit ausgewählten Papieren von ASM'07
- 2006: Springer LNCS 5115 Rigorous Methods for Software Construction and Analysis , ASM und B Dagstuhl Seminar
- 2005: Fundamenta Informatica Special Issue mit ausgewählten Papers von ASM'05 ( elektronischer Proceeding )
- 2004: Springer LNCS 3052 Abstrakte Zustandsmaschinen 2004
- 2003: Springer LNCS 2589 Abstrakte Zustandsmaschinen 2003: Fortschritte in Theorie und Praxis
- 2003: TCS-Sonderheft mit ausgewählten Papieren von ASM'03
- 2002: Dagstuhl-Seminarbericht Theorie und Anwendungen abstrakter Zustandsmaschinen
- 2001: J.UCS 7.11 Sonderausgabe mit ausgewählten Papieren von ASM'01
- 2000: Springer LNCS 1912 Abstrakte Zustandsmaschinen: Theorie und Anwendungen
- Vergleichende Fallstudien mit ASM-Beiträgen
- Dampfkesselsteuerung: Spezifikation Fallstudie , Springer LNCS 1165
- Produktionszelle: Fallstudie zur Softwareentwicklung , ASM-Modell
- Railcrossing: Formale Methoden für Echtzeit-Computing , ASM-Modell
- Lichtsteuerung: Fallstudie Requirements Engineering , Dagstuhl-Seminar
- Rechnungsstellung: Fallstudie zur Anforderungserfassung
Verhaltensmodelle für Industriestandards
- OMG für BPMN (Version 2006): Springer LNCS 5316
- OASIS für BPEL: IJBPMI 1.4 (2006)
- ECMA für C#: "Eine hochrangige modulare Definition der Semantik von C♯" doi : 10.1016/j.tcs.2004.11.008
- ITU-T für SDL-2000: Formale Semantik von SDL-2000 und Formale Definition von SDL-2000 - Kompilieren und Ausführen von SDL-Spezifikationen als ASM-Modelle
- IEEE für VHDL93: E. Boerger, U. Glaser, W. Mueller. Formale Definition eines abstrakten VHDL'93 Simulators von EA-Machines. In: Carlos Delgado Kloos und Peter T.~Breuer (Hrsg.), Formal Semantics for VHDL , S. 107–139, Kluwer Academic Publishers, 1995
- ISO für Prolog: "Eine mathematische Definition des vollständigen Prologs" doi : 10.1016/0167-6423(95)00006-E
Werkzeuge
(in historischer Reihenfolge seit 2000)
- ASMETA, das Abstract State Machine Metamodel und sein Toolset auf SourceForge
- Asml
- CoreASM , verfügbar bei CoreASM, einer erweiterbaren ASM-Ausführungs-Engine
- AsmGofer auf Archive.org
- Das Open-Source-Projekt XASM auf SourceForge
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 )