{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T15:54:30Z","timestamp":1791129270228,"version":"4.1.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1998,3,1]],"date-time":"1998-03-01T00:00:00Z","timestamp":888710400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,3,1]],"date-time":"1998-03-01T00:00:00Z","timestamp":888710400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[1998,3]]},"DOI":"10.1023\/a:1008645826258","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T10:12:40Z","timestamp":1040551960000},"page":"139-161","source":"Crossref","is-referenced-by-count":50,"title":["A Formal Verification Environment for Railway Signaling System Design"],"prefix":"10.1007","volume":"12","author":[{"given":"Cinzia","family":"Bernardeschi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Salvatore","family":"Larosa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giorgio","family":"Mongardi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dario","family":"Romano","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"161912_CR1","unstructured":"J.R. Abrial et al. The B Method. BP International Ltd., 1991."},{"key":"161912_CR2","first-page":"474","volume-title":"Proceedings SAFECOMP'95 Conference","author":"A. Anselmi","year":"1995","unstructured":"A. Anselmi, C. Bernardeschi, A. Fantechi, S. Gnesi and S. Larosa, G. Mongardi and F. Torielli. An Experience in Formal Verification of Safety Properties of a Railway Signaling Control System. In Proceedings SAFECOMP'95 Conference. Belgirate, Springer-Verlag, pages 474\u2013488, 1995."},{"key":"161912_CR3","unstructured":"C. Bernardeschi and G. Ferro. A Sample Study Exemplifying the Use of JACK. In Proceedings Workshop on Automated Formal Methods, ENTCS. University of Oxford, 1996 (to appear)."},{"key":"161912_CR4","unstructured":"R. S. Boyer and J.S. Moore. A Computational Logic. ACM Monograph Series, Academic Press, 1979."},{"key":"161912_CR5","doi-asserted-by":"crossref","unstructured":"J.P. Bowen and M.G. Hinchey. Seven More Myths of Formal Methods. IEEE Software 12:34\u201341, July 1995.","DOI":"10.1109\/52.391826"},{"key":"161912_CR6","doi-asserted-by":"crossref","unstructured":"A. Bouali and R. De Simone. Symbolic bisimulation minimization. In Proceedings Fourth Workshop on Computer-Aided Verification, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, pages 96\u2013108, 1992.","DOI":"10.1007\/3-540-56496-9_9"},{"key":"161912_CR7","unstructured":"A. Bouali, S. Gnesi and S. Larosa. The integration Project for the JACK Environment. Bulletin of the EATCS 54:207\u2013223, October 1994."},{"key":"161912_CR8","doi-asserted-by":"crossref","unstructured":"A. Bouali, A. Ressouche, V. Roy and R. De Simone. The FC2TOOLS set. In Proceedings Workshop on Computer-Aided Verification, volume 1102 of Lecture Notes in Computer Science. Springer-Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_98"},{"key":"161912_CR9","doi-asserted-by":"crossref","unstructured":"G. Boudol. Notes on Algebraic Calculi of Processes. NATO ASI Series F13, 1985.","DOI":"10.1007\/978-3-642-82453-1_9"},{"key":"161912_CR10","unstructured":"G. Bruns. A Case Study in Safety Critical Design. In Proceedings Workshop on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, pages 213\u2013224, 1992."},{"key":"161912_CR11","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation 98 2:142\u2013270, June 1992.","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"161912_CR12","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson and A.P. Sistla. Automatic Verification of Finite\u2014State Concurrent Systems Using Temporal Logic Specification. ACM Transaction on Programming Languages and Systems 8:244\u2013263, April 1986.","DOI":"10.1145\/5397.5399"},{"key":"161912_CR13","first-page":"199","volume-title":"Formal Description Techniques, V (C-10)","author":"C. Da Silva","year":"1993","unstructured":"C. Da Silva, B. Dehbonei and F. Mejia. Formal Specification in the Development of Industrial Applications: Subway Speed Control System. In M. Diaz and R. Groz, editors, Formal Description Techniques, V (C-10). Elsevier Science Publishers B, V, North-Holland, pages 199\u2013213, 1993."},{"key":"161912_CR14","doi-asserted-by":"crossref","unstructured":"B. Dehbonei and F. Mejia. Formal Methods in the Railways Signaling Industry. In Proceedings FME'94: Industrial Benefit of Formal Methods, volume 873 of Lecture Notes in Computer Science. Spain, pages 26\u201334, 1994.","DOI":"10.1007\/3-540-58555-9_84"},{"key":"161912_CR15","doi-asserted-by":"crossref","unstructured":"R. De Nicola, A. Fantechi, S. Gnesi and G. Ristori. An Action-based Framework for Verifying Logical and Behavioral Properties of Concurrent Systems. Computer Network and ISDN systems 25:761\u2013778, February 1993","DOI":"10.1016\/0169-7552(93)90047-8"},{"key":"161912_CR16","doi-asserted-by":"crossref","unstructured":"R. De Nicola and F.W. Vaandrager. Action versus State based Logics for Transition Systems. In Proceedings Ecole de Printemps on Semantics of Concurrency, volume 469 of Lecture Notes in Computer Science. Springer-Verlag, pages 407\u2013419, 1990.","DOI":"10.1007\/3-540-53479-2_17"},{"key":"161912_CR17","doi-asserted-by":"crossref","unstructured":"R. De Nicola, A. Fantechi, S. Gnesi and G. Ristori. Hardware Components within JACK,\u201d In Proceedings of CHARME '95, volume 987 of Lecture Notes in Computer Science. Springer-Verlag, pages 246\u2013260, 1995.","DOI":"10.1007\/3-540-60385-9_15"},{"key":"161912_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"E.A. Emerson and J.Y. Halpern. Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. Journal of Computer and System Sciences 30:1\u201324, 1985.","journal-title":"Journal of Computer and System Sciences"},{"key":"161912_CR19","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and J.Y. Halpern. Sometimes and Not Never Revisited: on Branching Time versus Linear Time Temporal Logic. Journal of ACM 33:51\u2013178, January 1986.","DOI":"10.1145\/4904.4999"},{"key":"161912_CR20","unstructured":"G. Ferro. AMC: ACTL Model Checker. Reference Manual. IEI-Internal Report, B4-47 December 1994."},{"key":"161912_CR21","doi-asserted-by":"crossref","unstructured":"S. Fisher, A. Scholz and D. Taubner. Verification in Process Algebra of the Distributed Control of Track Vehicles-A Case Study. Journal of Formal Methods in System Design ?:99\u2013122, February 1994","DOI":"10.1007\/BF01384080"},{"key":"161912_CR22","unstructured":"S. Gnesi. A Formal Verification Environment for Concurrent Systems Design. In Proceedings Workshop on Automated Formal Methods, ENTCS. University of Oxford, 1996 (to appear)."},{"key":"161912_CR23","unstructured":"V. Hartonas-Garmhausen, T. Kurfess, E.M. Clarke and D. Long. Automatic Verification of Industrial Designs. In Proceedings Workshop on Industrial-Strength Formal Specification Techniques. Boca Raton, Florida, April 1995."},{"key":"161912_CR24","volume-title":"Communicating Sequential Processes","author":"C.R. Hoare","year":"1985","unstructured":"C.R. Hoare. Communicating Sequential Processes. Prentice Hall Int., London, 1985."},{"key":"161912_CR25","doi-asserted-by":"crossref","unstructured":"M. Hennessy and R. Milner. Algebraic Laws for Nondeterminism and Concurrency. Journal of ACM 32:137\u2013161, January 1985.","DOI":"10.1145\/2455.2460"},{"key":"161912_CR26","doi-asserted-by":"crossref","unstructured":"R. Pugliese and E. Tronci. Automatic Verification of a Hydroelectric Power Plant. In Proceedings FME'96 Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 425\u2013444, 1996.","DOI":"10.1007\/3-540-60973-3_100"},{"key":"161912_CR27","unstructured":"E. Madelaine and D. Vergamini. AUTO: A Verification tool for Distributed Systems using Reduction of Finite Automata Networks. In S.T Vuong, edtor, Formal Description Techniques II, pages 61\u201366, 1990."},{"key":"161912_CR28","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems-Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"161912_CR29","doi-asserted-by":"crossref","unstructured":"R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"key":"161912_CR30","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"161912_CR31","doi-asserted-by":"crossref","unstructured":"G. Mongardi. Dependable Computing for Railway Control Systems. In Proceedings Dependable Computing for Critical Applications 3. Springer-Verlag, pages 255\u2013277, 1992.","DOI":"10.1007\/978-3-7091-4009-3_11"},{"key":"161912_CR32","unstructured":"W. Nyberg. An Evaluation of Using State-Based Specification Languages for an Automatic Train Protection System. In Proceedings Nordic Seminar on Dependable Computing Systems ( NSDCS'94). Lingby, Denmark, pages 105\u2013116, 1994."},{"key":"161912_CR33","doi-asserted-by":"crossref","unstructured":"D. Park. Concurrency and Automata on Infinite Sequences. In Proccedings Fifth GI Conference, volume 104 of Lecture Notes in Computer Science. Springer-Verlag, pages 167\u2013183, 1981.","DOI":"10.1007\/BFb0017309"},{"key":"161912_CR34","unstructured":"A. Pnueli. Linear and Branching Structures in the Semantics and Logic of Reactive Systems. In Proceedings of 12\n                    th\n                  \nICALP, volume 194 of Lecture Notes in Computer Science, 1985."},{"key":"161912_CR35","doi-asserted-by":"crossref","unstructured":"V. Roy and R. De Simone. AUTO and Autograph. In Proceedings Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science. Springer-Verlag, pages 65\u201375, 1990.","DOI":"10.1007\/BFb0023720"},{"key":"161912_CR36","doi-asserted-by":"crossref","unstructured":"A. Simpson. The Formal Specification of an Automatic Train Protection System. In Proceedings FME'94 Industrial Benefit of Formal Methods, volume 873 of Lecture Notes in Computer Science. Spain, pages 602\u2013617, 1994.","DOI":"10.1007\/3-540-58555-9_118"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008645826258.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008645826258\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008645826258.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:02:44Z","timestamp":1754366564000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008645826258"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,3]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1998,3]]}},"alternative-id":["161912"],"URL":"https:\/\/doi.org\/10.1023\/a:1008645826258","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,3]]}}}