eav - early analysis verification

EAV is a prototype tool for UML model checking. The software is based on the MIT Alloy Analyzer 4 and the USE - UML Specification Environment of the University Bremen.

It uses an UML class diagram given in the USE domain specific language as input data and transforms the given UML class diagram into relational logic/Alloy. The transformed model is then passed to Alloy for finding valid UML object diagrams for the UML class diagram. The drawing module of Alloy was manipulated for drawing real UML object diagrams.

download:

documents:

short introduction:

The frontend and the usage of the tool is described using screenshots and the following example. The example contains three classes:

and three associations:

between these classes.

        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

        -- associations

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

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

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

The UML class diagram will be textually specified in the main window of EAV (similar to the Alloy Analyzer):

Demonstration of frontend and input dsl

After executing the model for finding valid UML object diagrams a second view is shown where all fulfilling instances are shown and can be iterated separately:

Fulfilling instance for the UML class diagram

Furthermore it is possible to specifiy class invariants or pre- and post conditions for operations and to simulate the call of operations on different objects.

The following extension for the class Department and a constraint which defines the pre and post conditions can simulate a constructor for the class Department:

        ...
      
        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
      

The first part of the post condition self.oclIsNew() defines for a time t that the object was not alive in time t and that is alive in time t+1. So the operation NEW_Department() was called in time t.

The following image shows the state of an empty UML object diagram in time t4.

UML object diagram at time t4

In time t4 the operation NEW_Department() is called such that one object of class Department is instantiated

UML object diagram at time t5

=========

Patrick Vogt, 31th January 2012