{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:47:59Z","timestamp":1770338879027,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540372158","type":"print"},{"value":"9783540372165","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11813040_13","type":"book-chapter","created":{"date-parts":[[2006,8,7]],"date-time":"2006-08-07T06:51:03Z","timestamp":1154933463000},"page":"179-189","source":"Crossref","is-referenced-by-count":22,"title":["A Story About Formal Methods Adoption by a Railway Signaling Manufacturer"],"prefix":"10.1007","author":[{"given":"Stefano","family":"Bacherini","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Tempestini","sequence":"additional","affiliation":[]},{"given":"Niccol\u00f2","family":"Zingoni","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"Bacherini, S., Bianchi, S., Capecchi, L., Becheri, C., Felleca, A., Fantechi, A., Spinicci, E.: Modelling a railway signalling system using SDL. In: Proceedings 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003), Budapest. L\u2019Harmattan Hongrie (2003)"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/j.entcs.2004.02.083","volume":"116","author":"M. Banci","year":"2005","unstructured":"Banci, M., Becucci, M., Fantechi, A., Spinicci, E.: Validation Coverage for a Component-based SDL model of a Railway Signalling System. Electr. Notes Theor. Comput. Sci.\u00a0116, 99\u2013111 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"114","key":"13_CR3","first-page":"1317","volume":"35","author":"M. Becucci","year":"2005","unstructured":"Becucci, M., Fantechi, A., Giromini, M., Spinicci, E.: A Comparison between Handwritten and Automatic Generation of C Code from SDL using Static Analysis. Software: Practice&Experience\u00a035(114), 1317\u20131347 (2005)","journal-title":"Software: Practice&Experience"},{"key":"13_CR4","volume-title":"The Unified Modeling Language User Guide","author":"G. Booch","year":"1999","unstructured":"Booch, G., Rumbaugh, J., Jacobson, I.: The Unified Modeling Language User Guide. Addison-Wesley, Reading (1999)"},{"key":"13_CR5","volume-title":"SDL - Formal Object-oriented Language for Communicating Systems","author":"J. Ellsberger","year":"1997","unstructured":"Ellsberger, J., Hogrefe, D., Sarma, A.: SDL - Formal Object-oriented Language for Communicating Systems. Prentice-Hall, Englewood Cliffs (1997)"},{"key":"13_CR6","unstructured":"European Committee for Electrotechnical Standardization. EN 50128, Railway Applications Communications, Signaling and Processing Systems Software for Railway Control and Protection Systems (2001)"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Fantechi, A., Spinicci, E.: Modelling and Validating a Multiple-configuration railway signalling system using SDL. Electronic Notes in Theoretical Computer Science\u00a082(6) (2003)","DOI":"10.1016\/S1571-0661(04)81026-0"},{"key":"13_CR8","unstructured":"Foschi, U., Giuliani, M., Morzenti, A., Pradella, M., San Pietro, P.: The role of formal methods in software procurement for the railway transportation industry. In: Proceedings 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003), Budapest. L\u2019Harmattan Hongrie (2003)"},{"key":"13_CR9","unstructured":"Gnesi, S., Mazzanti, F.: On the fly model checking of communicating UML State Machines. In: Second ACIS International Conference on Software Engineering Research Management and Applications (SERA 2004), Los Angeles, USA, 5-7 May (2004)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-540-24721-0_17","volume-title":"Fundamental Approaches to Software Engineering","author":"G. Hamon","year":"2004","unstructured":"Hamon, G., Rushby, J.M.: An Operational Semantics for Stateflow. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol.\u00a02984, pp. 229\u2013243. Springer, Heidelberg (2004)"},{"issue":"3","key":"13_CR11","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming\u00a08(3), 231\u2013274 (1987)","journal-title":"Science of Computer Programming"},{"issue":"4","key":"13_CR12","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/32.54292","volume":"16","author":"D. Harel","year":"1990","unstructured":"Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M.: STATEMATE: A Working Environment for the Development of Complex Reactive Systems. IEEE Transactions on Software Engineering\u00a016(4), 403\u2013414 (1990)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"13_CR13","unstructured":"K\u00f6nig, N.H., Einer, S.: The Euro-Interlocking formalized functional requirements approach (EIFFRA). In: Proceedings 4th Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003), Budapest. L\u2019Harmattan Hongrie (2003)"},{"key":"13_CR14","unstructured":"Krogh, B., Spencer, C.: Formal Verification of Stateflow Diagrams Using SMV, \n                    \n                      http:\/\/www.ece.cmu.edu\/webk\/sf2smv\/"},{"key":"13_CR15","unstructured":"Le Bouar, P.: Interlocking SNCF functional requirements description. Euro-Interlocking Project, Paris (May 2003)"},{"key":"13_CR16","unstructured":"The Mathworks: Stateflow and Stateflow Coder, Users Guide (2005)"},{"key":"13_CR17","unstructured":"The Mathworks: MATLAB 7 Users Guide (2005)"},{"key":"13_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"13_CR19","unstructured":"Object Management Group, Unified Modeling Language Specification, Version 1.5 (1999), \n                    \n                      http:\/\/www.omg.org\/technology\/documents\/formal\/uml.htm"},{"issue":"1","key":"13_CR20","first-page":"10","volume":"12","author":"J. Warmer","year":"1999","unstructured":"Warmer, J., Kleppe, A.: OCL: The constraint language of the UML. Journal of Object-Oriented Programming\u00a012(1), 10\u201313,28 (1999)","journal-title":"Journal of Object-Oriented Programming"}],"container-title":["Lecture Notes in Computer Science","FM 2006: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11813040_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:27:19Z","timestamp":1619494039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11813040_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372158","9783540372165"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11813040_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}