{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:25:07Z","timestamp":1771889107066,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,10,7]],"date-time":"2020-10-07T00:00:00Z","timestamp":1602028800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,10,7]]},"DOI":"10.1145\/3372020.3391563","type":"proceedings-article","created":{"date-parts":[[2020,9,12]],"date-time":"2020-09-12T20:02:05Z","timestamp":1599940925000},"page":"34-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Impact Analysis of Cyber-Physical Attacks on a Water Tank System via Statistical Model Checking"],"prefix":"10.1145","author":[{"given":"Andrei","family":"Munteanu","sequence":"first","affiliation":[{"name":"University of Verona, Verona, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Pasqua","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Massimo","family":"Merro","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,7]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_1_2_1","volume-title":"QEST","author":"Behrmann G.","year":"2006","unstructured":"G. Behrmann , A. David , Larsen K. G., J. H\u00e5kansson , P. Pettersson , W. Yi , and M. Hendriks . 2006. UPPAAL 4.0 . In QEST 2006 . IEEE Computer Society, 125--126. G. Behrmann, A. David, Larsen K. G., J. H\u00e5kansson, P. Pettersson, W. Yi, and M. Hendriks. 2006. UPPAAL 4.0. In QEST 2006. IEEE Computer Society, 125--126."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1576303.1576304"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"C. Cheh A. Fawaz M. A. Noureddine B. Chen W. G. Temple and W. H. Sanders. 2018. Determining Tolerable Attack Surfaces that Preserves Safety of Cyber-Physical Systems. In PRDC. IEEE Computer Society 125--134.  C. Cheh A. Fawaz M. A. Noureddine B. Chen W. G. Temple and W. H. Sanders. 2018. Determining Tolerable Attack Surfaces that Preserves Safety of Cyber-Physical Systems. In PRDC. IEEE Computer Society 125--134.","DOI":"10.1109\/PRDC.2018.00023"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177700156"},{"key":"e_1_3_2_1_6_1","volume-title":"Model checking","author":"Clarke E. M.","unstructured":"E. M. Clarke , O. Grumberg , and D. A Peled . 2001. Model checking . MIT Press . E. M. Clarke, O. Grumberg, and D. A Peled. 2001. Model checking. MIT Press."},{"key":"e_1_3_2_1_7_1","volume-title":"Statistical Model Checking for Cyber-Physical Systems. In ATVA (LNCS)","volume":"6996","author":"Clarke E. M.","unstructured":"E. M. Clarke and P. Zuliani . 2011 . Statistical Model Checking for Cyber-Physical Systems. In ATVA (LNCS) , Vol. 6996 . Springer, 1--12. E. M. Clarke and P. Zuliani. 2011. Statistical Model Checking for Cyber-Physical Systems. In ATVA (LNCS), Vol. 6996. Springer, 1--12."},{"key":"e_1_3_2_1_8_1","volume-title":"Time for Statistical Model Checking of Real-Time Systems. In CAV (LNCS)","volume":"6806","author":"David D.","unstructured":"D. David , K. G. Larsen , A. Legay , M. Mikucionis , and Z. Wang . 2011 . Time for Statistical Model Checking of Real-Time Systems. In CAV (LNCS) , Vol. 6806 . Springer, 349--355. D. David, K. G. Larsen, A. Legay, M. Mikucionis, and Z. Wang. 2011. Time for Statistical Model Checking of Real-Time Systems. In CAV (LNCS), Vol. 6806. Springer, 349--355."},{"key":"e_1_3_2_1_9_1","first-page":"1","article-title":"TRITON","volume":"2018","author":"Pinto A. Di","year":"2018","unstructured":"A. Di Pinto , Y. Dragoni , and A. Carcano . 2018 . TRITON : The First ICS Cyber Attack on Safety Instrument Systems. In Black Hat USA 2018. 1 -- 28 . A. Di Pinto, Y. Dragoni, and A. Carcano. 2018. TRITON: The First ICS Cyber Attack on Safety Instrument Systems. In Black Hat USA 2018. 1--28.","journal-title":"In Black Hat USA"},{"key":"e_1_3_2_1_10_1","unstructured":"R. C. Dorf and R. H. Bishop. 2011. Modern control systems. Pearson.  R. C. Dorf and R. H. Bishop. 2011. Modern control systems. Pearson."},{"key":"e_1_3_2_1_11_1","unstructured":"N. Falliere L. Murchu and E. Chien. 2011. W32.Stuxnet Dossier.  N. Falliere L. Murchu and E. Chien. 2011. W32.Stuxnet Dossier."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0167-z"},{"key":"e_1_3_2_1_13_1","volume-title":"TACAS (LNCS)","volume":"8413","author":"Hartmanns A.","unstructured":"A. Hartmanns and H. Hermanns . 2014. The Modest Toolset: An integrated environment for quantitative modelling and verification . In TACAS (LNCS) , Vol. 8413 . Springer, 593--598. A. Hartmanns and H. Hermanns. 2014. The Modest Toolset: An integrated environment for quantitative modelling and verification. In TACAS (LNCS), Vol. 8413. Springer, 593--598."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/57.1.97"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"e_1_3_2_1_16_1","volume-title":"FASE (LNCS)","author":"Huang L.","unstructured":"L. Huang and E.-Y. Kang . 2019. Formal Verification of Safety & Security Related Timing Constraints for a Cooperative Automotive System . In FASE (LNCS) , Vol. 11424 . Springer , 210--227. L. Huang and E.-Y. Kang. 2019. Formal Verification of Safety & Security Related Timing Constraints for a Cooperative Automotive System. In FASE (LNCS), Vol. 11424. Springer, 210--227."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijcip.2009.06.001"},{"key":"e_1_3_2_1_18_1","unstructured":"ICS-CERT. 2015. Cyber-Attack Against Ukrainian Critical Infrastructure. (2015). https:\/\/ics-cert.us-cert.gov\/alerts\/IR-ALERT-H-16-056-01.  ICS-CERT. 2015. Cyber-Attack Against Ukrainian Critical Infrastructure. (2015). https:\/\/ics-cert.us-cert.gov\/alerts\/IR-ALERT-H-16-056-01."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/87.845876"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"R. Kumar and M. Stoelinga. 2017. Quantitative Security and Safety Analysis with Attack-Fault Trees. In HASE. IEEE Computer Society 25--32.  R. Kumar and M. Stoelinga. 2017. Quantitative Security and Safety Analysis with Attack-Fault Trees. In HASE. IEEE Computer Society 25--32.","DOI":"10.1109\/HASE.2017.12"},{"key":"e_1_3_2_1_21_1","volume-title":"CAV (LNCS)","volume":"6806","author":"Kwiatkowska M. Z.","unstructured":"M. Z. Kwiatkowska , G. Norman , and D. Parker . 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems . In CAV (LNCS) , Vol. 6806 . Springer, 585--591. M. Z. Kwiatkowska, G. Norman, and D. Parker. 2011. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV (LNCS), Vol. 6806. Springer, 585--591."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"R. Lanotte M. Merro and F. Mogavero. 2019. On the decidability of linear bounded periodic cyber-physical systems. In HSCC. ACM 87--98.  R. Lanotte M. Merro and F. Mogavero. 2019. On the decidability of linear bounded periodic cyber-physical systems. In HSCC. ACM 87--98.","DOI":"10.1145\/3302504.3311797"},{"key":"e_1_3_2_1_23_1","volume-title":"FORTE (LNCS)","volume":"10854","author":"Lanotte R.","unstructured":"R. Lanotte , M. Merro , and A. Munteanu . 2018. A Modest Security Analysis of Cyber-Physical Systems: A Case Study . In FORTE (LNCS) , Vol. 10854 . Springer, 58--78. R. Lanotte, M. Merro, and A. Munteanu. 2018. A Modest Security Analysis of Cyber-Physical Systems: A Case Study. In FORTE (LNCS), Vol. 10854. Springer, 58--78."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373270"},{"key":"e_1_3_2_1_25_1","volume-title":"IFM (LNCS)","volume":"11023","author":"Lanotte R.","unstructured":"R. Lanotte , M. Merro , and S. Tini . 2018. Towards a Formal Notion of Impact Metric for Cyber-Physical Attacks . In IFM (LNCS) , Vol. 11023 . Springer, 296--315. R. Lanotte, M. Merro, and S. Tini. 2018. Towards a Formal Notion of Impact Metric for Cyber-Physical Attacks. In IFM (LNCS), Vol. 11023. Springer, 296--315."},{"key":"e_1_3_2_1_26_1","volume-title":"Statistical Model Checking: An Overview. In RV (LNCS)","volume":"6418","author":"Legay A.","unstructured":"A. Legay , B. Delahaye , and S. Bensalem . 2010 . Statistical Model Checking: An Overview. In RV (LNCS) , Vol. 6418 . Springer, 122--135. A. Legay, B. Delahaye, and S. Bensalem. 2010. Statistical Model Checking: An Overview. In RV (LNCS), Vol. 6418. Springer, 122--135."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9001-5"},{"key":"e_1_3_2_1_28_1","volume-title":"AVATAR: A SysML Environment for the Formal Verification of Safety and Security Properties","author":"Pedroza G.","year":"2011","unstructured":"G. Pedroza , L. Apvrille , and D. Knorreck . 2011 . AVATAR: A SysML Environment for the Formal Verification of Safety and Security Properties . In NOTERE. IEEE , 1--10. G. Pedroza, L. Apvrille, and D. Knorreck. 2011. AVATAR: A SysML Environment for the Formal Verification of Safety and Security Properties. In NOTERE. IEEE, 1--10."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.envsoft.2018.11.008"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"crossref","unstructured":"D. I. Urbina J. A. Giraldo A. A. Cardenas N. O. Tippenhauer J. Valente M. Faisal J. Ruths R. Candell and H. Sandberg. 2016. Limiting the Impact of Stealthy Attacks on Industrial Control Systems. In ACM CCS. ACM 1092--1105.  D. I. Urbina J. A. Giraldo A. A. Cardenas N. O. Tippenhauer J. Valente M. Faisal J. Ruths R. Candell and H. Sandberg. 2016. Limiting the Impact of Stealthy Attacks on Industrial Control Systems. In ACM CCS. ACM 1092--1105.","DOI":"10.1145\/2976749.2978388"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.procs.2016.09.289"},{"key":"e_1_3_2_1_32_1","volume-title":"Cyber-Physical Systems Security: a Systematic Mapping Study. CoRR abs\/1605.09641","author":"Lun Y. Zacchia","year":"2016","unstructured":"Y. Zacchia Lun , A. D'Innocenzo , I. Malavolta , and M. D. Di Benedetto . 2016. Cyber-Physical Systems Security: a Systematic Mapping Study. CoRR abs\/1605.09641 ( 2016 ). arXiv:1605.09641 Y. Zacchia Lun, A. D'Innocenzo, I. Malavolta, and M. D. Di Benedetto. 2016. Cyber-Physical Systems Security: a Systematic Mapping Study. CoRR abs\/1605.09641 (2016). arXiv:1605.09641"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2018.12.006"}],"event":{"name":"FormaliSE '20: 8th International Conference on Formal Methods in Software Engineering","location":"Seoul Republic of Korea","acronym":"FormaliSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"]},"container-title":["Proceedings of the 8th International Conference on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391563","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372020.3391563","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:44:19Z","timestamp":1750203859000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372020.3391563"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,7]]},"references-count":33,"alternative-id":["10.1145\/3372020.3391563","10.1145\/3372020"],"URL":"https:\/\/doi.org\/10.1145\/3372020.3391563","relation":{},"subject":[],"published":{"date-parts":[[2020,10,7]]},"assertion":[{"value":"2020-10-07","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}