{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:38:36Z","timestamp":1725565116263},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642158971"},{"type":"electronic","value":"9783642158988"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-15898-8_1","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T09:43:47Z","timestamp":1284371027000},"page":"1-16","source":"Crossref","is-referenced-by-count":9,"title":["The Metr\u00f4 Rio ATP Case Study"],"prefix":"10.1007","author":[{"given":"Alessio","family":"Ferrari","sequence":"first","affiliation":[]},{"given":"Daniele","family":"Grasso","sequence":"additional","affiliation":[]},{"given":"Gianluca","family":"Magnani","sequence":"additional","affiliation":[]},{"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[]},{"given":"Matteo","family":"Tempestini","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"European Committee for Electrotechnical Standardization: CENELEC EN 50128, Railway Applications - Software for Railway Control and Protection Systems (1997)"},{"key":"1_CR2","unstructured":"Ferrari, A., Fantechi, A., Bacherini, S., Zingoni, N.: Modeling Guidelines for Code Generation in the Railway Signaling Context. In: 1st NASA Formal Methods Symphosium (NFM), Moffet Field, California, U.S.A. (2009)"},{"issue":"3","key":"1_CR3","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"},{"key":"1_CR4","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.: An operational semantics for stateflow. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol.\u00a02984, pp. 229\u2013243. Springer, Heidelberg (2004)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Hamon, G.: A denotational semantics for stateflow. In: 5th ACM Int. Conf. on Embedded Software, Jersey City, NJ, USA, pp. 164\u2013172 (2005)","DOI":"10.1145\/1086228.1086260"},{"key":"1_CR6","unstructured":"Mathworks Automotive Advisory Board (MAAB): Control Algorithm Modeling Guidelines Using Matlab, Simulink and Stateflow, Version 2.0 (2007), \n \n http:\/\/www.mathworks.com\/industries\/auto\/maab.html"},{"key":"1_CR7","unstructured":"Sahbani, A., Pascal, J.C.: Simulation of hybrid systems using stateflow. In: Proceedings of the 14th European Simulation Multiconference on Simulation and Modelling: Enablers for a Better Quality of Life, pp. 271\u2013275 (2000)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Scaife, N., et al.: Defining and translating a safe subset of simulink\/stateflow into lustre. In: 4th ACM Int. Conf. on Embedded Software, Pisa, Italy, pp. 259\u2013268 (2004)","DOI":"10.1145\/1017753.1017795"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/11813040_13","volume-title":"FM 2006: Formal Methods","author":"S. Bacherini","year":"2006","unstructured":"Bacherini, S., Fantechi, A., Tempestini, M., Zingoni, N.: A Story about Formal Methods Adoption by a Railway Signaling Manufacturer. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 179\u2013189. Springer, Heidelberg (2006)"},{"key":"1_CR10","first-page":"389","volume-title":"Formal Methods in System Design","author":"M. Conrad","year":"2009","unstructured":"Conrad, M.: Testing-based translation validation of generated code in the context of IEC 61508. In: Formal Methods in System Design, pp. 389\u2013401. Springer, Heidelberg (2009)"},{"key":"1_CR11","unstructured":"Baresel, A., Conrad, M., Sadeghipour, S., Wegener, J.: The interplay between model coverage and code coverage. In: Proceedings of the 11th Eur. int. Conf. on Software Testing, Analysis and Review EuroSTAR\u201903, Amsterdam, Netherlands (2003)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM Symp. on Principles of Programming Languages (POPL), Los Angeles, California, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Grasso, D., Fantechi, A., Ferrari, A.: Model Based Testing and Abstract Interpretation in the Railway Signaling Context. In: 3rd International Conference on Software Testing, Verification and Validation (ICST), Paris, France, pp. 103\u2013106 (2010)","DOI":"10.1109\/ICST.2010.44"},{"key":"1_CR14","unstructured":"Deutsch, A.: Static verification of dynamic properties. PolySpace White Paper (2004)"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Ferrari, A., Fantechi, A., Papini, M., Grasso, D.: An industrial application of formal model based development: the Metr\u00f4 Rio ATP case. In: 2nd International Workshop on Software Engineering for Resilient Systems, SERENE 2010 (2010)","DOI":"10.1145\/2401736.2401744"},{"key":"1_CR16","unstructured":"Faivre, A., Benoit, P.: Safety critical software of meteor developed with the B formal method and vital coded processor. In: Proc. of WCRR\u201999, pp. 84\u201389 (1999)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Guiho, G., Hennebert, A.: SACEM Software Validation. In: 12th International Conference on Software Engineering, pp. 186\u2013191 (1990)","DOI":"10.1109\/ICSE.1990.63621"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"810","DOI":"10.1007\/978-3-642-00255-7","volume-title":"FM 2009: Formal Methods","author":"M. Leuschel","year":"2009","unstructured":"Leuschel, M., et al.: Automated property verification for large scale B models. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 810\u2013814. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15898-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,20]],"date-time":"2019-03-20T11:36:43Z","timestamp":1553081803000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15898-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642158971","9783642158988"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15898-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}