# Wiki source code of UML State Machine Simulation/Model Checking with Maude

Last modified by Richard Kreissig on 2023/09/14 10:32
Export
Office Formats
Export as PDF Export as ODT Export as RTF
Other Formats

Select the pages to export:

select all/ none

Legend:
  Created Page
  Modified Extension Page
  Clean Extension Page

Export as HTML

Show last authors

author | version | line-number | content
--- | --- | --- | ---
|  | 1 | == Project Overview ==
|  | 2 | Responsible:
|  | 3 |
|  | 4 | * [[Christian Motika>>url:http://www.informatik.uni-kiel.de/rtsys/kontakt/cmot/||shape="rect"]]
|  | 5 | * Jens Schönborn
|  | 6 |
|  | 7 | = UML State Machine Simulation and Model Checking with Maude =
|  | 8 |
|  | 9 | ==== Topics ====
|  | 10 |
|  | 11 |
|  | 12 |
|  | 13 | {{toc maxLevel="2" minLevel="2"/}}
|  | 14 |
|  | 15 | ----
|  | 16 |
|  | 17 | == Standalone UML Maude ==
|  | 18 |
|  | 19 | You can download a standalone version of the UML Maude implementation here:[[attach:UML_SM_Maude.zip]]
|  | 20 |
|  | 21 | ----
|  | 22 |
|  | 23 | == Overview ==
|  | 24 |
|  | 25 | This subproject integrates the [[(% class="icon" %) (%%)Papyrus MDT>>url:http://www.eclipse.org/modeling/mdt/papyrus/||shape="rect" class="ext-link"]] UML State Machine editor into KIELER. It also integrates the [[(% class="icon" %) (%%)Maude System>>url:http://maude.cs.uiuc.edu/||shape="rect" class="ext-link"]] 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>>url:http://rtsys.informatik.uni-kiel.de/confluence/pages/viewpage.action?pageId=328095||shape="rect"]] are used as a GUI and I/O facility for modeling, simulating and model checking.
|  | 26 |
|  | 27 | ----
|  | 28 |
|  | 29 | == Installation ==
|  | 30 |
|  | 31 | 1. Download and install the [[(% class="icon" %) (%%)Maude System>>url:http://maude.cs.uiuc.edu/download/||shape="rect" class="ext-link"]]
|  | 32 |
|  | 33 | 1. Download and unpack the [[(% class="icon" %) (%%)KIELER Rich Client Applications nightly builds>>url:http://rtsys.informatik.uni-kiel.de/confluence/%7Ekieler/files/nightly/||shape="rect" class="ext-link"]]
|  | 34 |
|  | 35 | 1. Install Papyrus
|  | 36 | 1*. Start the KIELER RCA and klick on the //Install Modeling Components// button
|  | 37 | [[image:attach:uml-install1.jpg]]
|  | 38 |
|  | 39 | 1*. Select the Papyrus MDT Tools and install them into the KIELER RCA
|  | 40 | [[image:attach:uml-install2.jpg]]
|  | 41 |
|  | 42 | 1*. Eclipse should now ask you to restart the KIELER RCA. Click the //Restart Now// button.
|  | 43 |
|  | 44 | 1. Finally, install KIELER UML Simulation and Model Checking components
|  | 45 | 1*. Click on //Help/Install New Software...//.
|  | 46 | [[image:attach:uml-install3.jpg]]
|  | 47 |
|  | 48 | 1*. Choose the //KIELER nightly - [[(% class="icon" %) (%%)http:~~/~~/rtsys.informatik.uni-kiel.de/~~~~kieler/updatesite/nightly>>url:http://rtsys.informatik.uni-kiel.de/confluence/%7Ekieler/updatesite/nightly||shape="rect" class="ext-link"]]// Update Site from the drop down list.
|  | 49 |
|  | 50 | 1*. 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.
|  | 51 | [[image:attach:uml-install4.jpg]]
|  | 52 |
|  | 53 | 1*. Eclipse should again ask you to restart the KIELER RCA. Click the //Restart Now// button.
|  | 54 |
|  | 55 | 1. Congratulations! You have now installed everything you need to simulate and model check UML state machines with KIELER.
|  | 56 |
|  | 57 | ----
|  | 58 |
|  | 59 | == Simulating and Model Checking of UML State Machines ==
|  | 60 |
|  | 61 | 1. Close the //Outline// Eclipse View because it may produce errors with this early version of Papyrus MDT.
|  | 62 | 1. Create an empty (normal) Eclipse Project (//File/New/Project//) and give it some name, e.g., //test//.
|  | 63 | [[image:attach:uml1.jpg]]
|  | 64 |
|  | 65 | 1. Create a Papyrus Diagram in this new project:
|  | 66 | 1*. //File/New/Other//
|  | 67 |
|  | 68 | 1*. Select //Papyrus/Papyrus Model//
|  | 69 | [[image:attach:uml2.jpg]]
|  | 70 |
|  | 71 | 1*. Give it a name, e.g., //model.di//.
|  | 72 | [[image:attach:uml3.jpg]]
|  | 73 |
|  | 74 | 1*. Select [x] UML as the //Diagram Language//.
|  | 75 | [[image:attach:uml4.jpg]]
|  | 76 |
|  | 77 | 1*. Select [x] UML State Machine as the //Diagram Kind//.
|  | 78 | [[image:attach:uml5.jpg]]
|  | 79 |
|  | 80 | 1. You should now see a plain UML state machine diagram editor pane where you can freely model your state machine.
|  | 81 | [[image:attach:uml6.jpg]]
|  | 82 |
|  | 83 | 1. 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//.
|  | 84 | [[image:attach:uml7.jpg]]
|  | 85 |
|  | 86 | 1. During modeling you may want to use our integrated automatic layout feature.
|  | 87 | [[image:attach:uml8.jpg]]
|  | 88 | \\[[image:attach:uml9.jpg]]
|  | 89 |
|  | 90 |
|  | 91 | === Simulating ===
|  | 92 |
|  | 93 | 1. Deactivate the DataComponent for model checking as shown below and validate that the path to the Maude executable is set correctly.
|  | 94 | [[image:attach:uml-sim1.jpg]]
|  | 95 |
|  | 96 | 1. You must save your changes to the diagram before you can simulate it.
|  | 97 |
|  | 98 | 1. You may want to inspect the output of Maude in the //Console// Eclipse View.
|  | 99 |
|  | 100 | 1. Start the simulation by pressing the //Step// or //Run// button of the //Execution Manager// View.
|  | 101 | 1. The state machine's Maude representation will be generated in your projects folder.
|  | 102 | 1. Now you can set (input) events and inspect (output) actions in the DataTable Eclipse View.
|  | 103 | [[image:attach:uml-sim2.jpg]]
|  | 104 |
|  | 105 | 1. You can now you the //Step// button to perform a simulation (run-to-completion) step or use the //Run/Pause// buttons.
|  | 106 |
|  | 107 |
|  | 108 | ----
|  | 109 |
|  | 110 | === Model Checking ===
|  | 111 |
|  | 112 | 1. Deactivate the DataComponent for simulation as shown below and validate that the path to the Maude executable is set correctly.
|  | 113 | [[image:attach:uml-mc1.jpg]]
|  | 114 |
|  | 115 | 1. Set your desired model checking term in the properties of the model check DataComponent.
|  | 116 | 1. You must save your changes to the diagram before you can model check it.
|  | 117 |
|  | 118 | 1. You may want to inspect the output of Maude in the //Console// Eclipse View.
|  | 119 |
|  | 120 | 1. Start the simulation by pressing the //Step// button of the //Execution Manager// View.
|  | 121 | 1. The state machine's Maude representation will be generated in your projects folder.
|  | 122 | 1. Now you can set (input) events and inspect (output) actions in the DataTable Eclipse View.
|  | 123 | [[image:attach:uml-sim2.jpg]]
|  | 124 |
|  | 125 | 1. When you now click on //Step// again, model checking will be performed and you will be prompted the result.
|  | 126 |
|  | 127 | 1. If there is a counter example, then you can now use subsequent clicks on //Step// to inspect it.
|  | 128 |
|  | 129 |
|  | 130 | ----
|  | 131 |
|  | 132 | == Links ==
|  | 133 |
|  | 134 | * [[(% class="icon" %) (%%)Papyrus MDT Eclipse Project>>url:http://www.eclipse.org/modeling/mdt/papyrus/||shape="rect" class="ext-link"]]
|  | 135 | * [[(% class="icon" %) (%%)The Maude System>>url:http://maude.cs.uiuc.edu/||shape="rect" class="ext-link"]]
|  | 136 | * [[KIELER Execution Manager>>url:http://rtsys.informatik.uni-kiel.de/confluence/pages/viewpage.action?pageId=328095||shape="rect"]]
|  | 137 | * [[KIELER DataTable>>url:http://rtsys.informatik.uni-kiel.de/confluence/pages/viewpage.action?pageId=328095||shape="rect"]]

# Quick Links

KIELER on GitHub
RTSYS Homepage

XWiki 14.4.7