{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:32:24Z","timestamp":1752229944206,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175805"},{"type":"electronic","value":"9783319175812"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17581-2_7","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T12:22:36Z","timestamp":1429100556000},"page":"93-109","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Dynamic State Machines for Formalizing Railway Control System Specifications"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Nardone","sequence":"first","affiliation":[]},{"given":"Ugo","family":"Gentile","sequence":"additional","affiliation":[]},{"given":"Adriano","family":"Peron","sequence":"additional","affiliation":[]},{"given":"Massimo","family":"Benerecetti","sequence":"additional","affiliation":[]},{"given":"Valeria","family":"Vittorini","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Marrone","sequence":"additional","affiliation":[]},{"given":"Renato","family":"De Guglielmo","sequence":"additional","affiliation":[]},{"given":"Nicola","family":"Mazzocca","sequence":"additional","affiliation":[]},{"given":"Luigi","family":"Velardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-48523-6_14","volume-title":"Automata, Languages and Programming","author":"R Alur","year":"1999","unstructured":"Alur, R., Kannan, S., Yannakakis, M.: Communicating hierarchical state machines. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 169\u2013178. Springer, Heidelberg (1999)"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Ammann, P., Black, P., Majurski, W.: Using model checking to generate tests from specifications. In: Proceedings of the 2nd IEEE Internernational Conference on Formal Engineering Methods (ICFEM 1998), pp. 46\u201354. IEEE Computer Society (1998)","DOI":"10.6028\/NIST.IR.6166"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-319-10557-4_18","volume-title":"Computer Safety, Reliability, and Security","author":"G Barberio","year":"2014","unstructured":"Barberio, G., Di Martino, B., Mazzocca, N., Velardi, L., Amato, A., De Guglielmo, R., Gentile, U., Marrone, S., Nardone, R., Peron, A., Vittorini, V.: An interoperable testing environment for ERTMS\/ETCS control systems. In: Bondavalli, A., Ceccarelli, A., Ortmeier, F. (eds.) SAFECOMP 2014. LNCS, vol. 8696, pp. 147\u2013156. Springer, Heidelberg (2014)"},{"key":"7_CR4","unstructured":"Bjorner, D.: New results and trends in formal techniques and tools for the development of software for transportation systems - A review. In: Tarnai, G. and Schnieder, E. (eds.) Symposium on Formal Methods for Railway Operation and Control Systems (FORMS 2003), L\u2019Harmattan Hongrie, Budapest\/Hungary, Germany, May 2003"},{"key":"7_CR5","unstructured":"CENELEC, EN 50126:2012: Railway applications - Demonstration of Reliability, Availability, Maintainability and Safety (RAMS) - Part 1: Generic RAMS process"},{"key":"7_CR6","unstructured":"CENELEC, EN 50128:2011: Railway applications - Communication, signalling and processing systems - Software for railway control and protection systems"},{"key":"7_CR7","unstructured":"CESAR: Cost-Efficient methods and proceses for SAfety Relevant embedded systems. http:\/\/www.cesarproject.eu\/"},{"key":"7_CR8","unstructured":"CRYSTAL: CRitical sYSTem engineering AcceLeration. http:\/\/www.crystal-artemis.eu\/"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1007\/978-3-319-10702-8_12","volume-title":"Formal Methods for Industrial Critical Systems","author":"U Gentile","year":"2014","unstructured":"Gentile, U., Marrone, S., Mele, G., Nardone, R., Peron, A.: Test specification patterns for automatic generation of test sequences. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 170\u2013184. Springer, Heidelberg (2014)"},{"key":"7_CR10","unstructured":"Glinz, M.: Statecharts for requirements specification - as simple as possible, as rich as needed. In: International Workshop on Scenarios and State Machines: Models Algorithms and Tools (2002)"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Hamon, G.: A denotational semantics for Stateflow. In: The Fifth ACM International Conference on Embedded Software, pp. 164\u2013172. ACM Press (2005)","DOI":"10.1145\/1086228.1086260"},{"key":"7_CR12","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. 2984, pp. 229\u2013243. Springer, Heidelberg (2004)"},{"key":"7_CR13","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. Sci. Comput. Program. 8, 231\u2013274 (1987)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"7_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1145\/235321.235322","volume":"5","author":"D Harel","year":"1996","unstructured":"Harel, D., Naamad, A.: The STATEMATE semantics of statecharts. ACM Trans. Softw. Eng. Methodol. 5(4), 333 (1996)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"7_CR15","first-page":"237","volume":"54","author":"R Lanotte","year":"2003","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Peron, A., Tini, S.: Dynamical hierachical machines. Fundamenta Informaticae 54, 237\u2013252 (2003)","journal-title":"Fundamenta Informaticae"},{"issue":"9","key":"7_CR16","doi-asserted-by":"publisher","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"NG Leveson","year":"1994","unstructured":"Leveson, N.G., Heimdahl, M.P.E., Hildreth, H., Reese, J.D.: Requirements specification for process-control systems. IEEE Trans. Softw. Eng. 20(9), 684\u2013707 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"7_CR17","unstructured":"MBAT: Combined Model-based Analysis and Testing of Embedded Systems. http:\/\/www.mbat-artemis.eu\/"},{"issue":"2","key":"7_CR18","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1002\/stvr.1489","volume":"24","author":"S Mohalik","year":"2014","unstructured":"Mohalik, S., Gadkari, A.A., Yeolekar, A., Shashidhar, K.C., Ramesh, S.: Automatic test case generation from simulink\/stateflow models using model checking. Softw. Test. Verif. Reliab. 24(2), 155\u2013180 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"7_CR19","unstructured":"OMG. Unified Modeling Language (UML), v2.4.1, Superstructure Specification"},{"key":"7_CR20","first-page":"12","volume":"14","author":"H Pfl\u00fcgl","year":"2013","unstructured":"Pfl\u00fcgl, H., El-Salloum, C., Kundner, I.: CRYSTAL, CRitical sYSTem engineering AcceLeration, a Truly European Dimension. ARTEMIS Magazine 14, 12\u201315 (2013)","journal-title":"ARTEMIS Magazine"},{"key":"7_CR21","unstructured":"Steinberg, D., Budinsky, F., Paternostro, M., Merks, E.: EMF: Eclipse Modeling Framework. Addison-Wesley Professional (2009)"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17581-2_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T10:28:21Z","timestamp":1675852101000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17581-2_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175805","9783319175812"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17581-2_7","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}