Abstract
Digitalisation and innovation among the railway systems entail effort-demanding challenges, especially when considering how crucial it is to verify safety requirements and proof security levels. The early Verification and Validation (V&V) of railway systems detect critical issues and avoid severe consequences due to software failure. This paper aims to distinguish the subset of SysML language, which can be verified and usable by a systems engineer. As we are interested in proving safety properties expressed using invariants on states, we consider the Event-B method for this purpose. Later the selected SysML subset is used for automatic transformation and finally performing the verification using a formal verification tool. The transformation is applied on a simple point machine case study from DB Netz AG; First, a SysML model is designed using the Windchill modeler, then automatically transformed to Event-B and finally imported into the RODIN platform for formal verification.
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
Similar content being viewed by others
Notes
- 1.
- 2.
Our work is featured in embedded video on EULYNX website: https://www.youtube.com/watch?v=GhoNoMm4om0.
- 3.
- 4.
- 5.
References
Friedenthal, S., Moore, A., Steiner, R.: OMG systems modeling language (OMG SysML) tutorial. In: INCOSE International Symposium, vol. 9 (2006)
Abrial, J.-R., et al.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447–466 (2010)
Weidmann, N., et al.: Incremental bidirectional model transformation with eMoflon: IBeX. In: Cheney, J., Ko, H.-S. (eds.) [Email Protected] 2019 (CEUR Workshop Proceedings), vol. 2355, pp. 45–55. CEUR-WS.org (2019)
Berglehner, R., Rasheeq, A., Cherif, I.: An approach to improve SysML railway specification using UML-B and EVENT-B. Poster Presented at RSSRail (2019)
Schürr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-59071-4_45
Butler, M., Hallerstede, S.: The Rodin formal modelling tool. In: FACS 2007 Christmas Workshop: Formal Methods in Industry, pp. 1–5 (2007)
Snook, C., Butler, M.: UML-B and Event-B: an integration of languages and tools (2008)
Bousse, E., et al.: Aligning SysML with the B method to provide V&V for systems engineering. In: Proceedings of the Workshop on Model-driven Engineering, Verification and Validation (2012)
Wang, H., et al.: Integrating model checking with SysML in complex system safety analysis. IEEE Access 7, 16561–16571 (2019)
Zhang, Q., Huang, Z., Xie, J.: Distributed system model using SysML and Event-B. In: Gu, X., Liu, G., Li, B. (eds.) MLICOM 2017. LNICST, vol. 226, pp. 326–336. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73564-1_32
Giese, H., Hildebrandt, S., Neumann, S.: Towards integrating SysML and AUTOSAR modeling via bidirectional model synchronization. In: MBEES (2009)
Luttik, S.P.B.: What is the point: formal analysis and test generation for a railway standard. e-proc (ESREL2020 PSAM15) (2020)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Salunkhe, S., Berglehner, R., Rasheeq, A. (2021). Automatic Transformation of SysML Model to Event-B Model for Railway CCS Application. In: Raschke, A., Méry, D. (eds) Rigorous State-Based Methods. ABZ 2021. Lecture Notes in Computer Science(), vol 12709. Springer, Cham. https://doi.org/10.1007/978-3-030-77543-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-77543-8_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-77542-1
Online ISBN: 978-3-030-77543-8
eBook Packages: Computer ScienceComputer Science (R0)