{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T20:01:26Z","timestamp":1725739286188},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642396106"},{"type":"electronic","value":"9783642396113"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39611-3_20","type":"book-chapter","created":{"date-parts":[[2013,7,3]],"date-time":"2013-07-03T22:33:07Z","timestamp":1372890787000},"page":"193-208","source":"Crossref","is-referenced-by-count":18,"title":["Defining and Model Checking Abstractions of Complex Railway Models Using CSP||B"],"prefix":"10.1007","author":[{"given":"Faron","family":"Moller","sequence":"first","affiliation":[]},{"given":"Hoang Nga","family":"Nguyen","sequence":"additional","affiliation":[]},{"given":"Markus","family":"Roggenbach","sequence":"additional","affiliation":[]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","unstructured":"Advance FP7 project, http:\/\/www.advance-ict.eu\/ (accessed: July 23, 2012)"},{"key":"20_CR2","unstructured":"Practical formal validation method for interlocking or automated systems, http:\/\/www.dcds11.uni-saarland.de\/plenaries\/practical-formal-validation-method-for-interlocking-or-automated-systems.html (accessed: July 23, 2012)"},{"key":"20_CR3","unstructured":"ProB 1.3.5 beta15, http:\/\/www.stups.uni-duesseldorf.de\/ProB (accessed: July 23, 2012)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. CUP (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"20_CR5","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, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 378\u2013393. Springer, Heidelberg (2012)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Magnani, G., Grasso, D., Fantechi, A.: Model checking interlocking control tables. In: FORMS\/FORMAT, pp. 107\u2013115 (2010)","DOI":"10.1007\/978-3-642-14261-1_11"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-642-34032-1_25","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"A.E. Haxthausen","year":"2012","unstructured":"Haxthausen, A.E.: Automated generation of safety requirements from railway interlocking tables. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol.\u00a07610, pp. 261\u2013275. Springer, Heidelberg (2012)"},{"issue":"11","key":"20_CR8","doi-asserted-by":"publisher","first-page":"927","DOI":"10.1109\/32.730543","volume":"24","author":"C.L. Heitmeyer","year":"1998","unstructured":"Heitmeyer, C.L., Kirby, J., Labaw, B.G., Archer, M., Bharadwaj, R.: Using abstraction and model checking to detect safety violations in requirements specifications. IEEE Trans. Software Eng.\u00a024(11), 927\u2013948 (1998)","journal-title":"IEEE Trans. Software Eng."},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)","DOI":"10.1007\/978-3-642-82921-5_4"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-30729-4_5","volume-title":"Integrated Formal Methods","author":"Y. Isobe","year":"2012","unstructured":"Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways \u2013 an approach in Timed CSP. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol.\u00a07321, pp. 54\u201368. Springer, Heidelberg (2012)"},{"key":"20_CR11","unstructured":"Bj\u00f8rner, D.: TRain: The Railway domain - A \u201cGrand Challenge\u201d for Computing Science & Transportation Engineering. In: Jacquart, R. (ed.) Building the Information Society, IFIP 18th World Computer Congress, Topical Sessions, Toulouse, France, August 22-27, pp. 604\u2013612. Kluwer (2004)"},{"key":"20_CR12","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Combining event-based and state-based modelling for railway verification. Technical Report CS-12-02, University of Surrey (2012)"},{"key":"20_CR13","unstructured":"Moller, F., Nguyen, H.N., Roggenbach, M., Schneider, S., Treharne, H.: Railway modelling in CSP\u2225B: the double junction case study. In: AVOCS (2012)"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Morgan, C.C.: Of wp and CSP. In: Beauty Is Our Business: A Birthday Salute to Edsger J. Dijkstra. Springer (1990)","DOI":"10.1007\/978-1-4612-4476-9_37"},{"issue":"4","key":"20_CR15","doi-asserted-by":"publisher","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 Asp. Comput.\u00a017(4), 390\u2013422 (2005)","journal-title":"Formal Asp. Comput."},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-34032-1_24","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Applications and Case Studies","author":"K. Winter","year":"2012","unstructured":"Winter, K.: Optimising ordering strategies for symbolic model checking of railway interlockings. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol.\u00a07610, pp. 246\u2013260. Springer, Heidelberg (2012)"},{"key":"20_CR17","unstructured":"Winter, K., Robinson, N.J.: Modelling large railway interlockings and model checking small ones. In: ACSC, pp. 309\u2013316 (2003)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39611-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,27]],"date-time":"2022-02-27T05:57:13Z","timestamp":1645941433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39611-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396106","9783642396113"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39611-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}