Wiki source code of UML State Machine Simulation/Model Checking with Maude
Last modified by Richard Kreissig on 2023/09/14 10:32
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"]] |