Last modified by Richard Kreissig on 2023/09/14 10:32
From version < 4.1 >
edited by cmot
on 2012/04/10 14:15
To version 1.1 >
edited by tig
on 2012/03/20 15:11
>
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 with Maude
1 +UML State Machine Simulation/Model Checking
Author
... ... @@ -1,1 +1,1 @@
1 -XWiki.cmot
1 +XWiki.tig
Content
... ... @@ -1,138 +1,3 @@
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"]]
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}}
Confluence.Code.ConfluencePageClass[0]
Id
... ... @@ -1,1 +1,1 @@
1 -885046
1 +884938
URL
... ... @@ -1,1 +1,1 @@
1 -https://rtsys.informatik.uni-kiel.de/confluence//wiki/spaces/KIELER/pages/885046/UML State Machine Simulation/Model Checking with Maude
1 +https://rtsys.informatik.uni-kiel.de/confluence//wiki/spaces/KIELER/pages/884938/UML State Machine Simulation/Model Checking

Navigation

Quick Links

KIELER on GitHub
RTSYS Homepage