Abstract

Diese Bachelorarbeit untersucht, inwieweit sich formal spezifizierte Abstrakte Zustandmaschinen (engl.: abstract state machines, ASMs) in ausführbaren Java Code übersetzen lassen. Hierdurch soll eine Einschätzung gegeben werden, inwieweit eine 100% Modell-getriebene Entwicklung sinnvoll ist. Dies wird am Beispiel von Conways „Game of Life“ gezeigt: Zunächst wird das Modell in der ASM- Sprache CoreASM definiert, dann mit Hilfe eines Compilers in ausführbare Java Klassen umgewandelt.

Diese Arbeit kommt zu dem Schluss, dass die Abgrenzung zwischen Ground Model und Geschäftslogik extrem wichtig ist: Während das Ground Model (im Beispiel: die Petrischale) aufgrund fehlender Strukturen (z.B. Felder) in CoreASM kaum umgesetzt werden kann, ist die Geschäftslogik (im Beispiel:

Transformationsverhalten der Zellen) leicht zu definieren und lässt sich auch im Nachhinein auf eine für den Compiler erkennbare Weise verändern. Diese Erkenntnis hilft dabei das Konzept der Abstrakten Zustandsmaschinen in den Zusammenhang der modellgetriebenen Entwicklung einzuordnen: Die formale Spezifikation der Geschäftslogik lässt sich gut mit ASMs bewerkstelligen, während das Ground Model besser klassisch programmiert werden sollte.

Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 2

Inhaltsverzeichnis

1  Einleitung  5

1.1  Motivation  5

1.2  Abstract State Machines.  5

1.2.1  Einführung.  5

1.2.2  Typen von ASMs  9

1.2.3  Das Game Of Life  9

1.2.4  Geschäftslogik und Grundmodell.  10

1.2.5  Der Multi-Core Ansatz.  11

1.2.6  Überblick.  11

2  Das CoreASM Modell.  13

2.1  Einführung CoreASM  13

2.2  Das Game Of Life in CoreASM.  13

2.2.1  Grundform.  13

2.2.2  Variation 1: Randzellen.  16

2.2.3  Variation 2: runde Petrischale  17

2.3  Reduktion auf die Geschäftslogik  18

2.3.1  Zelle.casm  19

2.3.2  Conwayzelle.casm.  19

2.3.3  Keimzelle.casm  20

2.3.4  Randzelle.casm.  20

3  Von CoreASM zu Java: Der Compiler  21

3.1  Aufrufende Klasse.  21

3.2  Die Klasse compiler.java.  22

3.3  Adaptivität bei veränderten Transformationslogiken.  26

4  Das Java Programm.  27

4.1  Grundmodell.  27

4.1.1  GoL Aufruf.java  27

4.1.2  Petrischale.java.  28

4.1.3  Rundschale.java.  34

4.1.4  Zustand.java  36

4.2  Geschäftslogik.  37

4.2.1  Übersicht  37

4.2.2  Zelle.java (abstract)  38

4.2.3  Conwayzelle.java  39

4.2.4  Keimzelle.java.  40

4.2.5  Randzelle.java  41

4.3  Alternative Umsetzung mittels eines Arbitrators  41

4.3.1  Die aufrufende Klasse Main.java (Arbitrator-Version)  42

4.3.2  Zustand.java  46

4.3.3  Die Klasse MyArbitrator.java  47

4.3.4  Das Interface MyBehavior.java.  48

4.3.5  Mögliche Verhaltensweisen einer Zelle.  49

4.3.6  Die Klasse Zelle.java (Arbitrator-Version)  54

5  Ergebnis.  57

5.1  Zusammenfassung.  57

5.2  Schlussfolgerungen  57

Literaturverzeichnis.   58

Compilierszenarios  für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen  3

Abbildungsverzeichnis   

Abbildung  1: Aktualisierungsschema einer ASM  

Abbildung  2: Zustandsübergänge einer ASM  

Abbildung  3: Funktions-, Relations- und Lokationsklassen.  

Abbildung  4: ASM Typen  

Abbildung  5: Systemarchitektur  

Abbildung  6: Quelltext CoreAS-MProgramm GameOfLife.casm  

Abbildung  7: Quelltext CoreAS-MProgramm GameOfLife mit Randzellen -  

Intialisierung   

Abbildung  8: Quelltext CoreAS-MProgramm GameOfLife mit Randzellen - Regel  

r  Randzelle  

Abbildung  9: Quelltext CoreAS-MProgramm GameOfLife mit runder Petrischale  

Abbildung  10: Quelltext CoreAS-MProgramm zelle.casm  

Abbildung  11: Quelltext CoreAS-MProgramm conwayzelle.casm  

Abbildung  12: Quelltext CoreAS-MProgramm keimzelle.casm.  

Abbildung  13: Quelltext CoreAS-MProgramm randzelle.casm  

Abbildung  14: Quelltext der Klasse Compiler Aufruf.java  

Abbildung  15: Quelltext der Klasse Compiler.java.  

Abbildung  16: UML-Diagramm GoL Aufruf.java.  

Abbildung  17: Quelltext der Klasse GoL Aufruf.java.  

Abbildung  18: UML-Diagramm Petri- und Rundschale  

Abbildung  19: Quelltext der Klasse Petrischale.java  

Abbildung  20: Quelltext der KlasseRundschale.java  

Abbildung  21: UML-Diagramm Zustand.java  

Abbildung  22: Quelltext der Aufzählung Zustand.java  

Abbildung  23: UML-Diagramm Business Logic  

Abbildung  24: Quelltext der abstrakten Klasse Zelle.java.  

Abbildung  25: Quelltext der Klasse Conwayzelle.java.  

Abbildung  26: Quelltext der Klasse Keimzelle.java.  

Abbildung  27: Quelltext der Klasse Randzelle.java  

Abbildung  28: Quelltext Arbitrator-Version: Main.java  

Abbildung  29: Quelltext Arbitrator-Version: Petrischale.java  

Abbildung  30: Quelltext Arbitrator-Version: enum Zustand.java  

Abbildung  31: Quelltext Arbitrator-Version: MyArbitrator.java.  

Abbildung  32: Quelltext Arbitrator-Version: interface MyBahavior.java  

Abbildung  33: Quelltext Arbitrator-Version: Zelle.java  

Abbildung  34: Quelltext Arbitrator-Version: Bleibt2.java  

Abbildung  35: Quelltext Arbitrator-Version: Lebt2.java  

Abbildung  36: Quelltext Arbitrator-Version: Lebt3.java  

Abbildung  37: Quelltext Arbitrator-Version: Keim1.java  

Abbildung  38: Quelltext Arbitrator-Version: Stirbt.java.  

Abbildung  39: Quelltext Arbitrator-Version: Rand.java  

Compilierszenarios  für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen  

1 Einleitung

1.1 Motivation

Die vorliegende Bachelorarbeit untersucht, ob ein 100% Modell-getriebener Ansatz auf Basis von Abstrakten Zustandsmaschinen (engl.: Abstract State Machines, ASMs) für die Implementierung komplexer Systeme sinnvoll ist. Das Compilierszenario wird in vier Schritte aufgeteilt:

- Modellierung der Geschäftslogik als ASMs

- Syntaktische Überprüfung des Modells in CoreASM

- Übersetzung des Modells in eine übersetzbare Java-Klasse

- Einbettung der Klasse in das Grundmodell (Ground Model), das aus beliebig vielen anderen Java Klassen bestehen kann. Anschließend werden an dem Modell Veränderungen vorgenommen, deren Auswirkungen auf das Java-Programm deutlich gemacht werden sollen. Als Grundlage dienen die Arbeiten von Prof. Börger, sowie die Bachelorarbeit von Wolfgang Bühler, die sich mit „der Tauglichkeit von ASM als Kern der subjektorientierten Modellierung“ beschäftigt, und in diesem Rahmen bereits eine CoreASM Version des auch in dieser Arbeit verwendeten Beispiels (Conways Game of Life) vorstellt.

Die genannten Arbeiten werden durch die Vorliegende derart ergänzt, dass hier die Umsetzung der Geschäftslogik vollständig ohne manuelle Programmierung untersucht wird. Außerdem wird die Variationsfähigkeit einer 100% modellgetriebenen Entwicklung aufgezeigt.

Besonderes Augenmerk wird auf die Umsetzung des subjektorientierten Paradigmas für Multi-Core Maschinen gelegt.

Abschließend wird ein Ausblick gegeben, inwieweit sich die fallspezifisch gewonnenen Erkenntnisse auf größere Modelle und Entwicklungsszenarios übertragen lassen.

1.2 Abstract State Machines

1.2.1 Einführung

1985 entwickelte Yuri Gurevich das Konzept der abstrakten Zustandsmaschinen. [Gure93] Dieses Konzept liefert ein Modell zur formalen, operationellen Beschreibung von Algorithmen. Mit Hilfe abstrakter Zustandsmaschinen können Algorithmen auf einem beliebigen Abstraktionsniveau beschrieben werden. Dies ermöglicht auch komplexe Konzepte und Modelle zu integrieren.

Somit ermöglichen ASMs, jeden Algorithmus in einer bestimmten Abstraktionsebene als abstrakte Zustandsmaschine zu beschreiben, die den Algorithmus schrittweise simuliert.

Abstrakte Zustandsmaschinen bedienen sich der Ausdrucksstärke mathematischer Algebren um jeden Zustand des Systems als Algebra zu beschreiben. Eine Algebra wird zusammengesetzt aus einem (nicht leeren) Universum und einer Menge von Funktionen. Die Funktionen werden in dem Universum definiert.

Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 5

Mithilfe einer Algebra können komplizierte Strukturen beschrieben werden. Durch Darstellung von Abbildungen, Relationen und Mengen können auch komplexere Datenstrukturen wie Datenbanken, Graphen oder Körper abgebildet werden. [Kohl09], [Glau05]

Eine ASM transformiert Zustände schrittweise mit Hilfe von Regeln. Der Zustand einer ASM entspricht der klassischen mathematischen Struktur, die Daten als abstrakte Datentypen (ADT) betrachtet.

Universen (auch: Domänen) sind Mengen von Elementen. Jede Element-Kategorie bildet ein eigenes Universum. Darüber werden mathematische Funktionen („Operationen“) sowie Attribute und Relationen („Eigenschaften“) definiert. Eigenschaften werden als charakteristische Funktionen aufgefasst, die Konstanten als 0-stellige Funktionen behandeln. Partielle Funktionen werden in totale Funktionen umgeformt. Dies erreicht man durch Uminterpretation von f(x)=undef zu fixem Spezialwert undef für f(x) undefiniert.

Die Regeln zur Zustandstransformation heißen Transformationen. Diese entstehen durch eine endliche Anzahl von Aktualisierungen. Die Grundform einer Transitionsregel sieht folgendermaßen aus: if Condition then Updates

Hierbei steht Condition für einen booleschen Ausdruck. Da Updates nur ausgeführt wird, wenn die Condition den Wert „true“ annimmt, nennt man die Condition auch guard.

Updates repräsentiert eine Menge von Aktualisierungen, die Zuweisungen mit folgender Form darstellen: f (t1…tn) := t

Wird die Aktualisierung ausgeführt, so ändert sich der Wert der aufgerufenen Funktion f an dem entsprechenden Argument (t1…tn) auf den angegeben Wert t. [BöSt03]

Die folgende Grafik verdeutlicht den Ablauf eines Aktualisierungsschrittes.

Abbildung 1: Aktualisierungsschema einer ASM

Quelle: [BöSt03]

Die durch die linke Seite der Gleichung angegebene Verbindung aus Funktion f und Argument (t1…tn) wird als location (engl: Zuordnung) bezeichnet. Im ASM-Konzept werden locations zur Bildung von Objekt-Containern bzw. Speichereinheiten genutzt.

Eine Aktualisierung ist die Kopplung von location und Wert (loc,v). Der Ablauf einer ASM geschieht in mehreren Schritten. In jedem Schritt werden die guards geprüft. Falls diese wahr sind, so werden die entsprechenden Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 6

Aktualisierungen durch Transitionsregeln ausgeführt. Der nächste Zustand wird durch die Ausführung der Aktualisierungen erreicht, wenn diese konsistent sind.

Abbildung 2: Zustandsübergänge einer ASM

Ein Algorithmus wird durch die (un-)endliche Folge von Zuständen S n berechnet. S ⁰ beschreibt den Startzustand. Eine ASM iteriert ihre Berechnungsschritte und ist somit ein aktives System. Sie ist beendet, wenn die Menge der Aktualisierungen eines Schrittes leer ist. [BöSt03]

Funktionen, Relationen und locations einer ASM können in verschiedene Klassen eingeteilt werden. Die folgende Grafik gibt einen Überblick über die Aufteilung der Klassen und wird im Weiteren genauer erklärt.

Abbildung 3: Funktions-, Relations- und Lokationsklassen

Quelle: [BöSt03]

Zunächst kann man nach basic- und derived- Funktionen unterscheiden. Die basic-Funktionen werden weiter in statische und dynamische Funktionen aufgeteilt:

- Statische Funktionen behalten ihren Wert während des gesamten ASM-Ablaufs, und sind somit unabhängig von dem aktuellen Zustand der ASM.

- Dynamische Funktionen sind durch Aktualisierungen während des ASM-Ablaufs veränderlich. Diese Aktualisierungen können von der Umgebung oder aus der konkreten ASM vorgenommen werden. Somit ist für dynamische Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 7

Funktionen kein fester Wert definierbar, sondern die Werte sind zustandsabhängig. Andere ASMs als die, die die Funktion enthält, zählen ebenfalls zur Umgebung und können somit Werte anderer ASMs verändern. Die dynamischen Funktionen sind weiter in controlled-, monitored- (in-), shared- (interaction-)und out-Funktionen aufteilbar:

- Controlled-Funktionen können ausschließlich durch die Regeln der ASM aktualisiert werden.

- Monitored-Funktionen (auch: in-Funktionen) hingegen sind für die ASM nur lesbar, nicht aber veränderbar. Änderungen können nur von der Umgebung vorgenommen werden.

- Shared-Funktionen (auch: interaction-Funktionen) sind für ASM und Umgebung sowohl les- als auch aktualisierbar.

- Die out-Funktion ist das Gegenstück zur in-Funktion, hier darf die Umgebung nur lesen, während die ASM auch Rechte zum Aktualisieren besitzt. Die derived-Funktionen (abgeleiteten Funktionen) lassen sowohl für ASM als auch Umgebung nur Lesezugriff zu. Ihre Werte werden durch ein festes Schema von anderen Funktionen abgeleitet.

Die Menge der Funktionen und Regeln einer ASM bildet die so genannte Signatur. Die Definition einer abstrakten Zustandsmaschine geschieht durch Angabe ihrer Signatur, ihres Startzustandes sowie der so genannten main rule. Ein Agent führt das ASM Programm aus.

Pseudocode ermöglicht die leicht verständliche Notation der ASM, ohne auf präzise mathematische Semantik zu verzichten. [BöSt03] ASMs können auch mathematisch präzise beschrieben werden. Da diese Bachelorarbeit aber die Umsetzung von ASMs untersucht, wird für detailliertere Ausführungen auf die Arbeiten von Prof. Börger verwiesen, welche sich in aller Ausführlichkeit mit den Grundprinzipien und Definitionen von abstrakten Zustandsmaschinen beschäftigen.

Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 8

1.2.2 Typen von ASMs

Abstract State Machines lassen sich in mehrere Typen aufteilen. Die folgende Grafik gibt einen Überblick über die verschiedenen Typen.

Abbildung 4: ASM Typen

Als Grundform einer abstrakten Zustandsmaschine ist die Basic ASM zu sehen. Sie bietet ein geringes Abstraktionslevel, um die Vorgänge innerhalb einer ASM abzubilden (white box).

Durch Komposition und Iteration von Operatoren (zu Beispielen siehe Tab. 1) und den Aufruf von Untermaschinen wird die Basic ASM zur Turbo ASM erweitert. Diese ermöglicht ein höheres Abstraktionslevel und fungiert somit als black box. Wird zum Design großer Systeme eine Modularität des Modells benötigt, so verwendet man mehrere Agenten, die alle eine eigene Basic- oder Turbo ASM ausführen. Dies bezeichnet man als Multi-Agenten ASM, welche sich in die synchronen Multi-Agenten ASMs (globaler Taktgeber) und die asynchronen Multi-Agenten ASMs (eigenständige Agenten) aufteilen.

Die vorgestellte Einteilung sowie die Inhalte der Kapitel 1.2.1. und 1.2.2. basieren auf [BöSt03].

1.2.3 Das Game Of Life

Das Spiel des Lebens (engl.: Game of Life) ist ein vom Mathematiker John Horton Conway 1970 entworfenes System, basierend auf einem zweidimensionalen zellulären Automaten.

Die Automaten (auch: Zellen) können zwei verschiedene Zustände (meist: „lebendig“ und „tot“) annehmen. Die Simulation verläuft in Generationen, wobei die Zellen stets gleichzeitig ihren neuen Zustand einnehmen. Dieser Zustand entscheidet sich anhand der Anzahl der lebenden Nachbarn (ein Nachbar ist eine Zelle in einem der acht angrenzenden Nachbarfelder) der vorangegangenen Generation und wird in Conways Grundform nach folgenden Regeln festgelegt:

- Zellen mit drei lebenden Nachbarn sind in der nächsten Generation am Leben.

Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 9

- Zellen mit zwei lebenden Nachbarn behalten ihren Zustand in der nächsten Generation.

- Zellen mit weniger als zwei oder mehr als drei Nachbarn sind in der nächsten Generation tot.

1.2.4 Geschäftslogik und Grundmodell

Die in dieser Arbeit vorgestellte Game of Life Version beruht auf der Überlegung die Geschäftslogik (engl.: Ground Model) vom Grundmodell (engl.: Business Logic) zu trennen.

Abbildung 5: Ground Model und Business Logic

Zur Verdeutlichung betrachte man Abbildung 5: Ein Akteur (muss nicht zwingend ein Mensch sein, wird hier aber als Person dargestellt) agiert in einem abgeschlossenen Aktionsraum. Jegliche Interaktion mit der Außenwelt ist durch Vor- und Nachbedingungen geregelt während die eigentliche Aktion des Akteurs nicht fest vorgeschrieben ist.

Dies soll anhand eines Beispiels verdeutlicht werden:

Betrachten wir einen Sachbearbeiter in einem Großraumbüro, dessen Aufgabe darin besteht Formulare auszufüllen.

Dieser Sachbearbeiter sitzt an seinem Schriebtisch, bekommt leere Formulare gemailt, muss diese ausfüllen und faxt den fertigen Antrag zur nächsten Bearbeitungsinstanz und heftet den Ausdruck ab.

Bereits an diesem einfachen Beispiel lässt sich der Gedanke von Grundmodell und Geschäftslogik verdeutlichen.

Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 10

Das Empfangen eines Antrags unterliegt gewissen Vorbedingungen (der Antrag muss leer sein, der Antrag muss elektronisch vorliegen etc.), ebenso wie das (weiter-) Senden Bedingungen unterliegt (der Antrag muss ausgefüllt sein, in Papierform vorliegen etc.).

Die eigentliche Aktion des Sachbearbeiters jedoch kann dieser frei bestimmen: druckt er den Antrag erst aus und füllt ihn von Hand aus, füllt er ihn am PC aus und druckt erst dann, in welcher Reihenfolge füllt er ihn aus,…). Dies ist die wertschöpfende Aktion des Akteurs, seine Geschäftslogik. Diese bedarf aber gewissen Rahmenbedingungen: Der Sachbearbeiter benötigt Drucker, Fax, Schreibtisch, und ggf. sonstige Arbeitsmittel um seine Aufgabe auch wirklich erfüllen zu können. Diese Rahmenbedingungen bilden das Grundmodell (engl.: ground model), das in Abbildung 5 durch eine „Schneekugel“ dargestellt wird.

1.2.5 Der Multi-Core Ansatz

Eine Besonderheit der in dieser Arbeit vorgestellten Version des Game of Lifes besteht darin, dass jede Zelle durch einen eigenen Thread realisiert wird (vgl. hierzu Kapitel 4.2.2).

Ein Thread ist eine sequentielle Abfolge von Befehlen, Java ist jedoch in der Lage mehrere Threads gleichzeitig auszuführen, wodurch ein paralleler Programmablauf erzeugt werden kann. Für genauere Informationen zu Threads wird auf die Java API verwiesen.

Dieser Ansatz beruht auf dem Versuch, der zunehmenden Zahl moderner Rechnerkerne gerecht zu werden, um durch Arbeitsteilung eine bessere Performance zu erzielen.

1.2.6 Überblick

Die folgende Grafik gibt einen Überblick über die Gesamtsystemarchitektur und wird im Folgenden näher erläutert.

Abbildung 6: Systemarchitektur

Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 11

Das Ground Model besteht aus den Klassen GoL_Aufruf (vgl. Kapitel 4.1.1), Petrischale (vgl. Kapitel 4.1.2), der davon erbenden Klasse Rundschale (vgl. Kapitel 4.1.3) sowie dem Aufzählungstyp Zustand (vgl. Kapitel 4.1.4). Diese Klassen sind direkt in Java implementiert.

In CoreASM werden die Klassen Zelle (vgl. Kapitel 2.3.1), Conwayzelle (vgl. Kapitel 2.3.2), Keimzelle (vgl. Kapitel 2.3.3) und Randzelle (vgl. Kapitel 2.3.4) der Business Logik definiert.

Diese werden durch den Compiler (vgl. Kapitel 3) in die gleichnamigen Javaklassen (vgl. Kapitel 4.2.2 bis 4.2.5) übersetzt und bilden die Geschäftslogik des Spiels. Die Funktionsweisen der einzelnen Klassen werden in den genannten Kapiteln beschrieben.

Compilierszenarios für Abstrakte Zustandsmaschinen bei Multi-Core Anwendungen 12