Automatic Transformation of SysML Model to Event-B Model for Railway CCS Application

Shubhangi Salunkhe, Randolf Berglehner, Abdul Rasheeq
Digital Printed Abstract View Cite
Type
Short Paper
Publication
8th International Conference on Rigorous State Based Methods (ABZ'21)

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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{SalunkheBR21,
  author       = {Shubhangi Salunkhe and
                  Randolf Berglehner and
                  Abdul Rasheeq},
  editor       = {Alexander Raschke and
                  Dominique M{\'{e}}ry},
  title        = {Automatic Transformation of SysML Model to Event-B Model for Railway
                  {CCS} Application},
  booktitle    = {Rigorous State-Based Methods - 8th International Conference, {ABZ}
                  2021, Ulm, Germany, June 9-11, 2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12709},
  pages        = {143--149},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-77543-8\_14},
  doi          = {10.1007/978-3-030-77543-8\_14},
  timestamp    = {Tue, 15 Jun 2021 17:24:03 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/SalunkheBR21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'21

Related