{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T14:44:23Z","timestamp":1740149063909,"version":"3.37.3"},"reference-count":42,"publisher":"Wiley","license":[{"start":{"date-parts":[[2021,5,17]],"date-time":"2021-05-17T00:00:00Z","timestamp":1621209600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Key Research and Development Program of China","award":["2018YFB1003900","61772270","NJ2019006"],"award-info":[{"award-number":["2018YFB1003900","61772270","NJ2019006"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["2018YFB1003900","61772270","NJ2019006"],"award-info":[{"award-number":["2018YFB1003900","61772270","NJ2019006"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004193","name":"Nanjing University of Aeronautics and Astronautics","doi-asserted-by":"publisher","award":["2018YFB1003900","61772270","NJ2019006"],"award-info":[{"award-number":["2018YFB1003900","61772270","NJ2019006"]}],"id":[{"id":"10.13039\/501100004193","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006579","name":"Ministry of Industry and Information Technology of the People's Republic of China","doi-asserted-by":"publisher","award":["2018YFB1003900","61772270","NJ2019006"],"award-info":[{"award-number":["2018YFB1003900","61772270","NJ2019006"]}],"id":[{"id":"10.13039\/501100006579","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Security and Communication Networks"],"published-print":{"date-parts":[[2021,5,17]]},"abstract":"<jats:p>Safety-Critical Cyber-Physical System (SCCPS) refers to the system that if the system fails or its key functions fail, it will cause casualties, property damage, environmental damage, and other catastrophic consequences. Therefore, it is vital to verify the safety of safety critical systems. In the community, the SCCPS safety verification mainly relies on the statistical model checking methodology, but for SCCPS with extremely high safety requirements, the statistical model checking method is difficult\/infeasible to sample the extremely small probability event since the probability of the system violating the safety is very low (rare property). In response to this problem, we propose a new method of statistical model checking for high-safety SCCPS. Firstly, with the CTMC-approximated SCCPS path probability space model, it leverages the maximum likelihood estimation method to learn the parameters of CTMC. Then, the embedded DTMC can be derived from CTMC, and a cross-entropy optimization model based on DTMC can be constructed. Finally, we propose an algorithm of iteratively learning the optimal importance sampling distribution on the discrete path space and an algorithm to check the statistical model of verifying the rare attribute. Eventually, experimental results show that the method proposed in this paper can effectively verify the rare attributes of SCCPS. Under the same sample size, comparing with the heuristic importance sampling methods, the estimated value of this method can be better distributed around the mean value, and the related standard deviation and relative error are reduced by more than an order of magnitude.<\/jats:p>","DOI":"10.1155\/2021\/5536722","type":"journal-article","created":{"date-parts":[[2021,5,18]],"date-time":"2021-05-18T20:50:09Z","timestamp":1621371009000},"page":"1-12","source":"Crossref","is-referenced-by-count":4,"title":["Towards a Statistical Model Checking Method for Safety-Critical Cyber-Physical System Verification"],"prefix":"10.1155","volume":"2021","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3215-4691","authenticated-orcid":true,"given":"Jian","family":"Xie","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China"},{"name":"Key Laboratory of Safety-Critical Software, Nanjing University of Aeronautics and Astronautics, Nanjing, China"},{"name":"Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wenan","family":"Tan","sequence":"additional","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China"},{"name":"Key Laboratory of Safety-Critical Software, Nanjing University of Aeronautics and Astronautics, Nanjing, China"},{"name":"Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5010-0611","authenticated-orcid":true,"given":"Bingwu","family":"Fang","sequence":"additional","affiliation":[{"name":"Key Laboratory of Safety-Critical Software, Nanjing University of Aeronautics and Astronautics, Nanjing, China"},{"name":"College of Information Engineering, Anhui Finance and Trade Vocational College, Hefei, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiqiu","family":"Huang","sequence":"additional","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, China"},{"name":"Key Laboratory of Safety-Critical Software, Nanjing University of Aeronautics and Astronautics, Nanjing, China"},{"name":"Collaborative Innovation Center of Novel Software Technology and Industrialization, Nanjing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"key":"1","doi-asserted-by":"publisher","DOI":"10.1177\/1045389x03014001005"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.2136\/vzj2002.0186"},{"key":"3","article-title":"Revocable identitybased broadcast proxy re-encryption for data sharing in clouds","volume":"99","author":"G. Chunpeng","year":"2019","journal-title":"IEEE Transactions on Dependable and Secure Computing"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1631\/jzus.c0910684"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1631\/jzus.c1000045"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1631\/jzus.c0910377"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1631\/jzus.c1000224"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1631\/jzus.c1000361"},{"key":"9","first-page":"93","volume-title":"Order through Fluctuation: Self-Organization and Social System","author":"I. Prigogine","year":"1976"},{"key":"10","article-title":"Secure keyword search and data sharing mechanism for cloud computing","volume":"5","author":"C. Ge","year":"2020","journal-title":"IEEE Transactions on Dependable and Secure Computing"},{"key":"11","article-title":"Study on zoelite enhanced contact-adsorption regeneration-stabilization process for nitrogen removal","volume":"156","author":"Z. Wu","year":"2008","journal-title":"Journal of Hazardous Materials"},{"key":"12","first-page":"142","article-title":"Error control for probabilistic model checking","volume-title":"Lecture Notes in Computer Science","author":"H. L. S. Younes","year":"2006"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33365-1_2"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23401-4_3"},{"first-page":"443","article-title":"A novel sma-based actuator for a legged endoscopic capsule","author":"S. Gorini","key":"15"},{"volume-title":"Combined Multiple Transmit Antennas and Multi-Level Modulation Techniques","year":"2006","author":"U. Rizvi","key":"16"},{"first-page":"217","article-title":"Rare-event verification for stochastic hybrid systems,","author":"P. Zuliani","key":"17"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0195-3"},{"issue":"2","key":"19","first-page":"305","article-title":"Statistical model checking for rare-event in safety-critical system","volume":"26","author":"D. Du","year":"2015","journal-title":"Journal of Software in Chinese"},{"key":"20","unstructured":"SweeneyL.Uniqueness of simple demographics in the U.S. population2000Pittsburgh, PA, USACarnegie Mellon UniversityTechnical Report No. LIDAP-WP4"},{"key":"21","unstructured":"ISOSteels-classification-part 1: classification of steels into unalloyed and alloy steels based on chemical composition1982Geneva, SwitzerlandISOTechnical Report ISO 4948-1"},{"first-page":"251","article-title":"Rare event simulation for highly dependable systems with fast repairs","author":"D. Reijsbergen","key":"22"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_23"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24372-1_1"},{"volume-title":"Citing Electronic Sources of Information","year":"2001","author":"University","key":"25"},{"key":"26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/j.tcs.2016.08.009","article-title":"Command-based importance sampling for statistical model checking","volume":"649","author":"C. J\u00b4egourel","year":"2016","journal-title":"Theoretical Computer Science"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.05.002"},{"key":"28","first-page":"73","article-title":"Approximate probabilistic model checking","volume-title":"Lecture Notes in Computer Science","author":"T. H\u00b4erault","year":"2004"},{"first-page":"162","article-title":"Statistical moHaifa, Israeldel checking for safety critical hybrid systems: an empirical evaluation","author":"Y. J. Kim","key":"29"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1145\/3158668"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0384-z"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46430-1_16"},{"key":"33","first-page":"143","article-title":"An effective heuristic for adaptive importance splitting in statistical model checking","volume-title":"Lecture Notes in Computer Science","author":"C. J\u00b4egourel","year":"2014"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1109\/tac.2017.2758171"},{"volume-title":"Handbook of monte carlo methods","year":"2013","author":"D. P. Kroese","key":"35"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1007\/s10479-005-5724-z"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1016\/j.orl.2006.11.005"},{"key":"38","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_12"},{"key":"39","doi-asserted-by":"publisher","DOI":"10.1109\/jproc.2009.2039551"},{"key":"40","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2011.11.004"},{"key":"41","doi-asserted-by":"publisher","DOI":"10.1109\/tcad.2014.2299957"},{"article-title":"Feedback control for statistical model checking of cyber-physical systems","author":"K. Kalajdzic","key":"42","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-47166-2_4"}],"container-title":["Security and Communication Networks"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/scn\/2021\/5536722.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/scn\/2021\/5536722.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/scn\/2021\/5536722.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,18]],"date-time":"2021-05-18T20:50:32Z","timestamp":1621371032000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.hindawi.com\/journals\/scn\/2021\/5536722\/"}},"subtitle":[],"editor":[{"given":"Weizhi","family":"Meng","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2021,5,17]]},"references-count":42,"alternative-id":["5536722","5536722"],"URL":"https:\/\/doi.org\/10.1155\/2021\/5536722","relation":{},"ISSN":["1939-0122","1939-0114"],"issn-type":[{"type":"electronic","value":"1939-0122"},{"type":"print","value":"1939-0114"}],"subject":[],"published":{"date-parts":[[2021,5,17]]}}}