Skip to content
Snippets Groups Projects
Commit 654afb33 authored by Fabian Vu's avatar Fabian Vu
Browse files

Update information

parent 761ca62f
No related branches found
No related tags found
No related merge requests found
Pipeline #146415 passed
/*
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};
......
<!-- 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>
......
/*
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};
......
<!-- 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">
......
<!-- 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>
......
/*
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
......
/*
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}
......
/*
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
......
/*
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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment