Abstract
Normally, the passengers on urban rail systems remain fairly stationary, allowing for a relatively straightforward approach to controlling the dynamics of the system, based on the total rest mass of the train and passengers. However when a mischievous rugby club board an empty train and then run and jump-stop during the braking process, they can disrupt the automatic mechanisms for aligning train and platform doors. This is the rugby club problem for automated urban train control. A simple scenario of this kind is modelled in Hybrid Event-B, and sufficient conditions are derived for the prevention of the overshoot caused by the jump-stop. The challenges of making the model more realistic are discussed, and a strategy for dealing with the rugby club problem, when it cannot be prevented, is proposed.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Such as the Paris Météor Line 14, engineered using the B-Method.
- 2.
Acceleration, time taken to reach cruising speed, etc.
- 3.
O. K. The Météor line is not circular, but you get the idea.
- 4.
- 5.
Such a design is visible on the Shanghai Metro’s circular line 4, as well as on some other, older Shanghai Metro lines, built when train door alignment control was less precise than today.
- 6.
The robustness of the carriages on the Shanghai line 4 would put much heavy rail to shame.
- 7.
If a mode event has an input, the semantics assumes that its value only arrives at a time strictly later than the previous mode event, ensuring part of (1) automatically. By this means we can ensure a mode event executes asynchronously—and if the only purpose of having an input would be to ensure this asynchronous scheduling, we can introduce the ‘async’ status and omit the input altogether, as in Fig. 2.
- 8.
Thus, ‘STATUS async’ is an abbreviation for the semantic device of giving the mode event an external input which is not used in the event’s body. See footnote 7.
- 9.
In fact, RugbyClubBoards remains enabled during the resumed TrainStationary event, so could execute again. But RugbyClubBoards is async and idempotent, so no harm would be done.
- 10.
This could also have been handled via a CONST declaration. In fact, that would have been more convenient, since assignment to a (time dependent, in general) expression generates a verification condition to check that the initial value of the expression agrees with the value on entry to the pliant event, in order to ensure right continuity of the variable’s history at the entry point to the pliant event, as required by the semantics [8]. Not mentioning brDist at all would entail the default behaviour for pliant variables during pliant events, namely of constraining them to simply obey any relevant invariants. This would be inappropriate here.
- 11.
While TrainDecelerating executes, RugbyClubJumpStop is (more or less) always enabled, but as in other cases, it is an async event and its effect is idempotent, so executing it again would have no discernible effect.
References
Alur, R.: Principles of Cyberphysical Systems. MIT Press, Cambridge (2015)
Banach, R.: Pliant modalities in hybrid event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 37–53. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39698-4_3
Banach, R.: The landing gear system in multi-machine hybrid Event-B. Int. J. Soft. Tools for Tech. Trans. 19, 205–228 (2017)
Banach, R.: Formal refinement and partitioning of a fuel pump system for small aircraft in hybrid Event-B. In: Bonsangue, M., Deng, Y. (eds.) Proceedings of IEEE TASE-16, pp. 65–72. IEEE (2016)
Banach, R.: Hemodialysis machine in hybrid event-B. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 376–393. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_32
Banach, R., Butler, M.: A hybrid Event-B study of lane centering. In: Aiguier, M., Boulanger, F., Krob, D., Marchal, C. (eds.) Complex Systems Design & Management, pp. 97–111. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-02812-5_8
Banach, R., Butler, M.: Cruise control in hybrid Event-B. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 76–93. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39718-9_5
Banach, R., Butler, M., Qin, S., Verma, N., Zhu, H.: Core hybrid Event-B I: single hybrid Event-B machines. Sci. Comput. Program. 105, 92–123 (2015)
Banach, R., Butler, M., Qin, S., Zhu, H.: Core hybrid Event-B II: multiple cooperating hybrid Event-B machines. Sci. Comput. Program. 139, 1–35 (2017)
Banach, R., Su, W.: Cyberphysical systems: a behind-the-scenes foundational view. In: Mashkoor, A., Thalheim, B., Wang, Q. (eds.) Proceedings of Klaus-Dieter Schewe Festschrift 2018. College Publications (2018, to appear)
Banach, R., Van Schaik, P., Verhulst, E.: Simulation and formal modelling of yaw control in a drive-by-wire application. In: Proceedings of FedCSIS IWCPS-15, pp. 731–742 (2015)
Bloch, A., Krishnaprasad, P., Murray, R., Baillieul, J., Crouch, P., Marsden, J., Zenkov, D.: Nonholonomic Mechanics and Control. Springer, New York (2015). https://doi.org/10.1007/b97376
Carloni, L., Passerone, R., Pinto, A., Sangiovanni-Vincentelli, A.: Languages and tools for hybrid systems design. Foundations and Trends in Electronic Design Automation, vol. 1, pp. 1–193 (2006)
ClearSy. http://www.clearsy.com/
Fasano, A., Marmi, S.: Analytical Mechanics. Oxford University Press, Oxford (2013)
Geisberger, E., Broy, M. (eds.): Living in a networked world. In: Integrated Research Agenda Cyber-Physical Systems (agendaCPS) (2015). http://www.acatech.de/fileadmin/user_upload/Baumstruktur_nach_Website/Acatech/root/de/Publikationen/Projektberichte/acaetch_STUDIE_agendaCPS_eng_WEB.pdf
Goldstein, H., Poole, C., Safko, J.: Classical Mechanics. Addison Wesley, Boston (2001)
Horvarth, J.: Topological Vector Spaces and Distributions. Dover, Mineola (2012)
Lecomte, T.: Atelier B has Turned 20. In: Proceedings of ABZ-16, LNCS, vol. 9675, p. XVI. Springer (2016)
Lee, E., Shesha, S.: Introduction to Embedded Systems: A Cyberphysical Systems Approach. 2nd edn (2015). LeeShesha.org
Papastavridis, J.: Analytical Mechanics: A Comprehensive Treatise on the Dynamics of Constrained Systems, 2nd edn. World Scientific, Singapore (2014)
Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14509-4
Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, Heidelberg (2009). https://doi.org/10.1007/978-1-4419-0224-5
Treves, F.: Topological Vector Spaces, Distributions and Kernels. Dover, Mineola (2007)
Zemanian, A.: Distribution Theory and Transform Analysis: An Introduction to Generalized Functions, with Applications. Dover, Mineola (2003)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Banach, R. (2018). Issues in Automated Urban Train Control: ‘Tackling’ the Rugby Club Problem. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-91271-4_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-91270-7
Online ISBN: 978-3-319-91271-4
eBook Packages: Computer ScienceComputer Science (R0)