{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T22:50:23Z","timestamp":1757544623683},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319684987"},{"type":"electronic","value":"9783319684994"}],"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-68499-4_5","type":"book-chapter","created":{"date-parts":[[2017,10,18]],"date-time":"2017-10-18T10:35:37Z","timestamp":1508322937000},"page":"71-86","source":"Crossref","is-referenced-by-count":8,"title":["Formal Modelling Techniques for Efficient Development of Railway Control Products"],"prefix":"10.1007","author":[{"given":"M.","family":"Butler","sequence":"first","affiliation":[]},{"given":"D.","family":"Dghaym","sequence":"additional","affiliation":[]},{"given":"T.","family":"Fischer","sequence":"additional","affiliation":[]},{"given":"T. S.","family":"Hoang","sequence":"additional","affiliation":[]},{"given":"K.","family":"Reichl","sequence":"additional","affiliation":[]},{"given":"C.","family":"Snook","sequence":"additional","affiliation":[]},{"given":"P.","family":"Tummeltshammer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,10,19]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York (2010)"},{"issue":"6","key":"5_CR2","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An open toolset for modelling and reasoning in Event-B. Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)","journal-title":"Softw. Tools Technol. Transf."},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/11526841_16","volume-title":"FM 2005: Formal Methods","author":"M Butler","year":"2005","unstructured":"Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 221\u2013236. Springer, Heidelberg (2005). doi:\n10.1007\/11526841_16"},{"unstructured":"The Enable-S3 Consortium. Enable-S3 European project (2016). \nwww.enable-s3.eu","key":"5_CR4"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-319-33600-8_20","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Dghaym","year":"2016","unstructured":"Dghaym, D., Trindade, M.G., Butler, M., Fathabadi, A.S.: A graphical tool for event refinement structures in event-B. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 269\u2013274. Springer, Cham (2016). doi:\n10.1007\/978-3-319-33600-8_20"},{"issue":"3","key":"5_CR6","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/s00165-014-0311-1","volume":"27","author":"AS Fathabadi","year":"2015","unstructured":"Fathabadi, A.S., Butler, M., Rezazadeh, A.: Language and tool support for event refinement structures in Event-B. Formal Aspects Comput. 27(3), 499\u2013523 (2015)","journal-title":"Formal Aspects Comput."},{"key":"5_CR7","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/j.scico.2016.04.010","volume":"131","author":"A F\u00fcrst","year":"2016","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D.A., Sato, N., Miyazaki, K.: Large-scale system development using abstract data types and refinement. Sci. Comput. Program. 131, 59\u201375 (2016)","journal-title":"Sci. Comput. Program."},{"key":"5_CR8","first-page":"211","volume-title":"Industrial Deployment of System Engineering Methods","author":"TS Hoang","year":"2013","unstructured":"Hoang, T.S.: An introduction to the Event-B modelling method. In: Romanovsky, A., Thomas, M. (eds.) Industrial Deployment of System Engineering Methods, pp. 211\u2013236. Springer, Heidelberg (2013)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-319-67729-3_7","volume-title":"International Colloquium on Theoretical Aspects of Computing\u2013ICTAC 2017","author":"TS Hoang","year":"2017","unstructured":"Hoang, T.S., Snook, C., Dghaym, D., Butler, M.: Class-diagrams for abstract data types. In: Van Hung, D., Deepak, K. (eds.) International Colloquium on Theoretical Aspects of Computing\u2013ICTAC 2017. LNCS, pp. 100\u2013117. Springer, Cham (2017). doi:\n10.1007\/978-3-319-67729-3_7"},{"key":"5_CR10","volume-title":"System Development","author":"MA Jackson","year":"1983","unstructured":"Jackson, M.A.: System Development. Prentice-Hall, Englewood Cliffs (1983)"},{"key":"5_CR11","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1016\/j.scico.2014.04.005","volume":"96","author":"P James","year":"2014","unstructured":"James, P., Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S.A., Treharne, H.: On modelling and verifying railway interlockings: Tracking train lengths. Sci. Comput. Program 96, 315\u2013336 (2014)","journal-title":"Sci. Comput. Program"},{"issue":"2","key":"5_CR12","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: An automated analysis toolset for the B method. Softw. Tools Technol. Transf. (STTT) 10(2), 185\u2013203 (2008)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"issue":"1\u20132","key":"5_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M Oliveira","year":"2009","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for circus. Formal Aspects Comput. 21(1\u20132), 3\u201332 (2009)","journal-title":"Formal Aspects Comput."},{"unstructured":"Reichl, K.: RailGround model on github (2016). \nhttps:\/\/github.com\/klar42\/railground\/\n\n. Accessed 20 Apr 2017","key":"5_CR14"},{"issue":"4","key":"5_CR15","doi-asserted-by":"crossref","first-page":"1557","DOI":"10.1007\/s10270-013-0391-z","volume":"14","author":"MY Said","year":"2015","unstructured":"Said, M.Y., Butler, M., Snook, C.: A method of refinement in UML-B. Softw. Syst. Model 14(4), 1557\u20131580 (2015)","journal-title":"Softw. Syst. Model"},{"issue":"4","key":"5_CR16","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/s00165-005-0076-7","volume":"17","author":"S Schneider","year":"2005","unstructured":"Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Formal Aspects Comput. 17(4), 390\u2013422 (2005)","journal-title":"Formal Aspects Comput."},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-16265-7_19","volume-title":"Integrated Formal Methods","author":"S Schneider","year":"2010","unstructured":"Schneider, S., Treharne, H., Wehrheim, H.: A CSP approach to control in event-B. In: M\u00e9ry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 260\u2013274. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-16265-7_19"},{"unstructured":"Snook, C.: iUML-B state-machines. In: Proceedings of the Rodin Workshop 2014, Toulouse, France, pp. 29\u201330 (2014). \nhttp:\/\/eprints.soton.ac.uk\/365301\/","key":"5_CR18"},{"issue":"1","key":"5_CR19","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook, C., Butler, M.: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol. 15(1), 92\u2013122 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"5_CR20","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1016\/j.scico.2016.05.010","volume":"133","author":"LH Vu","year":"2017","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: Formal modelling and verification of interlocking systems featuring sequential release. Sci. Comput. Program. 133, 91\u2013115 (2017)","journal-title":"Sci. Comput. Program."},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"J Woodcock","year":"2002","unstructured":"Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184\u2013203. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-45648-1_10"}],"container-title":["Lecture Notes in Computer Science","Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-68499-4_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,10,18]],"date-time":"2017-10-18T10:36:40Z","timestamp":1508323000000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-68499-4_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319684987","9783319684994"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-68499-4_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}