In this website, we present the formal development of our examples in the paper “Formalizing Hybrid System with Event-B and Rodin Platform”.


The entire model of those examples can be obtained as either the PDF format document or the source model of the Rodin Platform. For those who are interesting in our model but don’t use the Rodin Platform, you can read our model in the PDF document.

For those who are interesting to check the models with the Rodin Platform, here are some information: if you have not yet downloaded the Rodin Platform, please download the newest version 2.8 from the website: http://www.event-b.org. If you have already got the Platform, please make sure that you have installed the plug-in of Atelier B and SMT solver. Please use the tactic profile WS_profile1 as provided in this website. This is the tactic profile we used for all the proofs. In order to change tactic profile, please go to: Preferences –> Event-B –> Sequent Prover –> Auto/Post Tactic, in the tag “Profiles”, please click “Import” and then choose the profile we proposed. After that, go the the tag “Auto/Post Tactic”, enable both the auto-tactic and the post-tactic for proving, and set them both to the profile we proposed.

We also recommend the plug-in AnimB for animation. In order to use AnimB, please check your editor, since only Event-B Context Editor is supported by AnimB.


If you have any question, please don’t hesitate to contact us: wsu@shu.edu.cn


PDF document

Readme Readme.pdf
Models in PDF document Examples.pdf

Models of the Rodin Platform

The Saw saw.zip
Nuclear Plant Cooling nuclear.zip
Controlling Train 1.One Train Model: train.zip
2.Multiple Train Model: train_multiple.zip
Aircraft Collision Avoidance aircraft.zip
Water Tank water_tank.zip

Tactic profile

WS_profile1 WS_profile1.xml

Download all

All previous material together: ALL.zip

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes:

<a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <s> <strike> <strong>