EAV - Erste Analyse Versicherung

EAV ist ein prototypisches Werkzeug zum UML Model-Checking. Diese Software basiert auf dem MIT Alloy Analyzer 4 und USE - UML Specification Environment der Universität Bremen.

EAV benutzt UML Klassendiagramme (gegeben in der DSL von USE) als Eingabedaten und transformiert dieses Modell in Relationale Logik/Alloy. Das transformierte Modell wird dann an den Alloy Analyzer weitergereicht, der gültige UML Objektdiagramme zum gegebenen UML Klassendiagramm sucht.

Downloads:

Dokumente:

Kurz-Einführung:

Die Oberfläche und die Benutzung des Werkzeugs wird hier kurz anhand von Bildschirmfotos und einem einfachen Beispiel erläutert. Das Beispiel-Klassendiagramm besteht aus drei Klassen:

und den drei Assoziationen:

zwischen diesen Klassen.

        model USEexample1

        class Employee
        attributes
          name : String
          salary : Integer
        end

        class Department
        attributes
          name : String
          location : String
          budget : Integer
        end

        class Project 
        attributes
          name : String
          budget : Integer
        end
		
		-- assocations

        association WorksIn between
          Employee[*]
          Department[1..*]
        end

        association WorksOn between
          Employee[*]
          Project[*]
        end

        association Controls between
          Department[1]
          Project[*]
        end
      

Das UML Klassendiagramm wird textuell im Hauptfenster des EAV-Werkzeugs eingegeben (ähnlich zum Alloy Analyzer):

Oberfläche und Eingabe von Klassendiagrammen

Nach dem Ausführen des Modells werden dem Benutzer gültige Instanzen des entsprechenden Modells in einer zweiten Ansicht angezeigt. Über jede dieser gültigen Modellinstanzen kann mithilfe einer Schaltfläche iteriert werden (und somit auf Fehler in der Spezifikation des UML Klassendiagramms überprüft werden):

Gültige Instanz des Klassendiagramms

Des Weiteren ist es möglich Klasseninvarianten, sowie Vor- und Nachbedingungen für Klassenmethoden zu definieren. Damit können Methodenaufrufe auf bestimmten Klasseninstanzen simuliert werden.

Die folgende Erweiterung des Klassenmodells für die Klasse Department, sowie die Spezifikation einer entsprechenden Vor- und Nachbedingung können bspw. einen Klassenkonstruktor für die Klasse Department simulieren:

        ...
      
        class Department
        attributes
          name : String
          location : String
          budget : Integer
        operations
          NEW_Department()
        end

        ...

        constraints

        context Department::NEW_Department()
          post: self.oclIsNew() and self.budget=0
      

Der erste Teil der Nachbedingung self.oclIsNew() definiert, das zu einem gegebenen Zeitpunkt t das entsprechende Objekt noch nicht instanziiert ist (zum Zeitpunkt t), jedoch im darauffolgenden Zeitpunkt instanziiert ist (zum Zeitpunkt t+1). Also folgt daraus, dass die Methode NEW_Department() im Zeitpunkt t aufgerufen und durchgeführt wurde.

Das folgende Bildschirmfoto zeigt den Zustand des (leeren) UML Objektdiagramm zum Zeitpunkt t4.

UML Objektdiagramm zum Zeitpunkt t4

Zum Zeitpunkt t4 wurde die Methode NEW_Department() aufgerufen, sodass nun (in Zeitpunkt t5) ein Objekt der Klasse Department existiert:

UML Objektdiagramm zum Zeitpunkt t5

=========

Patrick Vogt, 31. Januar 2012