Introduction (How to extend Rodin Tutorial)

>next: Creating our plugin

^up: How to extend Rodin Tutorial (Index)

In this tutorial, we will focus on the extension of the Rodin platform by adding plugins. This mechanism inherits from Eclipse extension mechanism. As we will discuss here about the provided Rodin extensibility possibilities, reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and are familiar with the notion of extension points.
For informations about extension points, please refer to this article : [[1]].

This tutorial is problem solving oriented. Hence, all contributions to the platform via plugin additions will address needs implied by the issues we aim to solve, or functionnalities we want to add.
We will, in a first time, focus on one concrete example of needed plugin that we will develop step-by-step. This first example is build to add Probabilistic Termination and Qualitative Reasoning in Rodin. For more informations about the Probabilistic Termination and Qualitative Reasoning, please refer to the paper of Emre Yilmaz and Thai Son Hoang : Development of Rabin's Choice Coordination Algorithm in Event-B in Proceedings of the 10th International Workshop on Automated Verification of Critical Systems (AVoCS 2010)
//FIXME Include link to the paper here
In a second time, we will use small examples, to review all extensions abilities that didn't appear in the first part of this tutorial.

---

Outline

First part : extending Rodin with a plugin for Qualitative Probabilistic Reasoning

1. Creating our plugin
2. Adding elements to the database (Extend the database)
3. //extend the ui
4. //extend the static checker
5. //extend the proof obligation generator

Second part : extending Rodin (other extension abilities not mentioned above)

---

Requirements

Reading this tutorial implies that you have basic knowledge about eclipse extension mechanism, and are familiar with the notion of extension points.
For informations about extension points, please refer to this article : [[2]].

Moreover, a development environment is required to develop the plugin code described in this tutorial.
//FIXME Document more about the needed environment to develop plugins for Rodin

>next: Creating our plugin

^up: How to extend Rodin Tutorial (Index)