Logo PTI Logo FedCSIS

Proceedings of the 17th Conference on Computer Science and Intelligence Systems

Annals of Computer Science and Information Systems, Volume 30

Formal analysis of timeliness in the RaSTA protocol

, ,

DOI: http://dx.doi.org/10.15439/2022F176

Citation: Proceedings of the 17th Conference on Computer Science and Intelligence Systems, M. Ganzha, L. Maciaszek, M. Paprzycki, D. Ślęzak (eds). ACSIS, Vol. 30, pages 505–514 ()

Full text

Abstract. Formal reasoning about the correctness of safety-critical system's properties is crucial since such systems may impact their environment when malfunctioning. The Rail Safe Transport Application (RaSTA) Protocol is a protocol for such systems used in railway applications such as signaling. It claims to provide highly available and timely communication based on the application's demands. We investigate timeliness, i.e. the property that application data do not become obsolete.We analyze the protocol's specification and provide assumptions necessary to resolve imprecisions. Under the specified error model, we find that the deadline's proposed bound until which messages are considered timely is to restrictive, disabling RaSTA's own mechanisms to recover from lost messages in time. We formalize the specification of timeliness to provide a counterexample for the proposed bound and create an improved bound that does not lead to violated deadlines under the same assumptions and error model.

References

  1. “Electric signalling systems for railways - part 200: Safe transmission protocol according to DIN EN 50159 (VDE 0831-159),” Jun. 2015.
  2. Home - Uppaal. Date accessed: 2022-21-04. [Online]. Available: https://uppaal.org
  3. “Railway applications - communication, signalling and processing systems - safety-related communication in transmission systems; german version EN 50159:2010,” Apr. 2011.
  4. R. L. Rivest, “The MD4 Message-Digest Algorithm,” Internet Requests for Comments, April 1992, http://www.rfc-editor.org/rfc/rfc1320.txt. [Online]. Available: http://www.rfc-editor.org/rfc/rfc1320.txt
  5. M. Heinrich, J. Vieten, T. Arul, and S. Katzenbeisser, “Security analysis of the rasta safety protocol,” in 2018 IEEE International Conference on Intelligence and Security Informatics (ISI), 2018. http://dx.doi.org/10.1109/ISI.2018.8587371 pp. 199–204.
  6. J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, and W. Yi, “Uppaal—a tool suite for automatic verification of Real–Time Systems,” BRICS Report Series, vol. 3, no. 58, Jun. 1996. doi: 10.7146/brics.v3i58.18769. [Online]. Available: https://tidsskrift.dk/brics/article/view/18769
  7. L. Lamport, “A fast mutual exclusion algorithm,” ACM Trans. Comput. Syst., vol. 5, no. 1, p. 1–11, jan 1987. http://dx.doi.org/10.1145/7351.7352. [Online]. Available: https://doi.org/10.1145/7351.7352
  8. K. G. Larsen, P. Pettersson, and W. Yi, “Compositional and Symbolic Model-Checking of Real-Time Systems,” in Proc. of the 16th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, Dec. 1995. http://dx.doi.org/10.1109/REAL.1995.495198 pp. 76–87.
  9. ——, “Diagnostic model-checking for real-time systems,” in Hybrid Systems III. Berlin, Heidelberg: Springer Berlin Heidelberg, 1996. http://dx.doi.org/10.1007/BFb0020977. ISBN 978-3-540-68334-6 pp. 575–586.
  10. K. Havelund, A. Skou, K. G. Larsen, and K. Lund, “Formal modeling and analysis of an audio/video protocol: An industrial case study using uppaal,” in Proceedings Real-Time Systems Symposium. IEEE, 1997. http://dx.doi.org/10.1109/REAL.1997.641264 pp. 2–13.
  11. G. Behrmann, A. David, and K. G. Larsen, A Tutorial on Uppaal, ser. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, 2004, vol. 3185, p. 200–236. ISBN 978-3-540-23068-7. [Online]. Available: http://link.springer.com/10.1007/978-3-540-30080-9_7
  12. Uppaal documentation. Date accessed: 2022-21-04. [Online]. Available: https://docs.uppaal.org/
  13. T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking for real-time systems,” Information and Computation, vol. 111, no. 2, p. 193–244, Jun 1994. http://dx.doi.org/10.1006/inco.1994.1045
  14. E. M. Clarke, W. Klieber, M. Nováček, and P. Zuliani, Model Checking and the State Explosion Problem, ser. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, vol. 7682, p. 1–30. ISBN 978-3-642-35745-9. [Online]. Available: http://link.springer.com/10.1007/978-3-642-35746-6_1