Summary

• Page properties (3 modified, 0 added, 0 removed)

Details

Page properties

Parent

...	...	@@ -1,1 +1,1 @@
1		-Kieler.Discontinued Projects.WebHome
	1	+KIELER.Discontinued Projects.WebHome

Author

...	...	@@ -1,1 +1,1 @@
1		-XWiki.cmot
	1	+XWiki.stu230980

Content

...	...	@@ -1,9 +1,8 @@
1		-{{panel borderStyle="dashed" title="Project Overview"}}
	1	+== Project Overview ==
2	2	Responsible:
3	3
4	4	* [[Christian Motika>>url:http://www.informatik.uni-kiel.de/rtsys/kontakt/cmot/||shape="rect"]]
5	5	* Jens Schönborn
6		-{{/panel}}
7	7
8	8	= UML State Machine Simulation and Model Checking with Maude =
9	9
...	...	@@ -30,29 +30,29 @@
30	30	== Installation ==
31	31
32	32	1. Download and install the [[(% class="icon" %) (%%)Maude System>>url:http://maude.cs.uiuc.edu/download/||shape="rect" class="ext-link"]]
33		-\\
	32	+
34	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		-\\
	34	+
36	36	1. Install Papyrus
37	37	1*. Start the KIELER RCA and klick on the //Install Modeling Components// button
38	38	[[image:attach:uml-install1.jpg]]
39		-\\
	38	+
40	40	1*. Select the Papyrus MDT Tools and install them into the KIELER RCA
41	41	[[image:attach:uml-install2.jpg]]
42		-\\
	41	+
43	43	1*. Eclipse should now ask you to restart the KIELER RCA. Click the //Restart Now// button.
44		-\\
	43	+
45	45	1. Finally, install KIELER UML Simulation and Model Checking components
46		-1*. Click on //Help/////Install New Software...//.
	45	+1*. Click on //Help/Install New Software...//.
47	47	[[image:attach:uml-install3.jpg]]
48		-\\
	47	+
49	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		-\\
	49	+
51	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	52	[[image:attach:uml-install4.jpg]]
53		-\\
	52	+
54	54	1*. Eclipse should again ask you to restart the KIELER RCA. Click the //Restart Now// button.
55		-\\
	54	+
56	56	1. Congratulations! You have now installed everything you need to simulate and model check UML state machines with KIELER.
57	57
58	58	----
...	...	@@ -60,51 +60,51 @@
60	60	== Simulating and Model Checking of UML State Machines ==
61	61
62	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//.
	62	+1. Create an empty (normal) Eclipse Project (//File/New/Project//) and give it some name, e.g., //test//.
64	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//
	64	+
	65	+1. Create a Papyrus Diagram in this new project:
	66	+1*. //File/New/Other//
	67	+
	68	+1*. Select //Papyrus/Papyrus Model//
70	70	[[image:attach:uml2.jpg]]
71		-\\
	70	+
72	72	1*. Give it a name, e.g., //model.di//.
73	73	[[image:attach:uml3.jpg]]
74		-\\
	73	+
75	75	1*. Select [x] UML as the //Diagram Language//.
76	76	[[image:attach:uml4.jpg]]
77		-\\
	76	+
78	78	1*. Select [x] UML State Machine as the //Diagram Kind//.
79	79	[[image:attach:uml5.jpg]]
80		-\\
	79	+
81	81	1. You should now see a plain UML state machine diagram editor pane where you can freely model your state machine.
82	82	[[image:attach:uml6.jpg]]
83		-\\
	82	+
84	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	85	[[image:attach:uml7.jpg]]
86		-\\
	85	+
87	87	1. During modeling you may want to use our integrated automatic layout feature.
88	88	[[image:attach:uml8.jpg]]
89	89	\\[[image:attach:uml9.jpg]]
90		-\\
	89	+
91	91
92	92	=== Simulating ===
93	93
94	94	1. Deactivate the DataComponent for model checking as shown below and validate that the path to the Maude executable is set correctly.
95	95	[[image:attach:uml-sim1.jpg]]
96		-\\
	95	+
97	97	1. You must save your changes to the diagram before you can simulate it.
98		-\\
	97	+
99	99	1. You may want to inspect the output of Maude in the //Console// Eclipse View.
100		-\\
	99	+
101	101	1. Start the simulation by pressing the //Step// or //Run// button of the //Execution Manager// View.
102	102	1. The state machine's Maude representation will be generated in your projects folder.
103	103	1. Now you can set (input) events and inspect (output) actions in the DataTable Eclipse View.
104	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		-\\
	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	+
108	108
109	109	----
110	110
...	...	@@ -112,21 +112,21 @@
112	112
113	113	1. Deactivate the DataComponent for simulation as shown below and validate that the path to the Maude executable is set correctly.
114	114	[[image:attach:uml-mc1.jpg]]
115		-\\
	114	+
116	116	1. Set your desired model checking term in the properties of the model check DataComponent.
117	117	1. You must save your changes to the diagram before you can model check it.
118		-\\
	117	+
119	119	1. You may want to inspect the output of Maude in the //Console// Eclipse View.
120		-\\
	119	+
121	121	1. Start the simulation by pressing the //Step// button of the //Execution Manager// View.
122	122	1. The state machine's Maude representation will be generated in your projects folder.
123	123	1. Now you can set (input) events and inspect (output) actions in the DataTable Eclipse View.
124	124	[[image:attach:uml-sim2.jpg]]
125		-\\
	124	+
126	126	1. When you now click on //Step// again, model checking will be performed and you will be prompted the result.
127		-\\
	126	+
128	128	1. If there is a counter example, then you can now use subsequent clicks on //Step// to inspect it.
129		-\\
	128	+
130	130
131	131	----
132	132