{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,17]],"date-time":"2023-01-17T12:30:32Z","timestamp":1673958632535},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","license":[{"start":{"date-parts":[[2020,10,8]],"date-time":"2020-10-08T00:00:00Z","timestamp":1602115200000},"content-version":"vor","delay-in-days":366,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"crossref","award":["N00014-17-1-2504"]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-19-1-0169"]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1652544, SaTC-1813388"]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2019,10,31]]},"abstract":"\n Many important properties of cyber-physical systems (CPS) are defined upon the relationship between multiple executions simultaneously in continuous time. Examples include probabilistic fairness and sensitivity to modeling errors (i.e., parameters changes) for real-valued signals. These requirements can only be specified by\n hyperproperties<\/jats:italic>\n . In this article, we focus on verifying probabilistic hyperproperties for CPS. To cover a wide range of modeling formalisms, we first propose a general model of probabilistic uncertain systems (PUSs) that unify commonly studied CPS models such as\n continuous-time Markov chains<\/jats:italic>\n (CTMCs) and\n probabilistically parametrized Hybrid I\/O Automata<\/jats:italic>\n (P\n 2<\/jats:sup>\n HIOA). To formally specify hyperproperties, we propose a new temporal logic,\n hyper probabilistic signal temporal logic<\/jats:italic>\n (HyperPSTL) that serves as a hyper and probabilistic version of the conventional signal temporal logic (STL). Considering the complexity of real-world systems that can be captured as PUSs, we adopt a\n statistical model checking<\/jats:italic>\n (SMC) approach for their verification. We develop a new SMC technique based on the direct computation of significance levels of statistical assertions for HyperPSTL specifications, which requires no\n a priori<\/jats:italic>\n knowledge on the indifference margin. Then, we introduce SMC algorithms for HyperPSTL specifications on the joint probabilistic distribution of multiple paths, as well as specifications with nested probabilistic operators quantifying different paths, which cannot be handled by existing SMC algorithms. Finally, we show the effectiveness of our SMC algorithms on CPS benchmarks with varying levels of complexity, including the Toyota Powertrain Control\u00a0System.\n <\/jats:p>","DOI":"10.1145\/3358232","type":"journal-article","created":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T13:13:05Z","timestamp":1570713185000},"page":"1-23","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Statistical Verification of Hyperproperties for Cyber-Physical Systems"],"prefix":"10.1145","volume":"18","author":[{"given":"Yu","family":"Wang","sequence":"first","affiliation":[{"name":"Duke University, Durham, NC"}]},{"given":"Mojtaba","family":"Zarei","sequence":"additional","affiliation":[{"name":"Duke University, Durham, NC"}]},{"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[{"name":"Iowa State University, Ames, IA"}]},{"given":"Miroslav","family":"Pajic","sequence":"additional","affiliation":[{"name":"Duke University, Durham, NC"}]}],"member":"320","published-online":{"date-parts":[[2019,10,8]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 12th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). 155--164","author":"Abbas H.","unstructured":"H. Abbas , H. D. Mittelmann , and G. E. Fainekos . 2014. Formal property verification in a conformance testing framework . In Proceedings of the 12th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). 155--164 . H. Abbas, H. D. Mittelmann, and G. E. Fainekos. 2014. Formal property verification in a conformance testing framework. In Proceedings of the 12th ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE). 155--164."},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Erika \u00c1brah\u00e1m and Borzoo Bonakdarpour. 2018. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Quantitative Evaluation of Systems. 20--35. Erika \u00c1brah\u00e1m and Borzoo Bonakdarpour. 2018. HyperPCTL: A temporal logic for probabilistic hyperproperties. In Quantitative Evaluation of Systems. 20--35.","DOI":"10.1007\/978-3-319-99154-2_2"},{"key":"e_1_2_1_3_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . The MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. The MIT Press."},{"key":"e_1_2_1_4_1","unstructured":"Beno\u00eet Barbot B\u00e9atrice B\u00e9rard Yann Duplouy and Serge Haddad. 2017. Statistical model-checking for autonomous vehicle safety validation. In SIA Simulation Num\u00e9rique. Beno\u00eet Barbot B\u00e9atrice B\u00e9rard Yann Duplouy and Serge Haddad. 2017. Statistical model-checking for autonomous vehicle safety validation. In SIA Simulation Num\u00e9rique."},{"key":"e_1_2_1_5_1","volume-title":"Hermann De Meer, and Kishor S. Trivedi","author":"Bolch Gunter","year":"2006","unstructured":"Gunter Bolch , Stefan Greiner , Hermann De Meer, and Kishor S. Trivedi . 2006 . Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications. John Wiley 8 Sons. Gunter Bolch, Stefan Greiner, Hermann De Meer, and Kishor S. Trivedi. 2006. Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications. John Wiley 8 Sons."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1214\/ss\/1009213286"},{"key":"e_1_2_1_7_1","volume-title":"Hyperproperties. In 2008 21st IEEE Computer Security Foundations Symposium. 51--65","author":"Michael","unstructured":"Michael R. Clarkson and Fred B. Schneider. 2008 . Hyperproperties. In 2008 21st IEEE Computer Security Foundations Symposium. 51--65 . Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In 2008 21st IEEE Computer Security Foundations Symposium. 51--65."},{"key":"e_1_2_1_8_1","volume-title":"Pearson","author":"Clopper Charles J.","year":"1934","unstructured":"Charles J. Clopper and Egon S . Pearson . 1934 . The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika ( 1934), 404--413. Charles J. Clopper and Egon S. Pearson. 1934. The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika (1934), 404--413."},{"key":"e_1_2_1_9_1","volume-title":"HyperPSTL Case Studies","unstructured":"CPSL@Duke. 2019. HyperPSTL Case Studies . http:\/\/cpsl.pratt.duke.edu\/research\/statistical-model-checking-hyperpstl. Accessed: 2019-7-15. CPSL@Duke. 2019. HyperPSTL Case Studies. http:\/\/cpsl.pratt.duke.edu\/research\/statistical-model-checking-hyperpstl. Accessed: 2019-7-15."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 26th European Symposium on Programming Languages and Systems (ESOP). 83--110","author":"D\u2019Argenio P. R.","unstructured":"P. R. D\u2019Argenio , G. Barthe , S. Biewer , B. Finkbeiner , and H. Hermanns . 2017. Is your software on dope? - Formal analysis of surreptitiously \u201cenhanced\u201d programs . In Proceedings of the 26th European Symposium on Programming Languages and Systems (ESOP). 83--110 . P. R. D\u2019Argenio, G. Barthe, S. Biewer, B. Finkbeiner, and H. Hermanns. 2017. Is your software on dope? - Formal analysis of surreptitiously \u201cenhanced\u201d programs. In Proceedings of the 26th European Symposium on Programming Languages and Systems (ESOP). 83--110."},{"key":"e_1_2_1_11_1","volume-title":"Meeting a powertrain verification challenge. In International Conference on Computer Aided Verification. Springer, 536--543","author":"Duggirala Parasara Sridhar","year":"2015","unstructured":"Parasara Sridhar Duggirala , Chuchu Fan , Sayan Mitra , and Mahesh Viswanathan . 2015 . Meeting a powertrain verification challenge. In International Conference on Computer Aided Verification. Springer, 536--543 . Parasara Sridhar Duggirala, Chuchu Fan, Sayan Mitra, and Mahesh Viswanathan. 2015. Meeting a powertrain verification challenge. In International Conference on Computer Aided Verification. Springer, 536--543."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2006.879361"},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Leonidas Georgiadis Michael J. Neely Leandros Tassiulas etal 2006. Resource allocation and cross-layer control in wireless networks. Foundations and Trends\u00ae in Networking 1 1 (2006) 1--144. Leonidas Georgiadis Michael J. Neely Leandros Tassiulas et al. 2006. Resource allocation and cross-layer control in wireless networks. Foundations and Trends\u00ae in Networking 1 1 (2006) 1--144.","DOI":"10.1561\/1300000001"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0021-9991(76)90041-3"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59615-5_13"},{"key":"e_1_2_1_17_1","volume-title":"Craig","author":"Hogg Robert V.","year":"2005","unstructured":"Robert V. Hogg , Joseph McKean , and Allen T . Craig . 2005 . Introduction to Mathematical Statistics. Pearson Education . Robert V. Hogg, Joseph McKean, and Allen T. Craig. 2005. Introduction to Mathematical Statistics. Pearson Education."},{"key":"e_1_2_1_18_1","volume-title":"1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH).","author":"Jin Xiaoqing","year":"2014","unstructured":"Xiaoqing Jin , Jyotirmoy V. Deshmukh , James Kapinski , Koichi Ueda , and Ken Butts . 2014 . Benchmarks for model transformations and conformance checking . In 1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH). Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts. 2014. Benchmarks for model transformations and conformance checking. In 1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH)."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562140"},{"key":"e_1_2_1_20_1","volume-title":"Larsen and Axel Legay","author":"Kim","year":"2016","unstructured":"Kim G. Larsen and Axel Legay . 2016 . Statistical model checking: past, present, and future. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques . 3--15. Kim G. Larsen and Axel Legay. 2016. Statistical model checking: past, present, and future. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques. 3--15."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0384-z"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"e_1_2_1_23_1","volume-title":"15th ACM-IEEE Int. Conf. on Formal Methods and Models for System Design. 104--113","author":"Nguyen Luan Viet","unstructured":"Luan Viet Nguyen , James Kapinski , Xiaoqing Jin , Jyotirmoy V. Deshmukh , and Taylor T. Johnson . 2017. Hyperproperties of real-valued signals . In 15th ACM-IEEE Int. Conf. on Formal Methods and Models for System Design. 104--113 . Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh, and Taylor T. Johnson. 2017. Hyperproperties of real-valued signals. In 15th ACM-IEEE Int. Conf. on Formal Methods and Models for System Design. 104--113."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049804"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.15607\/RSS.2016.XII.017"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Koushik Sen Mahesh Viswanathan and Gul Agha. 2005. On statistical model checking of stochastic systems. In Computer Aided Verification. 266--280. Koushik Sen Mahesh Viswanathan and Gul Agha. 2005. On statistical model checking of stochastic systems. In Computer Aided Verification. 266--280.","DOI":"10.1007\/11513988_26"},{"key":"e_1_2_1_27_1","volume-title":"Second International Conference on the Quantitative Evaluation of Systems. 251--252","author":"Sen K.","unstructured":"K. Sen , M. Viswanathan , and G. Agha . 2005. VESTA: A statistical model-checker and analyzer for probabilistic systems . In Second International Conference on the Quantitative Evaluation of Systems. 251--252 . K. Sen, M. Viswanathan, and G. Agha. 2005. VESTA: A statistical model-checker and analyzer for probabilistic systems. In Second International Conference on the Quantitative Evaluation of Systems. 251--252."},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Jeremy Sproston. 2000. Decidable model checking of probabilistic hybrid automata. In Formal Techniques in Real-Time and Fault-Tolerant Systems. 31--45. Jeremy Sproston. 2000. Decidable model checking of probabilistic hybrid automata. In Formal Techniques in Real-Time and Fault-Tolerant Systems. 31--45.","DOI":"10.1007\/3-540-45352-0_5"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2014.2315637"},{"key":"e_1_2_1_30_1","unstructured":"The MathWorks Inc. 2019. SimEvents. https:\/\/www.mathworks.com\/products\/simevents.html. Accessed: 2019-7-15. The MathWorks Inc. 2019. SimEvents. https:\/\/www.mathworks.com\/products\/simevents.html. Accessed: 2019-7-15."},{"key":"e_1_2_1_31_1","volume-title":"Statistical model checking for probabilistic hyperproperties. arXiv preprint arXiv:1902.04111","author":"Wang Yu","year":"2019","unstructured":"Yu Wang , Siddhartha Nalluri , Borzoo Bonakdarpour , and Miroslav Pajic . 2019. Statistical model checking for probabilistic hyperproperties. arXiv preprint arXiv:1902.04111 ( 2019 ). Yu Wang, Siddhartha Nalluri, Borzoo Bonakdarpour, and Miroslav Pajic. 2019. Statistical model checking for probabilistic hyperproperties. arXiv preprint arXiv:1902.04111 (2019)."},{"key":"e_1_2_1_32_1","volume-title":"55th Conference on Decision and Control (CDC). 3012--3017","author":"Wang Yu","unstructured":"Yu Wang , Nima Roohi , Matthew West , Mahesh Viswanathan , and Geir E. Dullerud . 2016. Verifying continuous-time stochastic hybrid systems via Mori-Zwanzig model reduction . In 55th Conference on Decision and Control (CDC). 3012--3017 . Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, and Geir E. Dullerud. 2016. Verifying continuous-time stochastic hybrid systems via Mori-Zwanzig model reduction. In 55th Conference on Decision and Control (CDC). 3012--3017."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2018.08.015"},{"key":"e_1_2_1_34_1","doi-asserted-by":"crossref","unstructured":"Lijun Zhang Zhikun She Stefan Ratschan Holger Hermanns and Ernst Moritz Hahn. 2010. Safety verification for probabilistic hybrid systems. In Computer Aided Verification. 196--211. Lijun Zhang Zhikun She Stefan Ratschan Holger Hermanns and Ernst Moritz Hahn. 2010. Safety verification for probabilistic hybrid systems. In Computer Aided Verification. 196--211.","DOI":"10.1007\/978-3-642-14295-6_21"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0343-0"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358232","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3358232","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T12:05:04Z","timestamp":1672574704000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3358232"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,8]]},"references-count":35,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2019,10,31]]}},"alternative-id":["10.1145\/3358232"],"URL":"http:\/\/dx.doi.org\/10.1145\/3358232","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":["Hardware and Architecture","Software"],"published":{"date-parts":[[2019,10,8]]},"assertion":[{"value":"2019-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-10-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}