{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:39:00Z","timestamp":1742913540899,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031753794"},{"type":"electronic","value":"9783031753800"}],"license":[{"start":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T00:00:00Z","timestamp":1730246400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,10,30]],"date-time":"2024-10-30T00:00:00Z","timestamp":1730246400000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-75380-0_13","type":"book-chapter","created":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T08:29:02Z","timestamp":1730190542000},"page":"220-246","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SIMPPAAL: A Framework for\u00a0Statistical Model Checking of\u00a0Industrial Simulink Models"],"prefix":"10.1007","author":[{"given":"Predrag","family":"Filipovikj","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nesredin","family":"Mahmud","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillermo","family":"Rodriguez-Navas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oscar","family":"Ljungkrantz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrik","family":"L\u00f6nn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,30]]},"reference":[{"key":"13_CR1","unstructured":"The\u00a0MathWorks, Inc. Simulink Reference, Matlab & Simulink. The MathWorks, Inc., 3 Apple Hill Drive Natick, MA 01760-2098, R2017a edition (2017)"},{"key":"13_CR2","unstructured":"Dabney, J.B., Harman, T.L.: Mastering Simulink. Pearson\/Prentice Hall (2004)"},{"key":"13_CR3","unstructured":"Mathworks. Mathworks: Simulink Design Verifier - User\u2019s Guide (2018). Accessed 24 October 2018"},{"key":"13_CR4","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, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29510-7_15"},{"key":"13_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). https:\/\/doi.org\/10.1007\/978-3-642-32469-7_6"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Jiang, Y., et al.: From Stateflow simulation to verified implementation: a verification approach and a real-time train controller design. In: RTAS 2016, pp. 1\u201311 (2016)","DOI":"10.1109\/RTAS.2016.7461337"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-319-47166-2_6","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"A Legay","year":"2016","unstructured":"Legay, A., Sedwards, S., Traonouez, L.-M.: Plasma lab: a modular statistical model checking platform. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 77\u201393. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_6"},{"key":"13_CR8","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). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"13_CR9","unstructured":"David, A., et al.: Statistical Model Checking for Stochastic Hybrid Systems. arXiv preprint arXiv:1208.3856 (2012)"},{"key":"13_CR10","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). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_25"},{"key":"13_CR11","unstructured":"Filipovikj, P., et al.: Analyzing Industrial Simulink Models by Statistical Model Checking. Technical Report (2017)"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30080-9_1","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"R Alur","year":"2004","unstructured":"Alur, R., Madhusudan, P.: Decision problems for timed automata: a survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1\u201324. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_1"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Marinescu, R., Mubeen, S., Seceleanu, C.: Pruning architectural models of automotive embedded systems via dependency analysis. In: Software Engineering and Advanced Applications (SEAA), 2016 42th Euromicro Conference on, pp. 293\u2013302. IEEE (2016)","DOI":"10.1109\/SEAA.2016.47"},{"key":"13_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-319-95582-7_23","volume-title":"Formal Methods","author":"J Nellen","year":"2018","unstructured":"Nellen, J., Rambow, T., Waez, M.T.B., \u00c1brah\u00e1m, E., Katoen, J.-P.: Formal verification of automotive simulink controller models: empirical technical challenges, evaluation and recommendations. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 382\u2013398. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_23"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-642-33675-1_38","volume-title":"Computer Safety, Reliability, and Security","author":"O Ferrante","year":"2012","unstructured":"Ferrante, O., Benvenuti, L., Mangeruca, L., Sofronis, C., Ferrari, A.: Parallel NuSMV: a NuSMV extension for the verification of complex embedded systems. In: Ortmeier, F., Daniel, P. (eds.) SAFECOMP 2012. LNCS, vol. 7613, pp. 409\u2013416. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33675-1_38"},{"key":"13_CR16","unstructured":"Bourbouh, H., Garoche, P.-L., Loquen, T., Noulard, \u00c9., Pagetti, C.: CoCoSim, a code generation framework for control\/command applications an overview of CoCoSim for multi- periodic discrete Simulink models. In: 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020). Springer (2020)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Hocking, A.B., Anthony Aiello, M., Knight, J.C., Ar\u00e9chiga, N.: Proving critical properties of simulink models. In: Proceedings of IEEE International Symposium on High Assurance Systems Engineering, vol. 2016, pp. 189\u2013196 (2016)","DOI":"10.1109\/HASE.2016.38"},{"key":"13_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/978-3-319-89963-3_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"I Dragomir","year":"2018","unstructured":"Dragomir, I., Preoteasa, V., Tripakis, S.: The refinement calculus of reactive systems toolset. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 201\u2013208. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_12"},{"key":"13_CR19","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). https:\/\/doi.org\/10.1007\/11901433_33"},{"key":"13_CR20","unstructured":"Manamcheri\u00a0Sukumar, K.: Translation of Simulink-Stateflow Models to Hybrid Automata (2011)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-95582-7_18","volume-title":"Formal Methods","author":"P Berger","year":"2018","unstructured":"Berger, P., Katoen, J.-P., \u00c1brah\u00e1m, E., Waez, M.T.B., Rambow, T.: Verifying auto-generated C code from Simulink. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 312\u2013328. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_18"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to Stateflow\/Simulink verification. Formal Methods Syst. Design 43(2), 338\u2013367 (2013)","DOI":"10.1007\/s10703-013-0195-3"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"Minopoli, S., Frehse, G.: SL2SX translator: from Simulink to SpaceEx models. In: Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control (HSCC 2016), pp. 93\u201398. ACM (2016)","DOI":"10.1145\/2883817.2883826"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/978-3-319-48989-6_46","volume-title":"FM 2016: Formal Methods","author":"P Filipovikj","year":"2016","unstructured":"Filipovikj, P., Mahmud, N., Marinescu, R., Seceleanu, C., Ljungkrantz, O., L\u00f6nn, H.: Simulink to UPPAAL statistical model checker: analyzing automotive industrial systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 748\u2013756. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_46"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Specification and Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75380-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,29]],"date-time":"2024-10-29T08:51:51Z","timestamp":1730191911000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75380-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,30]]},"ISBN":["9783031753794","9783031753800"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75380-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,30]]},"assertion":[{"value":"30 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Crete","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}