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: firstname.lastname@example.org
|Models in PDF document||Examples.pdf|
Models of the Rodin Platform
|Nuclear Plant Cooling||nuclear.zip|
1.One Train Model: train.zip
2.Multiple Train Model: train_multiple.zip
|Aircraft Collision Avoidance||aircraft.zip|
|All previous material together:||ALL.zip|