{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T23:26:31Z","timestamp":1742945191238,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030309411"},{"type":"electronic","value":"9783030309428"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30942-8_9","type":"book-chapter","created":{"date-parts":[[2019,9,22]],"date-time":"2019-09-22T23:03:06Z","timestamp":1569193386000},"page":"121-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Synthesis of Railway Signaling Layout from Local Capacity Specifications"],"prefix":"10.1007","author":[{"given":"Bj\u00f8rnar","family":"Luteberget","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christian","family":"Johansen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,9,23]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Abril, M., Barber, F., Ingolotti, L., Salido, M., Tormos, P., Lova, A.: An assessment of railway capacity. Transp. Res. Part E: Logistics Transp. Rev. 44(5), 774\u2013806 (2008). \nhttps:\/\/doi.org\/10.1016\/j.tre.2007.04.001","DOI":"10.1016\/j.tre.2007.04.001"},{"key":"9_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-98938-9_2","volume-title":"Integrated Formal Methods","author":"D Basile","year":"2018","unstructured":"Basile, D., et al.: On the industrial uptake of formal methods in the railway domain. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 20\u201329. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-98938-9_2"},{"issue":"11","key":"9_CR3","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Adv. Comput. 58(11), 117\u2013148 (2003). \nhttps:\/\/doi.org\/10.1016\/S0065-2458(03)58003-2","journal-title":"Adv. Comput."},{"key":"9_CR4","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)"},{"key":"9_CR5","unstructured":"Bj\u00f6rk, M.: Successful SAT encoding techniques. J. Sat. Boolean Model. Comput. 7(4), 189\u2013201 (2011). \nhttps:\/\/satassociation.org\/jsat\/index.php\/jsat\/article\/view\/153\/118"},{"key":"9_CR6","doi-asserted-by":"publisher","unstructured":"Bor\u00e4lv, A., St\u00e5lmarck, G.: Formal verification in railways. In: Hinchey, M.G., Bowen, J.P. (eds.) Industrial-Strength Formal Methods in Practice, pp. 329\u2013350. Springer (1999), \nhttps:\/\/doi.org\/10.1007\/978-1-4471-0523-7_15","DOI":"10.1007\/978-1-4471-0523-7_15"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Boulanger, J.L.: CENELEC 50128 and IEC 62279 Standards. Wiley-ISTE, March 2015","DOI":"10.1002\/9781119005056"},{"key":"9_CR8","volume-title":"Algorithms for Minimization Without Derivatives","author":"RP Brent","year":"2002","unstructured":"Brent, R.P.: Algorithms for Minimization Without Derivatives. Dover Publications, Mineola (2002)"},{"issue":"1\u20132","key":"9_CR9","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1016\/j.jrtpm.2012.10.001","volume":"2","author":"T B\u00fcker","year":"2012","unstructured":"B\u00fcker, T., Seybold, B.: Stochastic modelling of delay propagation in large networks. J. Rail Transp. Plan. Manag. 2(1\u20132), 34\u201350 (2012). \nhttps:\/\/doi.org\/10.1016\/j.jrtpm.2012.10.001","journal-title":"J. Rail Transp. Plan. Manag."},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-642-31424-7_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2012","unstructured":"Cimatti, A., et al.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378\u2013393. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-31424-7_29"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-18744-6_5","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"S Dillmann","year":"2019","unstructured":"Dillmann, S., H\u00e4hnle, R.: Automated planning of ETCS tracks. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 79\u201390. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-18744-6_5"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-319-05032-4_13","volume-title":"Software Engineering and Formal Methods","author":"A Fantechi","year":"2014","unstructured":"Fantechi, A.: Twenty-five years of formal methods and railways: what next? In: Counsell, S., N\u00fa\u00f1ez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 167\u2013183. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-05032-4_13"},{"key":"9_CR13","unstructured":"Hansen, I.A., Pachl, J.: Railway Timetabling and Operations. Eurailpress (2014)"},{"key":"9_CR14","unstructured":"Harris, T., Ross, F.S.: Fundamentals of a method for evaluating rail net capacities. Technical report, RM-1573, Rand Corporation (1955)"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Hartonas-Garmhausen, V., Campos, S.V.A., Cimatti, A., Clarke, E.M., Giunchiglia, F.: Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Program. 36(1), 53\u201364 (2000). \nhttps:\/\/doi.org\/10.1016\/S0167-6423(99)00016-7","DOI":"10.1016\/S0167-6423(99)00016-7"},{"issue":"2","key":"9_CR16","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00165-009-0143-6","volume":"23","author":"AE Haxthausen","year":"2011","unstructured":"Haxthausen, A.E., Peleska, J., Kinder, S.: A formal approach for the construction and verification of railway control systems. Formal Aspects Comput. 23(2), 191\u2013219 (2011). \nhttps:\/\/doi.org\/10.1007\/s00165-009-0143-6","journal-title":"Formal Aspects Comput."},{"key":"9_CR17","unstructured":"H\u00fcrlimann, D.: Objektorientierte Modellierung von Infrastrukturelementen und Betriebsvorg\u00e4ngen im Eisenbahnwesen. Ph.D. thesis, ETH Zurich (2002). \nhttps:\/\/www.research-collection.ethz.ch\/handle\/20.500.11850\/47957"},{"key":"9_CR18","doi-asserted-by":"publisher","unstructured":"Kamburjan, E., H\u00e4hnle, R., Sch\u00f6n, S.: Formal modeling and analysis of railway operations with active objects. Sci. Comput. Program. 166, 167\u2013193 (2018). \nhttps:\/\/doi.org\/10.1016\/j.scico.2018.07.001","DOI":"10.1016\/j.scico.2018.07.001"},{"key":"9_CR19","unstructured":"Landex, A.: Methods to estimate railway capacity and passenger delays. Ph.D. thesis, Technical University of Denmark (DTU) (2008). \nhttps:\/\/orbit.dtu.dk\/en\/publications\/id(f5578206-74c3-4c94-ba0d-43f7da82bf95).html"},{"key":"9_CR20","unstructured":"Luteberget, B.: Automated Reasoning for Planning Railway Infrastructure. Ph.D. thesis, Faculty of Mathematics and Natural Sciences, University of Oslo (2019)"},{"key":"9_CR21","doi-asserted-by":"publisher","unstructured":"Luteberget, B., Claessen, K., Johansen, C.: Design-time railway capacity verification using SAT modulo discrete event simulation. In: Bj\u00f8rner, N., Gurfinkel, A. (eds.) Formal Methods in Computer Aided Design (FMCAD), pp. 1\u20139. IEEE (2018). \nhttps:\/\/doi.org\/10.23919\/FMCAD.2018.8603003","DOI":"10.23919\/FMCAD.2018.8603003"},{"issue":"1","key":"9_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-017-0281-z","volume":"52","author":"B Luteberget","year":"2018","unstructured":"Luteberget, B., Johansen, C.: Efficient verification of railway infrastructure designs against standard regulations. Formal Methods Syst. Des. 52(1), 1\u201332 (2018). \nhttps:\/\/doi.org\/10.1007\/s10703-017-0281-z","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1007\/978-3-319-48989-6_49","volume-title":"FM 2016: Formal Methods","author":"B Luteberget","year":"2016","unstructured":"Luteberget, B., Johansen, C., Feyling, C., Steffen, M.: Rule-based incremental verification tools applied to railway designs and regulations. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 772\u2013778. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-48989-6_49"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-319-33693-0_31","volume-title":"Integrated Formal Methods","author":"B Luteberget","year":"2016","unstructured":"Luteberget, B., Johansen, C., Steffen, M.: Rule-based consistency checking of railway infrastructure designs. In: \u00c1brah\u00e1m, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 491\u2013507. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-33693-0_31"},{"issue":"1","key":"9_CR25","first-page":"35","volume":"13","author":"B Mao","year":"2006","unstructured":"Mao, B., Liu, J., Ding, Y., Liu, H., Ho, T.K.: Signalling layout for fixed-block railway lines with real-coded genetic algorithms. Hong Kong Inst. Eng. Trans. 13(1), 35\u201340 (2006). \nhttps:\/\/eprints.qut.edu.au\/38260\/","journal-title":"Hong Kong Inst. Eng. Trans."},{"key":"9_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-40065-5","volume-title":"Numerical Optimization","author":"J Nocedal","year":"2006","unstructured":"Nocedal, J., Wright, S.J.: Numerical Optimization, 2nd edn. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/978-0-387-40065-5","edition":"2"},{"key":"9_CR27","unstructured":"Pachl, J.: Railway Operation and Control. VTD Rail Publishing (2015)"},{"key":"9_CR28","volume-title":"Simulation: The Practice of Model Development and Use","author":"S Robinson","year":"2004","unstructured":"Robinson, S.: Simulation: The Practice of Model Development and Use. John Wiley & Sons Inc., New York (2004)"},{"key":"9_CR29","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for railway interlocking systems. In: Schnieder, E., Tarnai, G. (eds.) Proceedings of the 10th Symposium on Formal Methods for Automation and Safety in Railway and Automotive Systems, (FORMS\/FORMAT). pp. 200\u2013209. TU Braunschweig (2014)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods \u2013 The Next 30 Years"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30942-8_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,5]],"date-time":"2020-05-05T06:06:25Z","timestamp":1588658785000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30942-8_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309411","9783030309428"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30942-8_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"23 September 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2019.inesctec.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"129","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"44","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"34% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5,5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}