Skip to main content
SpringerLink
Log in

Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller

  • Conference paper
  • First Online:
Formal Methods for Industrial Critical Systems (FMICS 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14290))

  • 273 Accesses

Abstract

We propose a novel framework for model-based testing against specifications from EULYNX, a SysML-based standard from the railway industry for the controllers of systems such as points, signals, sensors, and crossings. The main challenge here is the sheer complexity: with state spaces exceeding \(10^{10}\) states, it is hard to derive test suites that achieve a meaningful type of coverage.

We tackle this problem by moving away from the traditional interleaving semantics for SysML. Instead, we propose a synchronous semantics in terms of Finite State Machines (FSMs), leveraging the fact that EULYNX is implemented on Programmable Logic Controllers (PLCs). Then, we deploy Single-Input-Change Deterministic Finite State Machines (SIC-DFSMs), which ensures fully deterministic tests thus minimizing scalability issues.

Our focus lies on the EULYNX specification for point controllers. The generated test suite achieves maximal transition coverage, but test execution time remains substantial. We introduce an additional test suite that achieves maximal transition label coverage. Remarkably, this smaller suite successfully identifies the same four faults as the larger suite.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 49.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 64.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Change history

  • 20 March 2024

    A correction has been published.

References

  1. Bachmann, T., van der Wal, D., van der Bijl, M., van der Meij, D., Oprescu, A.: Translating EULYNX SysML models into symbolic transition systems for model-based testing of railway signaling systems. 2022 IEEE Conference on Software Testing, Verification and Validation (ICST), pp. 355–364 (2022)

    Google Scholar 

  2. Basile, D., et al.: On the industrial uptake of formal methods in the railway domain. In: Furia, C., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 20–29. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98938-9_2

    Chapter  Google Scholar 

  3. Bonacchi, A., Fantechi, A., Bacherini, S., Tempestini, M.: Validation process for railway interlocking systems. Sci. Comput. Program. 128, 2–21 (2016)

    Article  Google Scholar 

  4. Bouwman, M., van der Wal, D., Luttik, B., Stoelinga, M., Rensink, A.: A case in point: verification and testing of a EULYNX interface. Formal Aspects Comput. 35, 1–38 (2022)

    Article  MathSciNet  Google Scholar 

  5. Braunstein, C., et al.: Complete model-based equivalence class testing for the ETCS ceiling speed monitor. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 380–395. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11737-9_25

    Chapter  Google Scholar 

  6. Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems (2019)

    Google Scholar 

  7. EULYNX website. http://eulynx.eu. Accessed 18 Jan 2023

  8. Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: SEFM Workshops (2013)

    Google Scholar 

  9. Ferrari, A., ter Beek, M.H.: Formal methods in railways: a systematic mapping study. ACM Comput. Surv. 55, 1–37 (2022). https://doi.org/10.1145/3520480

    Article  Google Scholar 

  10. Gay, G., Staats, M., Whalen, M.W., Heimdahl, M.P.E.: The risks of coverage-directed test case generation. IEEE Trans. Software Eng. 41, 803–819 (2015)

    Article  Google Scholar 

  11. Graf-Brill, A., Hermanns, H.: Model-based testing for asynchronous systems. In: FMICS-AVoCS (2017)

    Google Scholar 

  12. Haxthausen, A.E., Peleska, J.: model checking and model-based testing in the railway domain. In: SyDe Summer School (2015)

    Google Scholar 

  13. Huo, J., Petrenko, A.: Transition covering tests for systems with queues. Softw. Testing 19, 55–83 (2009)

    Google Scholar 

  14. International Electrotechnical Commission: International Standard IEC 61131: Programmable Controllers (2017)

    Google Scholar 

  15. Jia, Y., Harman, M.: An analysis and survey of the development of mutation testing. IEEE Trans. Software Eng. 37, 649–678 (2011)

    Article  Google Scholar 

  16. Kadakolmath, L., Ramu, U.D.: Model-checking-based automated test case generation for Z formal specification of an urban railway interlocking system. In: 2022 Fourth International Conference on Emerging Research in Electronics, Computer Science and Technology (ICERECT), pp. 1–8 (2022)

    Google Scholar 

  17. Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86, 43–68 (1983)

    Article  MathSciNet  Google Scholar 

  18. Khan, S.U.R., Lee, S.P., Javaid, N., Abdul, W.: A systematic review on test suite reduction: approaches, experiment’s quality evaluation, and guidelines. IEEE Access 6, 11816–11841 (2018)

    Article  Google Scholar 

  19. Kiran, A., Butt, W.H., Anwar, M.W., Azam, F., Maqbool, B.: A comprehensive investigation of modern test suite optimization trends, Tools and Techniques. IEEE Access 7, 89093–89117 (2019)

    Article  Google Scholar 

  20. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines-a survey. Proc. IEEE 84, 1090–1123 (1996)

    Article  Google Scholar 

  21. Liu, S., et al.: A formal semantics for complete UML state machines with communications. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 331–346. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38613-8_23

    Chapter  Google Scholar 

  22. Lv, J., Wang, H., Liu, H., Zhang, L., Tang, T.: A model-based test case generation method for function testing of train control systems. In: 2016 IEEE International Conference on Intelligent Rail Transportation (ICIRT), pp. 334–346 (2016)

    Google Scholar 

  23. Ma, C., Jordan, C.V., Provost, J.: SATE: model-based testing with design-to-test and plant features. IFAC-PapersOnLine 51, 310–315 (2018)

    Article  Google Scholar 

  24. Ma, C., Provost, J.: Design-to-test: an approach to enhance testability of programmable controllers for critical systems-two case studies (2016)

    Google Scholar 

  25. Ma, C., Provost, J.: Design-to-test approach for programmable controllers in safety-critical automation systems. IEEE Trans. Industr. Inf. 16, 6499–6508 (2020)

    Article  Google Scholar 

  26. Noroozi, N., Khosravi, R., Mousavi, M.R., Willemse, T.A.C.: Synchronizing asynchronous conformance testing. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 334–349. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24690-6_23

    Chapter  Google Scholar 

  27. Object Management Group: OMG Unified Modeling Language, Version 2.5.1 (2017). https://www.omg.org/spec/UML/

  28. Object Management Group: OMG Systems Modeling Language, Version 1.6 (2019). https://www.omg.org/spec/SysML/

  29. Paltor, I.: The Semantics of UML State Machines (1999)

    Google Scholar 

  30. Peleska, J.: Industrial-strength model-based testing - state of the art and current challenges. In: MBT (2013)

    Google Scholar 

  31. Polze, A.: EULYNX-Live: a methodology for validating system specifications in hybrid field tests EULYNX-Live: Eine Methodik zum Validieren von Systemspezifikationen in hybriden Feldtests (2021)

    Google Scholar 

  32. Provost, J., Roussel, J.M., Faure, J.M.: Testing programmable logic controllers from finite state machines specification. In: 2011 3rd International Workshop on Dependable Control of Discrete Systems, pp. 1–6 (2011)

    Google Scholar 

  33. Provost, J., Roussel, J.M., Faure, J.M.: Generation of single input change test sequences for conformance test of programmable logic controllers. IEEE Trans. Industr. Inf. 10, 1696–1704 (2014)

    Article  Google Scholar 

  34. Salunkhe, S., Berglehner, R., Rasheeq, A.: Automatic transformation of SysML model to event-B model for railway CCS application. In: International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (2021)

    Google Scholar 

  35. Sánchez, C., Cavalli, A.R., Yevtushenko, N.V., Santos, J., Abreu, R.: On modeling and testing components of the European train control system (2014)

    Google Scholar 

  36. Scippacercola, F., Pietrantuono, R., Russo, S., Zentai, A.: Model-in-the-loop testing of a railway interlocking system. In: Desfray, P., Filipe, J., Hammoudi, S., Pires, L.F. (eds.) MODELSWARD 2015. CCIS, vol. 580, pp. 375–389. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27869-8_22

    Chapter  Google Scholar 

  37. Sehr, M.A., et al.: programmable logic controllers in the context of industry 4.0. IEEE Trans. Industr. Inf. 17, 3523–3533 (2021)

    Google Scholar 

  38. Su, H., Chai, M., Liu, H., Chai, J., Yue, C.: A model-based testing system for safety of railway interlocking. 2022 IEEE 25th International Conference on Intelligent Transportation Systems (ITSC), pp. 335–340 (2022)

    Google Scholar 

  39. Tretmans, J.: Model based testing with labelled transition systems. In: Formal Methods and Testing (2008)

    Google Scholar 

  40. Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Testing 22, 297–312 (2012)

    Google Scholar 

  41. Verhaard, L., Tretmans, J., Kars, P., Brinksma, E.: On asynchronous testing. In: Protocol Test Systems (1992)

    Google Scholar 

  42. Virazel, A., David, R., Girard, P., Landrault, C., Pravossoudovitch, S.: Delay fault testing: choosing between random SIC and random MIC test sequences. J. Electron. Test. 17, 233–241 (2000)

    Article  Google Scholar 

  43. Wang, Y., Chen, L., Kirkwood, D., Fu, P., Lv, J., Roberts, C.: Hybrid online model-based testing for communication-based train control systems. IEEE Intell. Transp. Syst. Mag. 10, 35–47 (2018)

    Article  Google Scholar 

  44. Yi, W., Xing-hua, F., Dai-qiang, W.: An implementation of random single input change technique for low-power test. In: 2008 2nd International Conference on Anti-counterfeiting, Security and Identification, pp. 352–355 (2008)

    Google Scholar 

Download references

Acknowledgements

This paper is a product of the FormaSig project, fully funded by DB Netz AG and ProRail. The vision illustrated in this article reflects the personal views of the authors, and is not part of the strategy of DB Netz AG or ProRail. We thank the SIGNON Group (https://signon-group.com/) for providing access to the source code of the software simulator.

Author information

Authors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Djurre van der Wal, Marcus Gerhold & Mariëlle Stoelinga

Authors
  1. Djurre van der Wal
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marcus Gerhold
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mariëlle Stoelinga
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Djurre van der Wal .

Editor information

Editors and Affiliations

  1. Fondazione Bruno Kessler, Povo, Italy

    Alessandro Cimatti

  2. NASA Langley Research Center, AMA-NASA LaRC, Hampton, VA, USA

    Laura Titolo

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

van der Wal, D., Gerhold, M., Stoelinga, M. (2023). Conformance in the Railway Industry: Single-Input-Change Testing a EULYNX Controller. In: Cimatti, A., Titolo, L. (eds) Formal Methods for Industrial Critical Systems. FMICS 2023. Lecture Notes in Computer Science, vol 14290. Springer, Cham. https://doi.org/10.1007/978-3-031-43681-9_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-43681-9_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-43680-2

  • Online ISBN: 978-3-031-43681-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation