{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,8]],"date-time":"2026-02-08T23:33:16Z","timestamp":1770593596547,"version":"3.49.0"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319489889","type":"print"},{"value":"9783319489896","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-48989-6_46","type":"book-chapter","created":{"date-parts":[[2016,11,7]],"date-time":"2016-11-07T01:31:19Z","timestamp":1478482279000},"page":"748-756","source":"Crossref","is-referenced-by-count":22,"title":["Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems"],"prefix":"10.1007","author":[{"given":"Predrag","family":"Filipovikj","sequence":"first","affiliation":[]},{"given":"Nesredin","family":"Mahmud","sequence":"additional","affiliation":[]},{"given":"Raluca","family":"Marinescu","sequence":"additional","affiliation":[]},{"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[]},{"given":"Oscar","family":"Ljungkrantz","sequence":"additional","affiliation":[]},{"given":"Henrik","family":"L\u00f6nn","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,11,8]]},"reference":[{"key":"46_CR1","volume-title":"Mastering Simulink","author":"JB Dabney","year":"2004","unstructured":"Dabney, J.B., Harman, T.L.: Mastering Simulink. Pearson\/Prentice Hall, Upper Saddle River (2004)"},{"key":"46_CR2","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/978-3-319-29510-7_15","volume-title":"Formal Techniques for Safety-Critical Systems","author":"A Legay","year":"2016","unstructured":"Legay, A., Traonouez, L.-M.: Statistical model checking of Simulink models with Plasma Lab. In: Artho, C., \u00d6lveczky, P.C. (eds.) FTSCS 2015. CCIS, vol. 596, pp. 259\u2013264. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-29510-7_15"},{"issue":"4","key":"46_CR3","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: UPPAAL SMC tutorial. STTT J. 17(4), 397\u2013415 (2015)","journal-title":"STTT J."},{"key":"46_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17511-4_20"},{"key":"46_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-642-32469-7_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"J Barnat","year":"2012","unstructured":"Barnat, J., Beran, J., Brim, L., Kratochv\u00edla, T., Ro\u010dkai, P.: Tool chain to support automated formal verification of avionics Simulink designs. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 78\u201392. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-32469-7_6"},{"key":"46_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/11901433_33","volume-title":"Formal Methods and Software Engineering","author":"B Meenakshi","year":"2006","unstructured":"Meenakshi, B., Bhatnagar, A., Roy, S.: Tool for translating Simulink models into input language of a model checker. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 606\u2013620. Springer, Heidelberg (2006). doi: 10.1007\/11901433_33"},{"key":"46_CR7","first-page":"43","volume":"109","author":"A Agrawal","year":"2004","unstructured":"Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink\/Stateflow models to hybrid automata using graph transformations. ENTCS J. 109, 43\u201356 (2004)","journal-title":"ENTCS J."},{"key":"46_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-642-00768-2_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"SP Miller","year":"2009","unstructured":"Miller, S.P.: Bridging the gap between model-based development and model checking. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 443\u2013453. Springer, Heidelberg (2009). doi: 10.1007\/978-3-642-00768-2_36"},{"key":"46_CR9","doi-asserted-by":"crossref","unstructured":"Manamcheri, K., Mitra, S., Bak, S., Caccamo, M.: A step towards verification and synthesis from Simulink\/Stateflow models. In: HSCC 2011, pp. 317\u2013318. ACM (2011)","DOI":"10.1145\/1967701.1967749"},{"key":"46_CR10","doi-asserted-by":"crossref","unstructured":"Jiang, Y., Yang, Y., Liu, H., Kong, H., Gu, M., Sun, J., Sha, L.: From Stateflow simulation to verified implementation: a verification approach and a real-time train controller design. In: RTAS 2016, pp. 1\u201311, April 2016","DOI":"10.1109\/RTAS.2016.7461337"},{"key":"46_CR11","doi-asserted-by":"crossref","unstructured":"David, A., Du, D., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for stochastic hybrid systems. arXiv preprint arXiv:1208.3856 (2012)","DOI":"10.4204\/EPTCS.92.9"},{"issue":"1","key":"46_CR12","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT J. 1(1), 134\u2013152 (1997)","journal-title":"STTT J."},{"key":"46_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-35632-2_25","volume-title":"Runtime Verification","author":"P Bulychev","year":"2013","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 260\u2013275. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35632-2_25"}],"updated-by":[{"DOI":"10.1007\/978-3-319-48989-6_51","type":"erratum","label":"Erratum","source":"publisher","updated":{"date-parts":[[2017,2,23]],"date-time":"2017-02-23T00:00:00Z","timestamp":1487808000000}}],"container-title":["Lecture Notes in Computer Science","FM 2016: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48989-6_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,15]],"date-time":"2019-09-15T05:56:07Z","timestamp":1568526967000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48989-6_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489889","9783319489896"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48989-6_46","relation":{"erratum":[{"id-type":"doi","id":"10.1007\/978-3-319-48989-6_51","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}