(Update links) |
|||
| (One intermediate revision by the same user not shown) | |||
| Line 22: | Line 22: | ||
=== Resources === | === Resources === | ||
* [ | * [https://stups.hhu-hosting.de/downloads/pdf/abz14casestudy.pdf ABZ 2014 Case Study Paper] | ||
* [[Media:LandingGear.zip|Landing Gear Model EventB Model]] | * [[Media:LandingGear.zip|Landing Gear Model EventB Model]] | ||
| Line 28: | Line 28: | ||
==== BMotion Studio for ProB ==== | ==== BMotion Studio for ProB ==== | ||
* [ | * [[BMotion Studio|BMotion Studio for ProB Homepage]] | ||
* [https:// | * [https://stups.hhu-hosting.de/handbook/bmotion/current/html/ BMotion Studio for ProB User Handbook] | ||
* [https://github.com/ladenberger/bmotion-prob BMotion Studio for ProB Sourcecode] | * [https://github.com/ladenberger/bmotion-prob BMotion Studio for ProB Sourcecode] | ||
==== ProB 2.0 ==== | ==== ProB 2.0 ==== | ||
* [ | * [https://stups.hhu-hosting.de/handbook/prob2/prob_handbook.html ProB 2.0 Developer Handbook] | ||
* [https://github.com/ | * [https://github.com/hhu-stups/prob2_kernel ProB 2.0 Sourcecode] | ||
* [ | * [https://stups.hhu-hosting.de/rodin/prob2/nightly/ ProB 2.0 Nightly Build Updatesite] | ||
* [[Tutorial13|ProB 2.0 Tutorial]] | * [[Tutorial13|ProB 2.0 Tutorial]] | ||
=== References === | === References === | ||
<references /> | <references /> | ||
This page provides additional resources for the journal article we have submitted for the International Journal on Software Tools for Technology Transfer.
The journal article is an extended version of the paper we have submitted for the ABZ 2014 case study track.
The full description of the case study can be found here.
We have prepared two interactive live visualizations of the case study. One of our own Event-B model and one of the first development by Jean-Raymond Abrial and Wen Su [1].
The visualization of our own model can either be controlled by interacting with the displayed elements (i.e., clicking the handle) or using the Events view which can be opened using the "Open View" menu at the bottom right corner. The other model can only be controlled using the Events view.