Introduction (How to extend Rodin Tutorial)
In this tutorial, we will focus on the extension of the Rodin platform by adding plugins. This mechanism inherits from Eclipse extension mechanism (see paragraph about Extension points and Extensions below).
As we will discuss here about the provided Rodin extensibility possibilities, reading this tutorial implies that you have basic knowledge in Event-B, and are familiar with Java programming language.
Extension Points and Extensions
Rodin uses Eclipse extensibility mechanism. This mechanism is based on the notions of "extension points" and "extensions".
A plugin that wants to offer functionnalities (e.g. extension services) defines an extension point. An extension point is a sort of contract given to other plugins, to use (e.g. extend) those provided extension services. This contract is expressed in XML. A concrete example of extension service is offered by the plugin org.rodinp.core to register new elements in Rodin database.
Moreover, a plugin defining an extension point will manage all contributions (that we call extensions), through its lifecycle. In the case of Rodin Database, all extensions of the database (added elements, added attributes, etc.) are managed by the plugin org.rodinp.core.
To extend Rodin, we are in the situation where plugins (callers) want to use the extension services offered by one plugin (e.g. the callee that defines an extension point).
Thus, we will define a caller (a new plugin) that accepts one or more contracts with the Rodin platform. To accept such contract, a caller has to specify its dependency to the callee, and define one (resp. many) extensions, which conforms to an (resp. corresponding) imported extension point. The terms of the contract are often given through required interfaces, which defines a protocol to use the provided extension services. In other words, the results of the computation performed in caller's code need to conform to an interface defined by the callee (the extension service provider). Sometimes, the callee defines additional interfaces to give the callers a view on the managed contributions.
In this tutorial, we will define new callers and use the contracts offered by the Rodin platform.
For more informations about extension points, please refer to this article : [[1]].
Explanations and Outline
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 step-by-step plugin development . This first example will 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.
First part : extending Rodin with a plugin for Qualitative Probabilistic Reasoning
- Creating our plugin
- Adding elements to the database (Extend the database)
- //extend the ui
- //extend the static checker
- //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 programming in Java.
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
