KIELER Project


Get me back to the home page!

Page tree

Versions Compared

Old Version 2

changes.mady.by.user Unknown User (cds)

Saved on

compared with

New Version Current

changes.mady.by.user Unknown User (cmot)

Saved on

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.
Comment: Migrated to Confluence 5.3
Warning

This page is not migrated yet. Try the old wiki until someone fills me with content.

Responsible:

  • Christian Motika
    • Jens Schönborn
    Panel
    titleProject Overview
    borderStyledashed
    Panel
    borderStyledashed
    titleProject Overview

    Responsible:

    UML State Machine Simulation and Model Checking with Maude

    Topics

    Table of Contents
    maxLevel2
    minLevel2

    ...

    Standalone UML Maude

    You can download a standalone version of the UML Maude implementation here: UML_SM_Maude.zip

    ...

    Overview

    This subproject integrates the  Papyrus MDT UML State Machine editor into KIELER. It also integrates the  Maude System into Eclipse/KIELER and additionally uses KIELER technologies and a special generic Maude state machine backend to offer simulation and model checking based on state machines modeled in Papyrus. The editor, the DataTable and KIEM are used as a GUI and I/O facility for modeling, simulating and model checking.

    ...

    Installation

    1. Download and install the  Maude System

    2. Download and unpack the  KIELER Rich Client Applications nightly builds

    3. Install Papyrus
      • Start the KIELER RCA and klick on the Install Modeling Components button
        Image Added

      • Select the Papyrus MDT Tools and install them into the KIELER RCA
        Image Added

      • Eclipse should now ask you to restart the KIELER RCA. Click the Restart Now button.

    4. Finally, install KIELER UML Simulation and Model Checking components
      • Click on Help/Install New Software....
        Image Added

      • Choose the KIELER nightly -  http://rtsys.informatik.uni-kiel.de/~kieler/updatesite/nightly Update Site from the drop down list.

      • Select the KIELER Bridge to Papyrus and UML Simulation feature and continue installation with Next. If that does not work you might have an older version of the nightly build and you should select the whole [x] KIELER category for installation/update.
        Image Added

      • Eclipse should again ask you to restart the KIELER RCA. Click the Restart Now button.

    5. Congratulations! You have now installed everything you need to simulate and model check UML state machines with KIELER.

    ...

    Simulating and Model Checking of UML State Machines

    1. Close the Outline Eclipse View because it may produce errors with this early version of Papyrus MDT.
    2. Create an empty (normal) Eclipse Project (File/New/Project) and give it some name, e.g., test.
      Image Added

    3. Create a Papyrus Diagram in this new project:
      • File/New/Other

      • Select Papyrus/Papyrus Model
        Image Added

      • Give it a name, e.g., model.di.
        Image Added

      • Select [x] UML as the Diagram Language.
        Image Added

      • Select [x] UML State Machine as the Diagram Kind.
        Image Added

    4. You should now see a plain UML state machine diagram editor pane where you can freely model your state machine.
      Image Added

    5. For simulation and model checking you should modify the DataComponents in the Execution Manager View as seen on the above screen shot. You can simply remove the other components. While in the Execution Manger View you can press the Save button to save this setting for later usage in your project's folder. Give it some name, e.g., model.execution.
      Image Added

    6. During modeling you may want to use our integrated automatic layout feature.
      Image Added

      Image Added

    Simulating

    1. Deactivate the DataComponent for model checking as shown below and validate that the path to the Maude executable is set correctly.
      Image Added

    2. You must save your changes to the diagram before you can simulate it.

    3. You may want to inspect the output of Maude in the Console Eclipse View.

    4. Start the simulation by pressing the Step or Run button of the Execution Manager View.
    5. The state machine's Maude representation will be generated in your projects folder.
    6. Now you can set (input) events and inspect (output) actions in the DataTable Eclipse View.
      Image Added

    7. You can now you the Step button to perform a simulation (run-to-completion) step or use the Run/Pause buttons.

    ...

    Model Checking

    1. Deactivate the DataComponent for simulation as shown below and validate that the path to the Maude executable is set correctly.
      Image Added

    2. Set your desired model checking term in the properties of the model check DataComponent.
    3. You must save your changes to the diagram before you can model check it.

    4. You may want to inspect the output of Maude in the Console Eclipse View.

    5. Start the simulation by pressing the Step button of the Execution Manager View.
    6. The state machine's Maude representation will be generated in your projects folder.
    7. Now you can set (input) events and inspect (output) actions in the DataTable Eclipse View.
      Image Added

    8. When you now click on Step again, model checking will be performed and you will be prompted the result.

    9. If there is a counter example, then you can now use subsequent clicks on Step to inspect it.

    ...