diff --git a/visualizations/LandingGear/GearsDoors/LandingGear_R6.mch b/visualizations/LandingGear/GearsDoors/LandingGear_R6.mch index 72bd1819e166f1370614ab88f8b30a4c1927338b..0c757ca067c37034036d77d487566ccae7b49376 100644 --- a/visualizations/LandingGear/GearsDoors/LandingGear_R6.mch +++ b/visualizations/LandingGear/GearsDoors/LandingGear_R6.mch @@ -1,3 +1,9 @@ +/* +Original model from Event-B: +L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. + +Translated to Classical B manually +*/ MACHINE LandingGear_R6 SETS /* enumerated */ DOOR_STATE={open,closed,door_moving}; diff --git a/visualizations/LandingGear/GearsDoors/physical.svg b/visualizations/LandingGear/GearsDoors/physical.svg index 6b9a224c00c47cd67d52084428ed6287e5f958ac..15b5728d1bab0cc8d050c9d3eff066f1ee1df432 100644 --- a/visualizations/LandingGear/GearsDoors/physical.svg +++ b/visualizations/LandingGear/GearsDoors/physical.svg @@ -1,3 +1,4 @@ +<!-- From L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. !--> <svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink"> <metadata id="metadata3467">image/svg+xml</metadata> diff --git a/visualizations/LandingGear/HydraulicCircuit/LandingGear_R6.mch b/visualizations/LandingGear/HydraulicCircuit/LandingGear_R6.mch index 72bd1819e166f1370614ab88f8b30a4c1927338b..0c757ca067c37034036d77d487566ccae7b49376 100644 --- a/visualizations/LandingGear/HydraulicCircuit/LandingGear_R6.mch +++ b/visualizations/LandingGear/HydraulicCircuit/LandingGear_R6.mch @@ -1,3 +1,9 @@ +/* +Original model from Event-B: +L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. + +Translated to Classical B manually +*/ MACHINE LandingGear_R6 SETS /* enumerated */ DOOR_STATE={open,closed,door_moving}; diff --git a/visualizations/LandingGear/HydraulicCircuit/architecture.svg b/visualizations/LandingGear/HydraulicCircuit/architecture.svg index 81bba719c8c6819b864376d7f6a1046752211c32..66c9f0ca829689ccb1bbce7ffe784cc688a481a1 100644 --- a/visualizations/LandingGear/HydraulicCircuit/architecture.svg +++ b/visualizations/LandingGear/HydraulicCircuit/architecture.svg @@ -1,3 +1,4 @@ +<!-- From L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. !--> <?xml-stylesheet href="landinggear.css" type="text/css"?> <svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink"> diff --git a/visualizations/LandingGear/HydraulicCircuit/physical.svg b/visualizations/LandingGear/HydraulicCircuit/physical.svg index 6b9a224c00c47cd67d52084428ed6287e5f958ac..15b5728d1bab0cc8d050c9d3eff066f1ee1df432 100644 --- a/visualizations/LandingGear/HydraulicCircuit/physical.svg +++ b/visualizations/LandingGear/HydraulicCircuit/physical.svg @@ -1,3 +1,4 @@ +<!-- From L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017. !--> <svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink"> <metadata id="metadata3467">image/svg+xml</metadata> diff --git a/visualizations/LightModel/BlinkLamps_v3.mch b/visualizations/LightModel/BlinkLamps_v3.mch index 78ad6fc069a5c106451640dfd93ee5dee8866a22..a3efb1a4a7982750f9f367339251323b556c409d 100644 --- a/visualizations/LightModel/BlinkLamps_v3.mch +++ b/visualizations/LightModel/BlinkLamps_v3.mch @@ -1,3 +1,7 @@ +/* +Formal Model and VisB Visualization from +M. Leuschel, M. Mutz, and M. Werth. Modelling and Validating an Automotive System in Classical B and Event-B. In Proceedings ABZ, LNCS 12071, pages 335–350, 2020. +*/ MACHINE BlinkLamps_v3 // Manage Blinking Lights Actuators (blinkLeft, blinkRight) // and manage timing cycles diff --git a/visualizations/LightModel/GenericTimersMC.mch b/visualizations/LightModel/GenericTimersMC.mch index 80cb34ee6e39fa2c24e7c861f016a4b06508eb8f..35ded86c5c2ab5403f46959ef8f44961603c11cc 100644 --- a/visualizations/LightModel/GenericTimersMC.mch +++ b/visualizations/LightModel/GenericTimersMC.mch @@ -1,3 +1,7 @@ +/* +Formal Model and VisB Visualization from +M. Leuschel, M. Mutz, and M. Werth. Modelling and Validating an Automotive System in Classical B and Event-B. In Proceedings ABZ, LNCS 12071, pages 335–350, 2020. +*/ MACHINE GenericTimersMC SETS TIMERS = {blink_deadline, tip_deadline} diff --git a/visualizations/LightModel/PitmanController_TIME_MC_v4.mch b/visualizations/LightModel/PitmanController_TIME_MC_v4.mch index bc7ab486d668edfd8c22ba8133a3ca0bfb7715cf..3192f969d57ed6f95e760ab07e16b0f0783ce4bc 100644 --- a/visualizations/LightModel/PitmanController_TIME_MC_v4.mch +++ b/visualizations/LightModel/PitmanController_TIME_MC_v4.mch @@ -1,3 +1,7 @@ +/* +Formal Model and VisB Visualization from +M. Leuschel, M. Mutz, and M. Werth. Modelling and Validating an Automotive System in Classical B and Event-B. In Proceedings ABZ, LNCS 12071, pages 335–350, 2020. +*/ MACHINE PitmanController_TIME_MC_v4 INCLUDES BlinkLamps_v3, Sensors, GenericTimersMC diff --git a/visualizations/LightModel/Sensors.mch b/visualizations/LightModel/Sensors.mch index 1b3342e7a1df7afc251865a4a2797ce5edeb4915..007a51f8accd9e08996da6e1756d6aeeec2d7629 100644 --- a/visualizations/LightModel/Sensors.mch +++ b/visualizations/LightModel/Sensors.mch @@ -1,3 +1,7 @@ +/* +Formal Model and VisB Visualization from +M. Leuschel, M. Mutz, and M. Werth. Modelling and Validating an Automotive System in Classical B and Event-B. In Proceedings ABZ, LNCS 12071, pages 335–350, 2020. +*/ MACHINE Sensors /* Sensors and sensor value updates