Last modified by Richard Kreissig on 2023/09/14 10:32
Hide last authors
Richard Kreissig 9.1 1 == Project Overview ==
cds 3.1 2 Responsible:
3
4 * [[Christian Motika>>url:http://www.informatik.uni-kiel.de/rtsys/kontakt/cmot/||shape="rect"]]
5 * Jens Schönborn
cmot 4.1 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
cmot 6.1 19 You can download a standalone version of the UML Maude implementation here:[[attach:UML_SM_Maude.zip]]
cmot 4.1 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"]]
Richard Kreissig 9.1 32
cmot 4.1 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"]]
Richard Kreissig 9.1 34
cmot 4.1 35 1. Install Papyrus
36 1*. Start the KIELER RCA and klick on the //Install Modeling Components// button
37 [[image:attach:uml-install1.jpg]]
Richard Kreissig 9.1 38
cmot 4.1 39 1*. Select the Papyrus MDT Tools and install them into the KIELER RCA
40 [[image:attach:uml-install2.jpg]]
Richard Kreissig 9.1 41
cmot 4.1 42 1*. Eclipse should now ask you to restart the KIELER RCA. Click the //Restart Now// button.
Richard Kreissig 9.1 43
cmot 4.1 44 1. Finally, install KIELER UML Simulation and Model Checking components
Richard Kreissig 9.1 45 1*. Click on //Help/Install New Software...//.
cmot 4.1 46 [[image:attach:uml-install3.jpg]]
Richard Kreissig 9.1 47
cmot 4.1 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.
Richard Kreissig 9.1 49
cmot 4.1 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]]
Richard Kreissig 9.1 52
cmot 4.1 53 1*. Eclipse should again ask you to restart the KIELER RCA. Click the //Restart Now// button.
Richard Kreissig 9.1 54
cmot 4.1 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.
Richard Kreissig 9.1 62 1. Create an empty (normal) Eclipse Project (//File/New/Project//) and give it some name, e.g., //test//.
cmot 4.1 63 [[image:attach:uml1.jpg]]
Richard Kreissig 9.1 64
65 1. Create a Papyrus Diagram in this new project:
66 1*. //File/New/Other//
67
68 1*. Select //Papyrus/Papyrus Model//
cmot 4.1 69 [[image:attach:uml2.jpg]]
Richard Kreissig 9.1 70
cmot 4.1 71 1*. Give it a name, e.g., //model.di//.
72 [[image:attach:uml3.jpg]]
Richard Kreissig 9.1 73
cmot 4.1 74 1*. Select [x] UML as the //Diagram Language//.
75 [[image:attach:uml4.jpg]]
Richard Kreissig 9.1 76
cmot 4.1 77 1*. Select [x] UML State Machine as the //Diagram Kind//.
78 [[image:attach:uml5.jpg]]
Richard Kreissig 9.1 79
cmot 4.1 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]]
Richard Kreissig 9.1 82
cmot 4.1 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]]
Richard Kreissig 9.1 85
cmot 4.1 86 1. During modeling you may want to use our integrated automatic layout feature.
87 [[image:attach:uml8.jpg]]
88 \\[[image:attach:uml9.jpg]]
Richard Kreissig 9.1 89
cmot 4.1 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]]
Richard Kreissig 9.1 95
cmot 4.1 96 1. You must save your changes to the diagram before you can simulate it.
Richard Kreissig 9.1 97
cmot 4.1 98 1. You may want to inspect the output of Maude in the //Console// Eclipse View.
Richard Kreissig 9.1 99
cmot 4.1 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]]
Richard Kreissig 9.1 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
cmot 4.1 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]]
Richard Kreissig 9.1 114
cmot 4.1 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.
Richard Kreissig 9.1 117
cmot 4.1 118 1. You may want to inspect the output of Maude in the //Console// Eclipse View.
Richard Kreissig 9.1 119
cmot 4.1 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]]
Richard Kreissig 9.1 124
cmot 4.1 125 1. When you now click on //Step// again, model checking will be performed and you will be prompted the result.
Richard Kreissig 9.1 126
cmot 4.1 127 1. If there is a counter example, then you can now use subsequent clicks on //Step// to inspect it.
Richard Kreissig 9.1 128
cmot 4.1 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"]]

Navigation

Quick Links

KIELER on GitHub
RTSYS Homepage