Rodin Handbook
This work is sponsored by the Deploy Project
This work is licensed under a Creative Commons Attribution 3.0 Unported License
 |
 |
 |
User Manual for Rodin v.2.3 |  |
 |
 |
2 Tutorial
The objective is to get you to a stage where you can use Rodin and build Event-B models. We expect you to have a basic understanding of logic and an idea why doing formal modeling is a good idea. You should be able to work through the tutorial with little or no outside help.
This tutorial covers installation and configuration for Rodin. It brings you step by step through building formal models, it provides the essential theory and provides pointers to more information.
We attempt to alternate between theory and practical application and thereby keep you motivated. We encourage you not to download solutions to the examples but instead to actively build them up yourself as the tutorial progresses.
If something is unclear, remember to check the Reference chapter (Chapter 3) for more information.
|
|
|
|
|
|