{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:20Z","timestamp":1740109100498,"version":"3.37.3"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"1","funder":[{"name":"DB Netz AG and ProRail"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2023,3,31]]},"abstract":"We present a case study on the application of formal methods in the railway domain. The case study is part of the FormaSig project, which aims to support the development of EULYNX \u2014 a European standard defining generic interfaces for railway equipment \u2014 using formal methods. We translate the semi-formal SysML models created within EULYNX to formal mCRL2 models. By adopting a model-centric approach in which a formal model is used both for analyzing the quality of the EULYNX specification and for automated compliance testing, a high degree of traceability is achieved.<\/jats:p>\n The target of our case study is the EULYNX Point subsystem interface. We present a detailed catalog of the safety requirements, and provide counterexamples that show that some of them do not hold without specific fairness assumptions. We also use the mCRL2 model to generate both random and guided tests, which we apply to a third-party software simulator. We share metrics on the coverage and execution time of the tests, which show that guided testing outperforms random testing. The test results indicate several discrepancies between the model and the simulator. One of these discrepancies is caused by a fault in the simulator, the others are caused by false positives, i.e. an over-approximation of fail verdicts by our test setup.<\/jats:p>","DOI":"10.1145\/3528207","type":"journal-article","created":{"date-parts":[[2022,5,10]],"date-time":"2022-05-10T11:12:58Z","timestamp":1652181178000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["A Case in Point: Verification and Testing of a EULYNX Interface"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5131-008X","authenticated-orcid":false,"given":"Mark","family":"Bouwman","sequence":"first","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, Noord-Brabant, The Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4214-5438","authenticated-orcid":false,"given":"Djurre","family":"van der Wal","sequence":"additional","affiliation":[{"name":"University of Twente, Enschede, Overijssel, The Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6710-8436","authenticated-orcid":false,"given":"Bas","family":"Luttik","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, Noord-Brabant, The Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6793-8165","authenticated-orcid":false,"given":"Mari\u00eblle","family":"Stoelinga","sequence":"additional","affiliation":[{"name":"University of Twente, Enschede, Overijssel, The Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1714-6319","authenticated-orcid":false,"given":"Arend","family":"Rensink","sequence":"additional","affiliation":[{"name":"University of Twente, Enschede, Overijssel, The Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2023,3,16]]},"reference":[{"key":"e_1_3_3_2_2","volume-title":"Principles of Model Checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_3_3_3_2","first-page":"20","volume-title":"Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5\u20137, 2018, Proceedings (Lecture Notes in Computer Science)","volume":"11023","author":"Basile Davide","year":"2018","unstructured":"Davide Basile, Maurice H. ter Beek, Alessandro Fantechi, Stefania Gnesi, Franco Mazzanti, Andrea Piattino, Daniele Trentini, and Alessio Ferrari. 2018. On the industrial uptake of formal methods in the railway domain - A survey with stakeholders. In Integrated Formal Methods - 14th International Conference, IFM 2018, Maynooth, Ireland, September 5\u20137, 2018, Proceedings (Lecture Notes in Computer Science), Carlo A. Furia and Kirsten Winter (Eds.), Vol. 11023. Springer, 20\u201329. 10.1007\/978-3-319-98938-9_2"},{"key":"e_1_3_3_4_2","first-page":"266","volume-title":"TACAS\u201910 Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"Belinfante Axel","year":"2010","unstructured":"Axel Belinfante. 2010. JTorX: A tool for on-line model-driven test derivation and execution. In TACAS\u201910 Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 266\u2013270."},{"key":"e_1_3_3_5_2","volume-title":"JTorX: Exploring Model-Based Testing","author":"Belinfante Axel","year":"2014","unstructured":"Axel Belinfante. 2014. JTorX: Exploring Model-Based Testing. Ph.D. Dissertation. University of Twente, Enschede, Netherlands. http:\/\/purl.utwente.nl\/publications\/91781."},{"doi-asserted-by":"publisher","key":"e_1_3_3_6_2","DOI":"10.1016\/0304-3975(85)90088-X"},{"doi-asserted-by":"publisher","key":"e_1_3_3_7_2","DOI":"10.1016\/j.scico.2016.04.004"},{"key":"e_1_3_3_8_2","first-page":"22","volume-title":"24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019","author":"Bouwman Mark","year":"2019","unstructured":"Mark Bouwman, Bob Janssen, and Bas Luttik. 2019. Formal modelling and verification of an interlocking using mCRL2. In 24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019. 22\u201339."},{"key":"e_1_3_3_9_2","first-page":"42","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, held as part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14\u201318, 2021, Proceedings (Lecture Notes in Computer Science)","volume":"12719","author":"Bouwman Mark","year":"2021","unstructured":"Mark Bouwman, Bas Luttik, and Djurre van der Wal. 2021. A formalisation of SysML state machines in mCRL2. In Formal Techniques for Distributed Objects, Components, and Systems - 41st IFIP WG 6.1 International Conference, FORTE 2021, held as part of the 16th International Federated Conference on Distributed Computing Techniques, DisCoTec 2021, Valletta, Malta, June 14\u201318, 2021, Proceedings (Lecture Notes in Computer Science), Kirstin Peters and Tim A. C. Willemse (Eds.), Vol. 12719. Springer, 42\u201359. 10.1007\/978-3-030-78089-0_3"},{"doi-asserted-by":"publisher","key":"e_1_3_3_10_2","DOI":"10.1007\/s00236-020-00371-w"},{"key":"e_1_3_3_11_2","first-page":"921","volume-title":"Proceedings of ESREL2020-PSAM15","author":"Bouwman Mark","year":"2020","unstructured":"Mark Bouwman, Djurre van der Wal, Bas Luttik, Mari\u00eblle Stoelinga, and Arend Rensink. 2020. What is the point: Formal analysis and test generation for a railway standard. In Proceedings of ESREL2020-PSAM15, Piero Baraldi, Francesco Di Maio, and Enrico Zio (Eds.). Research Publishing, Singapore, 921\u2013928. 10.3850\/978-981-14-8593-0_4410-cd"},{"key":"e_1_3_3_12_2","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1109\/CMPSAC.2002.1044538","volume-title":"Proceedings 26th Annual International Computer Software and Applications","author":"Bowen J. P.","year":"2002","unstructured":"J. P. Bowen, K. Bogdanov, J. A. Clark, M. Harman, R. M. Hierons, and P. Krause. 2002. FORTEST: Formal methods and testing. In Proceedings 26th Annual International Computer Software and Applications. 91\u2013104."},{"doi-asserted-by":"publisher","key":"e_1_3_3_13_2","DOI":"10.1007\/978-3-540-27863-4_21"},{"doi-asserted-by":"publisher","key":"e_1_3_3_14_2","DOI":"10.1007\/11901914_30"},{"key":"e_1_3_3_15_2","first-page":"21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings, Part II (Lecture Notes in Computer Science)","volume":"11428","author":"Bunte Olav","year":"2019","unstructured":"Olav Bunte, Jan Friso Groote, Jeroen J. A. Keiren, Maurice Laveaux, Thomas Neele, Erik P. de Vink, Wieger Wesselink, Anton Wijs, and Tim A. C. Willemse. 2019. The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6\u201311, 2019, Proceedings, Part II (Lecture Notes in Computer Science), Tom\u00e1s Vojnar and Lijun Zhang (Eds.), Vol. 11428. Springer, 21\u201339. 10.1007\/978-3-030-17465-1_2"},{"doi-asserted-by":"publisher","key":"e_1_3_3_16_2","DOI":"10.1007\/s11334-011-0170-3"},{"doi-asserted-by":"publisher","key":"e_1_3_3_17_2","DOI":"10.1007\/978-3-642-15228-3"},{"doi-asserted-by":"publisher","key":"e_1_3_3_18_2","DOI":"10.1007\/978-3-319-05032-4"},{"doi-asserted-by":"publisher","key":"e_1_3_3_19_2","DOI":"10.1007\/s10009-014-0342-1"},{"issue":"2","key":"e_1_3_3_20_2","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10009-012-0244-z","article-title":"CADP 2011: A toolbox for the construction and analysis of distributed processes","volume":"15","author":"Garavel Hubert","year":"2013","unstructured":"Hubert Garavel, Fr\u00e9d\u00e9ric Lang, Radu Mateescu, and Wendelin Serwe. 2013. CADP 2011: A toolbox for the construction and analysis of distributed processes. International Journal on Software Tools for Technology Transfer 15, 2 (2013), 89\u2013107.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"e_1_3_3_21_2","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"Groote Jan Friso","year":"2014","unstructured":"Jan Friso Groote and Mohammad Reza Mousavi. 2014. Modeling and Analysis of Communicating Systems. MIT Press. https:\/\/mitpress.mit.edu\/books\/modeling-and-analysis-communicating-systems."},{"doi-asserted-by":"publisher","key":"e_1_3_3_22_2","DOI":"10.1016\/S1567-8326(01)00005-4"},{"key":"e_1_3_3_23_2","first-page":"141","volume-title":"Monterey\u201908 Proceedings of the 15th Monterey Conference on Foundations of Computer Software: Future Trends and Techniques for Development","author":"Haxthausen Anne E.","year":"2008","unstructured":"Anne E. Haxthausen, Marie Le Bliguet, and Andreas A. Kj \\({æ}\\) r. 2008. Modelling and verification of relay interlocking systems. In Monterey\u201908 Proceedings of the 15th Monterey Conference on Foundations of Computer Software: Future Trends and Techniques for Development. 141\u2013153."},{"doi-asserted-by":"publisher","key":"e_1_3_3_24_2","DOI":"10.1007\/978-3-658-09994-7_4"},{"issue":"2","key":"e_1_3_3_25_2","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s00165-009-0143-6","article-title":"A formal approach for the construction and verification of railway control systems","volume":"23","author":"Haxthausen Anne E.","year":"2011","unstructured":"Anne E. Haxthausen, Jan Peleska, and Sebastian Kinder. 2011. A formal approach for the construction and verification of railway control systems. Formal Aspects of Computing 23, 2 (2011), 191\u2013219.","journal-title":"Formal Aspects of Computing"},{"issue":"2","key":"e_1_3_3_26_2","first-page":"9","article-title":"Using formal specifications to support testing","volume":"41","author":"Hierons Robert M.","year":"2009","unstructured":"Robert M. Hierons, Kirill Bogdanov, Jonathan P. Bowen, Rance Cleaveland, John Derrick, Jeremy Dick, Marian Gheorghe, Mark Harman, Kalpesh Kapoor, Paul Krause, Gerald L\u00fcttgen, Anthony J. H. Simons, Sergiy Vilkomir, Martin R. Woodward, and Hussein Zedan. 2009. Using formal specifications to support testing. Comput. Surveys 41, 2 (2009), 9.","journal-title":"Comput. Surveys"},{"doi-asserted-by":"publisher","key":"e_1_3_3_27_2","DOI":"10.1007\/s10009-014-0304-7"},{"doi-asserted-by":"publisher","key":"e_1_3_3_28_2","DOI":"10.1109\/TSE.2010.62"},{"key":"e_1_3_3_29_2","first-page":"2","volume-title":"Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014, Grenoble, France, 5th April 2014 (EPTCS)","volume":"159","author":"Kant Gijs","year":"2014","unstructured":"Gijs Kant and Jaco van de Pol. 2014. Generating and solving symbolic parity games. In Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014, Grenoble, France, 5th April 2014 (EPTCS), Dragan Bosnacki, Stefan Edelkamp, Alberto Lluch-Lafuente, and Anton Wijs (Eds.), Vol. 159. 2\u201314. 10.4204\/EPTCS.159.2"},{"key":"e_1_3_3_30_2","first-page":"344","volume-title":"Proceedings of 12th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2007, September 25\u201328, 2007, Patras, Greece","author":"Linhares Marcos Vinicius","year":"2007","unstructured":"Marcos Vinicius Linhares, R\u00f4mulo Silva de Oliveira, Jean-Marie Farines, and Fran\u00e7ois Vernadat. 2007. Introducing the modeling and verification process in SysML. In Proceedings of 12th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2007, September 25\u201328, 2007, Patras, Greece. IEEE, 344\u2013351. 10.1109\/EFTA.2007.4416788"},{"key":"e_1_3_3_31_2","volume-title":"Efficient Learning and Analysis of System Behavior","author":"Meijer Jeroen Johan Gerardus","year":"2019","unstructured":"Jeroen Johan Gerardus Meijer. 2019. Efficient Learning and Analysis of System Behavior. Ph.D. Dissertation. University of Twente."},{"key":"e_1_3_3_32_2","first-page":"92","volume-title":"International Symposium on Systems Engineering (ISSE)","author":"Morkevicius Aurelijus","year":"2015","unstructured":"Aurelijus Morkevicius and Nerijus Jankevicius. 2015. An approach: SysML-based automated requirements verification. In International Symposium on Systems Engineering (ISSE). IEEE, 92\u201397."},{"doi-asserted-by":"crossref","unstructured":"Object Management Group. 2017. OMG Unified Modeling Language version 2.5.1. (2017). https:\/\/www.omg.org\/spec\/UML\/.","key":"e_1_3_3_33_2","DOI":"10.1016\/B978-1-78548-171-0.50001-3"},{"unstructured":"Object Management Group. 2019. OMG Systems Modeling Language version 1.6. (2019). https:\/\/www.omg.org\/spec\/SysML\/.","key":"e_1_3_3_34_2"},{"key":"e_1_3_3_35_2","first-page":"1","volume-title":"11th Annual International Conference on New Technologies of Distributed Systems, NOTERE 2011, Paris, France, 9\u201313 May 2011","author":"Pedroza Gabriel","year":"2011","unstructured":"Gabriel Pedroza, Ludovic Apvrille, and Daniel Knorreck. 2011. AVATAR: A SysML environment for the formal verification of safety and security properties. In 11th Annual International Conference on New Technologies of Distributed Systems, NOTERE 2011, Paris, France, 9\u201313 May 2011, Isabelle M. Demeure, Thomas Robert, and Ahmed Serhrouchni (Eds.). IEEE, 1\u201310. 10.1109\/NOTERE.2011.5957992"},{"key":"e_1_3_3_36_2","volume-title":"22nd International Conference on Software & Systems Engineering and their Applications","author":"P\u00e9tin Jean-Fran\u00e7ois","year":"2010","unstructured":"Jean-Fran\u00e7ois P\u00e9tin, Dominique Evrot, G\u00e9rard Morel, and Pascal Lamy. 2010. Combining SysML and formal methods for safety requirements verification. In 22nd International Conference on Software & Systems Engineering and their Applications."},{"key":"e_1_3_3_37_2","first-page":"214","volume-title":"Proceedings of the 7th International Conference on Tests And Proofs (TAP) (Lecture Notes in Computer Science)","volume":"7942","author":"Stokkink W. G. J.","year":"2013","unstructured":"W. G. J. Stokkink, M. Timmer, and M. I. A. Stoelinga. 2013. Divergent quiescent transition systems. In Proceedings of the 7th International Conference on Tests And Proofs (TAP) (Lecture Notes in Computer Science), Margus Veanes and Luca Vigan\u00f2 (Eds.), Vol. 7942. Springer, 214\u2013231. 10.1007\/978-3-642-38916-0_13"},{"key":"e_1_3_3_38_2","series-title":"NATO Science for Peace and Security Series - D: Information and Communication Security","first-page":"1","volume-title":"Software and Systems Safety - Specification and Verification","author":"Timmer M.","year":"2011","unstructured":"M. Timmer, H. Brinksma, and M. I. A. Stoelinga. 2011. Model-based testing. In Software and Systems Safety - Specification and Verification. NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 30. IOS Press, 1\u201332. 10.3233\/978-1-60750-711-6-1"},{"key":"e_1_3_3_39_2","first-page":"31","article-title":"TorX: Automated model-based testing","author":"Tretmans G. J.","year":"2003","unstructured":"G. J. Tretmans and Hendrik Brinksma. 2003. TorX: Automated model-based testing. First European Conference on Model-Driven Software Engineering (2003), 31\u201343.","journal-title":"First European Conference on Model-Driven Software Engineering"},{"issue":"3","key":"e_1_3_3_40_2","first-page":"103","article-title":"Test generation with inputs, outputs and repetitive quiescence","volume":"17","author":"Tretmans Jan","year":"1996","unstructured":"Jan Tretmans. 1996. Test generation with inputs, outputs and repetitive quiescence. Softw. Concepts Tools 17, 3 (1996), 103\u2013120.","journal-title":"Softw. Concepts Tools"},{"key":"e_1_3_3_41_2","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Formal Methods and Testing, An Outcome of the FORTEST Network, Revised Selected Papers","author":"Tretmans Jan","year":"2008","unstructured":"Jan Tretmans. 2008. Model based testing with labelled transition systems. In Formal Methods and Testing, An Outcome of the FORTEST Network, Revised Selected Papers, Robert M. Hierons, Jonathan P. Bowen, and Mark Harman (Eds.). Lecture Notes in Computer Science, Vol. 4949. Springer, 1\u201338. 10.1007\/978-3-540-78917-8_1"},{"issue":"5","key":"e_1_3_3_42_2","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1002\/stvr.456","article-title":"A taxonomy of model-based testing approaches","volume":"22","author":"Utting Mark","year":"2012","unstructured":"Mark Utting, Alexander Pretschner, and Bruno Legeard. 2012. A taxonomy of model-based testing approaches. Software Testing, Verification & Reliability 22, 5 (2012), 297\u2013312.","journal-title":"Software Testing, Verification & Reliability"},{"key":"e_1_3_3_43_2","first-page":"64","volume-title":"Tests and Proofs - 13th International Conference, TAP@FM 2019, Porto, Portugal, October 9\u201311, 2019, Proceedings (Lecture Notes in Computer Science)","volume":"11823","author":"Bos Petra van den","year":"2019","unstructured":"Petra van den Bos and Jan Tretmans. 2019. Coverage-based testing with symbolic transition systems. In Tests and Proofs - 13th International Conference, TAP@FM 2019, Porto, Portugal, October 9\u201311, 2019, Proceedings (Lecture Notes in Computer Science), Dirk Beyer and Chantal Keller (Eds.), Vol. 11823. Springer, 64\u201382. 10.1007\/978-3-030-31157-5_5"},{"doi-asserted-by":"publisher","key":"e_1_3_3_44_2","DOI":"10.1145\/3329125"},{"key":"e_1_3_3_45_2","article-title":"Electric signalling systems for railways - Part200: Safe transmission protocol according to DIN EN50159 (DIN VDE V 0831-159)","year":"2015","unstructured":"VDE. 2015. Electric signalling systems for railways - Part200: Safe transmission protocol according to DIN EN50159 (DIN VDE V 0831-159). DIN VDE V 0831-200. (62015).","journal-title":"DIN VDE V 0831-200"},{"unstructured":"Wikimedia Commons. 2021. File:Facing points Broomhill.jpg. (2021). https:\/\/commons.wikimedia.org\/wiki\/File:Facing_points_Broomhill.jpg. [Online; accessed July 9 2021].","key":"e_1_3_3_46_2"},{"issue":"4","key":"e_1_3_3_47_2","doi-asserted-by":"crossref","first-page":"2614","DOI":"10.1109\/JSYST.2015.2496293","article-title":"Perceptions on the state of the art in verification and validation in cyber-physical systems","volume":"11","author":"Zheng Xi","year":"2017","unstructured":"Xi Zheng, Christine Julien, Miryung Kim, and Sarfraz Khurshid. 2017. Perceptions on the state of the art in verification and validation in cyber-physical systems. IEEE Systems Journal 11, 4 (2017), 2614\u20132627.","journal-title":"IEEE Systems Journal"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3528207","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,16]],"date-time":"2023-03-16T12:07:00Z","timestamp":1678968420000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3528207"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,3,16]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3,31]]}},"alternative-id":["10.1145\/3528207"],"URL":"https:\/\/doi.org\/10.1145\/3528207","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2023,3,16]]},"assertion":[{"value":"2021-07-12","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-03-17","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-03-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}