{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T19:26:31Z","timestamp":1776885991861,"version":"3.51.2"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319577074","type":"print"},{"value":"9783319577081","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-57708-1_10","type":"book-chapter","created":{"date-parts":[[2017,4,20]],"date-time":"2017-04-20T08:03:37Z","timestamp":1492675417000},"page":"160-177","source":"Crossref","is-referenced-by-count":7,"title":["Applying SOFL to a Railway Interlocking System in Industry"],"prefix":"10.1007","author":[{"given":"Juan","family":"Luo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaoying","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yanqin","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tingliang","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,21]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1109\/2.962984","volume":"34","author":"BW Boehm","year":"2001","unstructured":"Boehm, B.W., Basili, V.R.: Software defect reduction top 10 list. IEEE Comput. 34(1), 135\u2013137 (2001)","journal-title":"IEEE Comput."},{"issue":"4","key":"10_CR2","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1049\/sej.1993.0025","volume":"8","author":"J Bowen","year":"1993","unstructured":"Bowen, J., Stavridou, V.: Safety-critical methods and systems, formal standards. Softw. Eng. J. 8(4), 189\u2013209 (1993)","journal-title":"Softw. Eng. J."},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08766-4","volume-title":"The Vienna Development Method: The Meta-Language","year":"1978","unstructured":"Bj\u00f8rner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978). doi: 10.1007\/3-540-08766-4"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Diller, A.: Z: an introduction to formal methods 23(9), 10\u201323 (1990). Wiley","DOI":"10.1109\/2.58215"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Abrial, J.-R.: Modeling in Event-B System and Software Engineering. Cambridge University Press, Cambridge (2010), ISBN-13 978-0-521-89556-9","DOI":"10.1017\/CBO9781139195881"},{"key":"10_CR6","unstructured":"Efficient Development of Safe Railway Applications Software with EN 50128 Objectives Using SCADE Suite, 3rd edn.. Esterel Technologies, SA (2012)"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Liu, S.: Formal engineering for industrial software development using the SOFL method. Springer, Heidelberg (2004), ISBN 3-540-20602-7","DOI":"10.1007\/978-3-662-07287-5"},{"issue":"9","key":"10_CR8","doi-asserted-by":"publisher","first-page":"785","DOI":"10.1109\/32.159839","volume":"18","author":"N Halbwachs","year":"1992","unstructured":"Halbwachs, N., Lagnier, F., Ratel, C.: Programming and verifying real-time systems by means of the synchronous data-flow language LUSTR. IEEE Trans. Softw. Eng. 18(9), 785\u2013793 (1992)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"5","key":"10_CR9","doi-asserted-by":"publisher","first-page":"1100","DOI":"10.1109\/TSE.2011.102","volume":"38","author":"S Liu","year":"2012","unstructured":"Liu, S., Chen, Y., Nagoya, F., McDermid, J.A.: Formal specification-based inspection for verification of programs. IEEE Trans. Softw. Eng. 38(5), 1100\u20131122 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"10_CR10","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1016\/j.jss.2007.05.036","volume":"81","author":"S Liu","year":"2008","unstructured":"Liu, S., Chen, Y.: A relation-based method combining functional and structural testing for test case generation. J. Syst. Softw. 81(2), 234\u2013248 (2008)","journal-title":"J. Syst. Softw."},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Liu, S., Nakajima, S.: A decompositional approach to automatic test case generation based on formal specifications. In: 4th IEEE International Conference on Secure Software Integration and Reliability Improvement, Singapore, 9\u201311 June, pp. 147\u2013155 (2010)","DOI":"10.1109\/SSIRI.2010.11"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Liu, S., Nakajima, S: A \u201cVibration\u201d method for automatically generating test cases based on formal specifications. In: 18th Asia Pacific Conference on Software Engineering (APSEC 2011), 5\u20138 December, pp. 73\u201380. IEEE CS Press, VNU-HCM, Vietnam (2011)","DOI":"10.1109\/APSEC.2011.16"},{"issue":"8","key":"10_CR13","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1109\/32.879808","volume":"26","author":"AE Haxthausen","year":"2000","unstructured":"Haxthausen, A.E., Peleska, J.: Formal development and verification of a distributed railway control system. IEEE Trans. Softw. Eng. 26(8), 369\u2013387 (2000)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR14","unstructured":"DaSilva, C., Dehbonei, B., Mejia, F.: Formal specification in the development of industrial applications: subway speed control system. In: IFIP Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE), Perros-Guirec, France, 13\u201316 October, pp. 199\u2013213 (1992)"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 \u2014 Formal Methods","author":"P Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: a successful application of B in a large project. In: Wing, Jeannette M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369\u2013387. Springer, Heidelberg (1999). doi: 10.1007\/3-540-48119-2_22"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54108-7_14","volume-title":"Verified Software: Theories, Tools, Experiments","author":"L Zou","year":"2014","unstructured":"Zou, L., Lv, J., Wang, S., Zhan, N., Tang, T., Yuan, L., Liu, Yu.: Verifying Chinese train control system under a combined scenario by theorem proving. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 262\u2013280. Springer, Heidelberg (2014). doi: 10.1007\/978-3-642-54108-7_14"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Zou, L., Zhan, N., Franzle, M., Qin, S.: Verifying simulink diagrams via a hybrid hoare logic pover. In: International Conference on Embedded Software (EMSOFT), Montreal, QC, 29 September 2013\u20134 October 2013, pp. 1\u201310 (2013)","DOI":"10.1109\/EMSOFT.2013.6658587"},{"key":"10_CR18","unstructured":"Horste, M., Hungar, A., Schnieder, E.: Modelling functionality of train control systems using petri nets. In: FM-RAIL-BOK Workshop, Madrid, Spain, September 23\u201324, 2013, pp. 46\u201350 (2013)"},{"key":"10_CR19","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., Corvino, R., Lazzaro, A., Narasamdya, I., Rizzo, T., Roveri, M., Sanseviero, A., Tchaltsev, A.: Formal verification and validation of ERTMS industrial railway train spacing system. In: Madhusudan, P., Seshia, Sanjit A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 378\u2013393. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_29"},{"key":"10_CR20","unstructured":"Study cases of Prover technology, http:\/\/www.prover.com\/company\/casestudies\/"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Qian, J., Liu, J., Chen, X., Sun, J.: Formal design and verification of zone controller. In: 21st Asia-Pacific Conference on Software Engineering (APSEC 2014), 1\u20134 December 2014, pp. 375\u2013382. IEEE CS Press, Jeju (2014)","DOI":"10.1109\/APSEC.2014.62"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Qian, J., Liu, J., Chen, X., Sun, J.: Modeling and verification of zone controller: the SCADE experience in china\u2019s railway systems. In: ICSE Workshop on Complex Faults and Failures in Large Software Systems (COUFLESS), 23 May 2015, pp. 48\u201354. IEEE, Florence (2015)","DOI":"10.1109\/COUFLESS.2015.15"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-57708-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,21]],"date-time":"2019-09-21T07:23:35Z","timestamp":1569050615000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-57708-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319577074","9783319577081"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-57708-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}