Last modified by Richard Kreissig on 2023/09/14 10:32
From version 1.1 >
edited by tig
on 2012/03/20 15:11
To version < 4.1 >
edited by cmot
on 2012/04/10 14:15
>
Change comment: There is no comment for this version

Summary

Details

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

Navigation

Quick Links

KIELER on GitHub
RTSYS Homepage