{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,26]],"date-time":"2025-06-26T10:27:58Z","timestamp":1750933678290,"version":"3.40.3"},"publisher-location":"Wiesbaden","reference-count":33,"publisher":"Springer Fachmedien Wiesbaden","isbn-type":[{"type":"print","value":"9783658099930"},{"type":"electronic","value":"9783658099947"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-658-09994-7_4","type":"book-chapter","created":{"date-parts":[[2015,6,5]],"date-time":"2015-06-05T07:56:17Z","timestamp":1433490977000},"page":"82-121","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Model Checking and Model-Based Testing in the Railway Domain"],"prefix":"10.1007","author":[{"given":"Anne E.","family":"Haxthausen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Peleska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,6,6]]},"reference":[{"key":"4_CR1","unstructured":"M. Aanffis and H. P. Thai. Modelling and Verification of Relay Interlocking Systems. Master\u2019s thesis, Technical University of Denmark, DTU Informatics, E-mail: reception@imm.dtu.dk, 2012."},{"key":"4_CR2","first-page":"541","volume":"14","author":"Babcsanyi Istvan","year":"2000","unstructured":"Istvan Babcsanyi. Equivalence of Mealy and Moore Automata. Acta Cybernetica, 14:541\u2013552, 2000.","journal-title":"Acta Cybernetica"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Patrick Behm, Paul Benoit, Alain Faivre, and Jean-Marc Meynadier. Meteor: A successful application of b in a large project. In J. Wing, J. Woodcock, and J. Davies, editors, FM\u201999 \u2013 Formal Methods, volume\u00a01708 of Lecture Notes in Computer Science, pages 369\u2013387, Berlin Heidelberg, 1999. Springer.","DOI":"10.1007\/3-540-48119-2_22"},{"key":"4_CR4","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS \u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999","author":"Biere Armin","year":"1999","unstructured":"Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic Model Checking without BDDs. In Rance Cleaveland, editor, Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS \u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, volume\u00a01579 of Lecture Notes in Computer Science, pages 193-207. Springer, 1999."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Armin Biere, Keijo Heljanko, Tommi Junttila, Timo Latvala, and Viktor Schuppan. Linear encodings of bounded LTL model checking. Logical Methods in ComputerScience, 2(5), November 2006. arXiv: cs\/0611029.","DOI":"10.2168\/LMCS-2(5:5)2006"},{"key":"4_CR6","unstructured":"Dines Bjprner. New Results and Current Trends in Formal Techniques for the Development of Software for Transportation Systems. In Proceedings of the Symposium on Formal Methods for Railway Operation and Control Systems (FORMS\u20192003), Budapest\/Hungary. L\u2019Harmattan Hongrie, May 15-16 2003."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Cecile Braunstein, Anne E. Haxthausen, Wen ling Huang, Felix Hubner, Jan Pe- leska, Uwe Schulze, and Linh Hong Vu. Complete model-based equivalence class testing for the ETCS ceiling speed monitor. In S. Merz and J. Pang, editors, Proceedings of the ICFEM 2014, volume\u00a08829 of Lecture Notes in Computer Science, pages 380\u2013395. Springer Berlin Heidelberg, November 2014.","DOI":"10.1007\/978-3-319-11737-9_25"},{"key":"4_CR8","unstructured":"C\u00e9cile Braunstein, Wen-ling Huang, Jan Peleska, Uwe Schulze, Felix H\u00fcbner, Anne E. Haxthausen, and Linh Hong Vu. A SysML test model and test suite for the ETCS ceiling speed monitor. Technical report, Embedded Systems Testing Benchmarks Site, 2014-04-30. Available under http:\/\/www.mbt-benchmarks.org."},{"key":"4_CR9","volume-title":"Model Checking","author":"Edmund M. Clarke","year":"1999","unstructured":"Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura, Harald Rue\u00df, and Maria Sorea. Bounded Model Checking and Induction: From Refutation to Verification. In Computer Aided Verification, pages 14\u201326. Springer, 2003.","DOI":"10.1007\/978-3-540-45069-6_2"},{"key":"4_CR11","unstructured":"Ulrich W. Eisenecker and Krzysztof Czarnecki. Generative Programming: Methods, Tools, and Applications. Addison-Wesley, 2000."},{"key":"4_CR12","unstructured":"ERTMS. Annex A for ETCS Baseline 3 and GSM-R Baseline 0, April 2012."},{"key":"4_CR13","unstructured":"CENELEC European Committee for Electrotechnical Standardization. EN 50128:2011 \u2013 Railway applications \u2013 Communications, signalling and processing systems \u2013 Software for railway control and protection systems. 2011."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Alessandro Fantechi. Twenty-Five Years of Formal Methods and Railways: What Next? In Steve Counsell and Manuel Nunez, editors, Software Engineering and Formal Methods, volume\u00a08368 of Lecture Notes in Computer Science, pages 167183. Springer, 2014.","DOI":"10.1007\/978-3-319-05032-4_13"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Alessio Ferrari, Gianluca Magnani, Daniele Grasso, and Alessandro Fantechi. Model Checking Interlocking Control Tables. In Eckehard Schnieder and Geza Tarnai, editors, FORMS\/FORMAT 2010 \u2013 Formal Methods for Automation and Safety in Railway and Automotive Systems, pages 107\u2013115. Springer, 2010.","DOI":"10.1007\/978-3-642-14261-1_11"},{"issue":"8","key":"4_CR16","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1109\/32.879808","volume":"26","author":"A. E. Haxthausen","year":"2000","unstructured":"A. E. Haxthausen and J. Peleska. Formal Development and Verification of a Distributed Railway Control System. IEEE Transaction on Software Engineering, 26(8):687\u2013701, 2000.","journal-title":"IEEE Transaction on Software Engineering"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"Anne E. Haxthausen. Automated Generation of Formal Safety Conditions from Railway Interlocking Tables. International Journal on Software Tools for Technology Transfer (STTT), Special Issue on Formal Methods for Railway Control Systems, 16(6):713\u2013726, 2014.","DOI":"10.1007\/s10009-013-0295-9"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Anne E. Haxthausen, Marie Le Bliguet, and Andreas A. Kjffir. Modelling and Verification of Relay Interlocking Systems. In Christine Choppy and Oleg Sokol- sky, editors, 15th Monterey Workshop: Foundations of Computer Software, Future Trends and Techniques for Development, number 6028 in Lecture Notes in Computer Science, pages 141\u2013153. Springer, 2010. Invited paper.","DOI":"10.1007\/978-3-642-12566-9_8"},{"key":"4_CR19","unstructured":"Anne E. Haxthausen and Jan Peleska. Efficient Development and Verification of Safe Railway Control Software. In Railways: Types, Design and Safety Issues, pages 127\u2013148. Nova Science Publishers, Inc., 2013."},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Anne E. Haxthausen, Jan Peleska, and Sebastian Kinder. A Formal Approach for the Construction and Verification of Railway Control Systems. In Formal Aspects of Computing, volume\u00a023, pages 191\u2013219. Springer, 2011.","DOI":"10.1007\/s00165-009-0143-6"},{"key":"4_CR21","unstructured":"Wen-ling Huang and Jan Peleska. Complete model-based equivalence class testing. International Journal on Software Tools for Technology Transfer, pages 1\u201319, 2014."},{"key":"4_CR22","unstructured":"Phillip James and Markus Roggenbach. Automatically Verifying Railway Interlockings Using SAT-based Model Checking. In Electronic Communications of the EASST, volume\u00a035. EASST, 2011."},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"Helge Loding and Jan Peleska. Timed moore automata: test data generation and model checking. In Proc. 3rd International Conference on Software Testing, Verification and Validation (ICST\u201910). IEEE Computer Society, 2010.","DOI":"10.1109\/ICST.2010.60"},{"key":"4_CR24","unstructured":"Kirsten Mewes. Domain-specific Modelling of Railway Control Systems with Integrated Verification and Validation. PhD thesis, University of Bremen, 2010. http:\/\/www.dr.hut-verlag.de\/978-3-86853-359-0.html."},{"key":"4_CR25","volume-title":"Proceedings 8th Workshop on Model-Based Testing","author":"Jan Peleska. Industrial-Strength Model-Based Testing \u2013 State of the Art and Current Challenges","year":"2013","unstructured":"Jan Peleska. Industrial-Strength Model-Based Testing \u2013 State of the Art and Current Challenges. In Alexander K. Petrenko and Holger Schlingloff, editors, Proceedings 8th Workshop on Model-Based Testing, Rome, Italy, volume\u00a0111 of Electronic Proceedings in Theoretical Computer Science, pages 3-28. Open Publishing Association, 2013."},{"key":"4_CR26","unstructured":"Jan Peleska, Daniel Gro\u00dfe, Anne E. Haxthausen, and Rolf Drechsler. Automated verification for train control systems. In E. Schnieder and G. Tarnai, editors, Formal Methods for Automation and Safety in Railway and Automotive Systems, Braunschweig, Germany, December, 2004, pages 252-265. Technical University of Braunschweig, ISBN 3-9803363-8-7, 2004."},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Jan Peleska, Artur Honisch, Florian Lapschies, Helge L\u00f6ding, Hermann Schmid, Peer Smuda, Elena Vorobev, and Cornelia Zahlten. A real-world benchmark model for testing concurrent real-time systems in the automotive domain. In Burkhart Wolff and Fatiha Zaidi, editors, Testing Software and Systems. Proceedings of the 23rd IFIP WG 6.1 International Conference, ICTSS 2011, volume\u00a07019 of LNCS, pages 146\u2013161, Heidelberg Dordrecht London New York, November 2011. IFIP WG 6.1, Springer.","DOI":"10.1007\/978-3-642-24580-0_11"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Jan Peleska, Elena Vorobev, and Florian Lapschies. Automated test case generation with SMT-solving and abstract interpretation. In Mihaela Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, Nasa Formal Methods, Third International Symposium, NFM 2011, volume\u00a06617 of LNCS, pages 298\u2013312, Pasadena, CA, USA, April 2011. Springer.","DOI":"10.1007\/978-3-642-20398-5_22"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"A. Petrenko, N. Yevtushenko, and G. v. Bochmann. Fault models for testing in context. In Reinhard Gotzhein and Jan Bredereke, editors, Formal Description Techniques IX \u2013 Theory, application and tools, pages 163\u2013177. Chapman & Hall, 1996.","DOI":"10.1007\/978-0-387-35079-0_10"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Mary Sheeran, Satnam Singh, and Gunnar Stalmarck. Checking safety properties using induction and a SAT-solver. In Jr. Hunt, Warren A. and Steven D. Johnson, editors, Formal Methods in Computer-Aided Design, volume\u00a01954 of Lecture Notes in Computer Science, pages 127\u2013144. Springer Berlin Heidelberg, 2000.","DOI":"10.1007\/3-540-40922-X_8"},{"issue":"1\u20132","key":"4_CR31","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/S0304-3975(99)00134-6","volume":"254","author":"J.G. Springintveld","year":"2001","unstructured":"J.G. Springintveld, F.W. Vaandrager, and P.R. D\u2019Argenio. Testing timed automata. Theoretical Computer Science, 254(1\u20132):225\u2013257, March 2001.","journal-title":"Theoretical Computer Science"},{"key":"4_CR32","unstructured":"Linh Hong Vu, Anne E. Haxthausen, and Jan Peleska. A Domain-Specific Language for Railway Interlocking Systems. In Eckehard Schnieder and Geza Tarnai, editors, FORMS\/FORMAT 2014 \u2013 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, pages 200-209. Institute for Traffic Safety and Automation Engineering, Technische Universit\u00f6at Braunschweig, 2014."},{"key":"4_CR33","unstructured":"Linh Hong Vu, Anne E. Haxthausen, and Jan Peleska. Formal Modeling and Verification of Interlocking Systems Featuring Sequential Release. In Formal Techniques for Safety-Critical Systems, volume\u00a0476 of Communications in Computer and Information Science. Springer International Publishing Switzerland, 2015."}],"container-title":["Formal Modeling and Verification of Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-658-09994-7_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T11:47:27Z","timestamp":1676461647000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-658-09994-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783658099930","9783658099947"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-658-09994-7_4","relation":{},"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"6 June 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}