ABZ14: Difference between revisions

(Update links)
 
(18 intermediate revisions by 5 users not shown)
Line 7: Line 7:
The full description of the case study can be found [[Media:landing_system.pdf|here]].
The full description of the case study can be found [[Media:landing_system.pdf|here]].


=== ProB Live Visualisation (click to join) ===
=== ProB Live Visualisations  ===
<html><a href="http://cobra.cs.uni-duesseldorf.de:8084/bms/landing/landinggear.html">
<img src="http://www.stups.uni-duesseldorf.de/ProB/images/7/7b/Landing_gear.png" width="600" /><a>
</html>


=== ProB Live Visualisations of other Event-B models (click to join) ===
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 <ref>Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System, Su, W. and Abrial, J., 2014 in Communications in Computer and Information Science (ABZ 2014: The Landing Gear Case Study)</ref>.


The following  two links contains executeable visualisations of the model from<ref>Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System, Su, W. and Abrial, J., 2014 in Communications in Computer and Information Science (ABZ 2014: The Landing Gear Case Study)</ref>  before and after our fix respectively.
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.


<html><a href="http://cobra.cs.uni-duesseldorf.de:8087/bms/vis_dev1/landinggear.html">
<!--
Before fix
# [http://wyvern.cs.uni-duesseldorf.de/bms/landing.html Visualization of our own model]
<a></html>
# [http://wyvern.cs.uni-duesseldorf.de:18080/bms/vis_dev1_fixed/landinggear.html Visualization of the model by Jean-Raymond Abrial and Wen Su  (Temporally disabled)]
-->


<html><a href="http://cobra.cs.uni-duesseldorf.de:8083/bms/vis_dev1_fixed/landinggear.html">
=== BMotion Studio for ProB Video ===
After fix
<html><iframe width="420" height="315" src="https://www.youtube.com/embed/wFr_pEjbpqo" frameborder="0" allowfullscreen></iframe></html>
<a></html>
 
=== ProB BMotion Studio Video ===
{{#ev:youtube|wFr_pEjbpqo|640}}


=== Resources ===
=== Resources ===
* [http://www.stups.hhu.de/w/Special:Publication/abz14casestudy Case Study Paper]
* [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 34: Line 28:


==== BMotion Studio for ProB ====
==== BMotion Studio for ProB ====
* [http://www.stups.hhu.de/ProB/index.php5/BMotion_Studio BMotion Studio for ProB Homepage]
* [[BMotion Studio|BMotion Studio for ProB Homepage]]
* [http://nightly.cobra.cs.uni-duesseldorf.de/bmotion/bmotion-prob-handbook/nightly/html/ BMotion Studio for ProB User Handbook]
* [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 ====
* [http://nightly.cobra.cs.uni-duesseldorf.de/prob2/prob2-handbook/nightly/devel/html/ ProB 2.0 Developer Handbook]
* [https://stups.hhu-hosting.de/handbook/prob2/prob_handbook.html ProB 2.0 Developer Handbook]
* [https://github.com/bendisposto/prob2 ProB 2.0 Sourcecode]
* [https://github.com/hhu-stups/prob2_kernel ProB 2.0 Sourcecode]
* [http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/ ProB 2.0 Nightly Build Updatesite]
* [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 />

Latest revision as of 12:54, 23 February 2023


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.

ProB Live Visualisations

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.


BMotion Studio for ProB Video

Resources

Links

BMotion Studio for ProB

ProB 2.0

References

  1. Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System, Su, W. and Abrial, J., 2014 in Communications in Computer and Information Science (ABZ 2014: The Landing Gear Case Study)