{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,12]],"date-time":"2026-11-12T00:35:44Z","timestamp":1794443744374,"version":"4.9.1"},"publisher-location":"London","reference-count":13,"publisher":"Springer London","isbn-type":[{"value":"9783540199625","type":"print"},{"value":"9781447130543","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/978-1-4471-3054-3_33","type":"book-chapter","created":{"date-parts":[[2013,4,8]],"date-time":"2013-04-08T23:33:23Z","timestamp":1365464003000},"page":"474-488","source":"Crossref","is-referenced-by-count":5,"title":["An Experience in Formal Verification of Safety Properties of a Railway Signalling Control System"],"prefix":"10.1007","author":[{"given":"A.","family":"Anselmi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C.","family":"Bernardeschi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A.","family":"Fantechi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Gnesi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Larosa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"G.","family":"Mongardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"F.","family":"Torielli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"33_CR1","volume-title":"Testing of a Computer Based Interlocking Software: Methodology and Environment","author":"C Abbaneo","year":"1992","unstructured":"C. Abbaneo, G. Biondi, M. Ferrando, G. Mongardi. Testing of a Computer Based Interlocking Software: Methodology and Environment. SAFECOMP 1992, Zurich."},{"issue":"2","key":"33_CR2","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"J. R. Burch, E.M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), June 1992, pp. 142\u2013270.","journal-title":"Information and Computation"},{"key":"33_CR3","unstructured":"A. Bouali, S. Gnesi, S. Larosa. The integration Project for the JACK Environment. Bulletin of the EATCS, n.54, October 1994, pp.207\u2013223."},{"key":"33_CR4","unstructured":"CENELEC - pr EN 50128 - Railway Applications: Software fo Railway Control and Protection Systems."},{"issue":"2","key":"33_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"E. M. Clarke, E. A. Emerson, A. P. Sistla. Automatic Verification of Finite-State Concurrent, Systems Using Temporal Logic Specification. ACM Transaction on Programming Languages and Systems, Vol. 8, No. 2, April 1986, pp. 244 \u2013 263.","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Action versus State based Logics for Transition Systems","author":"R Nicola De","year":"1990","unstructured":"R. De Nicola, F. W. Vaandrager. Action versus State based Logics for Transition Systems. Proceedings Ecole de Printemps on Semantics of Concurrency. Lecture Notes in Computer Science 469, Springer-Verlag, 1990, pp. 407\u2013419."},{"key":"33_CR7","volume-title":"Three Logics for Branching Bisimulation. Internal Report DSI-92-03, Dipartimento di Scienze dell\u2019Informazione, Univ. di Roma \u201cLa Sapienza\u201d","author":"R Nicola De","year":"1992","unstructured":"R. De Nicola and F.W. Vaandrager. Three Logics for Branching Bisimulation. Internal Report DSI-92-03, Dipartimento di Scienze dell\u2019Informazione, Univ. di Roma \u201cLa Sapienza\u201d, 1992. To appear in Journal of ACM."},{"issue":"1","key":"33_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"E. A. Emerson, J. Y. Halpern. \u201cSometimes\u201d and \u201cNot Never\u201d Revisited: on Branching Time versus Linear Time Temporal Logic. Journal of ACM, 33 (1),1986, pp. 151\u2013178.","journal-title":"Journal of ACM"},{"key":"33_CR9","volume-title":"AMC: ACTL Model Checker","author":"G Ferro","year":"1994","unstructured":"G. Ferro. AMC: ACTL Model Checker. Reference Manual. IEI-Internal Report, B4-47 December 1994."},{"key":"33_CR10","volume-title":"Communicating Sequential Processes","author":"CAR Hoare","year":"1985","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall Int., London, 1985."},{"key":"33_CR11","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM, 32, 1985, pp. 137\u2013161.","journal-title":"Journal of ACM"},{"key":"33_CR12","volume-title":"Communication and Concurrency","author":"R Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"33_CR13","unstructured":"Programma logica Gioul (vers.5.2) \u2014 Specifica funzionale \u2014 parte II, cap. 13, Ansaldo Trasporti, 1994."}],"container-title":["Safe Comp 95"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-1-4471-3054-3_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,12]],"date-time":"2019-05-12T01:13:36Z","timestamp":1557623616000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-1-4471-3054-3_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540199625","9781447130543"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-1-4471-3054-3_33","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-1-4471-3054-3","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[1995]]}}}