{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,19]],"date-time":"2025-09-19T08:14:24Z","timestamp":1758269664574,"version":"3.41.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2018,1,22]],"date-time":"2018-01-22T00:00:00Z","timestamp":1516579200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Key R8D Program of China","award":["2017YFB1001801"],"award-info":[{"award-number":["2017YFB1001801"]}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation","doi-asserted-by":"crossref","award":["61690204 and 61472174"],"award-info":[{"award-number":["61690204 and 61472174"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004608","name":"Natural Science Foundation of Jiangsu Province","doi-asserted-by":"crossref","award":["BK20150589"],"award-info":[{"award-number":["BK20150589"]}],"id":[{"id":"10.13039\/501100004608","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Internet Technol."],"published-print":{"date-parts":[[2018,5,31]]},"abstract":"<jats:p>Cyber-Physical Systems (CPS) intrinsically combine hardware and physical systems with software and network, which are together creating complex and correlated interactions. CPS applications often experience uncertainty in interacting with environment through unreliable sensors. They can be faulty and exhibit runtime errors if developers have not considered environmental interaction uncertainty adequately. Existing work in verifying CPS applications ignores interaction uncertainty and thus may overlook uncertainty-related faults. To improve verification accuracy, in this article we propose a novel approach to verifying CPS applications with explicit modeling of uncertainty arisen in the interaction between them and the environment. Our approach builds an Interactive State Machine network for a CPS application and models interaction uncertainty by error ranges and distributions. Then it encodes both the application and uncertainty models to Satisfiability Modulo Theories (SMT) formula to leverage SMT solvers searching for counterexamples that represent application failures. The precision of uncertainty model can affect the verification results. However, it may be difficult to model interaction uncertainty precisely enough at the beginning, because of the uncontrollable noise of sensors and insufficient data sample size. To further improve the accuracy of the verification results, we propose an approach to identifying and calibrating imprecise uncertainty models. We exploit the inconsistency between the counterexamples\u2019 estimate and actual occurrence probabilities to identify possible imprecision in uncertainty models, and the calibration of imprecise models is to minimize the inconsistency, which is reduced to a Search-Based Software Engineering problem. We experimentally evaluated our verification and calibration approaches with real-world CPS applications, and the experimental results confirmed their effectiveness and efficiency.<\/jats:p>","DOI":"10.1145\/3093894","type":"journal-article","created":{"date-parts":[[2018,1,23]],"date-time":"2018-01-23T14:53:36Z","timestamp":1516719216000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Improving Verification Accuracy of CPS by Modeling and Calibrating Interaction Uncertainty"],"prefix":"10.1145","volume":"18","author":[{"given":"Wenhua","family":"Yang","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology and Department of Computer Science and Technology, Nanjing University, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chang","family":"Xu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology and Department of Computer Science and Technology, Nanjing University, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Minxue","family":"Pan","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology and Software Institute, Nanjing University, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaoxing","family":"Ma","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology and Department of Computer Science and Technology, Nanjing University, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jian","family":"Lu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology and Department of Computer Science and Technology, Nanjing University, P.R. China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,1,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Sara Abbaspour Asadollah Rafia Inam and Hans Hansson. 2015. A Survey on Testing for Cyber Physical System. Springer Cham 194--207.  Sara Abbaspour Asadollah Rafia Inam and Hans Hansson. 2015. A Survey on Testing for Cyber Physical System. Springer Cham 194--207.","DOI":"10.1007\/978-3-319-25945-1_12"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2009.101"},{"volume-title":"Proceedings of the 2015 IEEE 8th International Conference on Software Testing, Verification and Validation (ICST\u201915)","author":"Ali S.","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Cesare Alippi. 2014. Intelligence for Embedded Systems. Springer Berlin.   Cesare Alippi. 2014. Intelligence for Embedded Systems. Springer Berlin.","DOI":"10.1007\/978-3-319-05278-6"},{"key":"e_1_2_1_5_1","unstructured":"Christel Baier Joost-Pieter Katoen and others. 2008. Principles of Model Checking. MIT Press Cambridge.   Christel Baier Joost-Pieter Katoen and others. 2008. Principles of Model Checking. MIT Press Cambridge."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2165689"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2016.46"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1002\/hyp.3360060305"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508443.2508452"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04425-0_36"},{"volume-title":"Proceedings of the 9th International Conference on Automated Technology for Verification and Analysis (ATVA\u201911)","year":"2050","author":"Edmund","key":"e_1_2_1_11_1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2666608"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2834965.2834968"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.csi.2016.11.003"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2014.55"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Andrew Gelman B. Carlin John S. Stern Hal and Donald B. Rubin. 2014. Bayesian Data Analysis. Chapman 8 Hall\/CRC Press.  Andrew Gelman B. Carlin John S. Stern Hal and Donald B. Rubin. 2014. Bayesian Data Analysis. Chapman 8 Hall\/CRC Press.","DOI":"10.1201\/b16018"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_19"},{"key":"e_1_2_1_19_1","unstructured":"David E. Goldberg. 1989. Genetic Algorithms in Search Optimization and Machine Learning (1st ed.). Addison-Wesley Longman Boston MA.   David E. Goldberg. 1989. Genetic Algorithms in Search Optimization and Machine Learning (1st ed.). Addison-Wesley Longman Boston MA."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25231-0_1"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSEN.2013.2271721"},{"volume-title":"Proceedings of the 16th IEEE Real-Time Systems Symposium. 56--65","author":"Henzinger T. A.","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","unstructured":"John H. Holland. 1975. Adaptation in Natural and Artificial Systems. University of Michigan Press.  John H. Holland. 1975. Adaptation in Natural and Artificial Systems. University of Michigan Press."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1795194.1795205"},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/BF00047572","article-title":"Simulated annealing: Theory and applications","volume":"12","author":"Hwang Chii-Ruey","year":"1988","journal-title":"Acta Appl. Math."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2014.28"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"S. Kirkpatrick C. D. Gelatt and M. P. Vecchi. 1983. Optimization by simulated annealing. Science 220 4598 (1983) 671--680. arXiv: http:\/\/science.sciencemag.org\/content\/220\/4598\/671.full.pdf  S. Kirkpatrick C. D. Gelatt and M. P. Vecchi. 1983. Optimization by simulated annealing. Science 220 4598 (1983) 671--680. arXiv: http:\/\/science.sciencemag.org\/content\/220\/4598\/671.full.pdf","DOI":"10.1126\/science.220.4598.671"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228484"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/355769.355773"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2008.25"},{"key":"e_1_2_1_31_1","unstructured":"Jian L\u00fc Yu Huang Chang Xu and Xiaoxing Ma. 2013. Theories of Programming and Formal Methods. Springer-Verlag Berlin 271--284. http:\/\/dl.acm.org\/citation.cfm?id&equals;2554641.2554658  Jian L\u00fc Yu Huang Chang Xu and Xiaoxing Ma. 2013. Theories of Programming and Formal Methods. Springer-Verlag Berlin 271--284. http:\/\/dl.acm.org\/citation.cfm?id&equals;2554641.2554658"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640206.1640213"},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Atif Mashkoor and Osman Hasan. 2012. Formal Probabilistic Analysis of Cyber-Physical Transportation Systems. Springer Berlin 419--434.  Atif Mashkoor and Osman Hasan. 2012. Formal Probabilistic Analysis of Cyber-Physical Transportation Systems. Springer Berlin 419--434.","DOI":"10.1007\/978-3-642-31137-6_32"},{"key":"e_1_2_1_34_1","unstructured":"MathWorks. 2017. MATLAB. Retrieved from http:\/\/www.mathworks.com\/.  MathWorks. 2017. MATLAB. Retrieved from http:\/\/www.mathworks.com\/."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2012.189"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2013.77"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1137\/0904038"},{"key":"e_1_2_1_38_1","unstructured":"John Neter Michael H. Kutner Christopher J. Nachtsheim and William Wasserman. 1996. Applied Linear Statistical Models. Vol. 4. Irwin Chicago IL.  John Neter Michael H. Kutner Christopher J. Nachtsheim and William Wasserman. 1996. Applied Linear Statistical Models. Vol. 4. Irwin Chicago IL."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837461"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1002\/9780470549124"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340492"},{"volume":"1","volume-title":"Parallel Distributed Processing: Explorations in the Microstructure of Cognition","author":"Rumelhart D. E.","key":"e_1_2_1_42_1"},{"volume":"2","volume-title":"Artificial Intelligence: A Modern Approach","author":"Russell Stuart Jonathan","key":"e_1_2_1_43_1"},{"key":"e_1_2_1_44_1","doi-asserted-by":"crossref","unstructured":"Muhammad Usman Sanwal and Osman Hasan. 2013. Formal Verification of Cyber-Physical Systems: Coping with Continuous Elements. Springer Berlin 358--371.  Muhammad Usman Sanwal and Osman Hasan. 2013. Formal Verification of Cyber-Physical Systems: Coping with Continuous Elements. Springer Berlin 358--371.","DOI":"10.1007\/978-3-642-39637-3_29"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.1539-6924.1989.tb01007.x"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/646511.695177"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2554850.2555028"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018628609742"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2351632"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2009.41"},{"key":"e_1_2_1_51_1","doi-asserted-by":"crossref","unstructured":"Tazio Vanni Jonathan Karnon Jason Madan Richard G. White W. John Edmunds Anna M. Foss and Rosa Legood. 2011. Calibrating models in economic evaluation. PharmacoEconom. 29 (Jan. 2011) 35--49.  Tazio Vanni Jonathan Karnon Jason Madan Richard G. White W. John Edmunds Anna M. Foss and Rosa Legood. 2011. Calibrating models in economic evaluation. PharmacoEconom. 29 (Jan. 2011) 35--49.","DOI":"10.2165\/11584600-000000000-00000"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1115\/94-GT-058"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00175354"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2011.03.003"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693118"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642999"},{"key":"e_1_2_1_57_1","first-page":"15","article-title":"Test case generation from formal models of cyber physical system","volume":"6","author":"Zhang Lichen","year":"2013","journal-title":"Int. J. Hybrid Inf. Technol."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-42061-5_16"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/PerComW.2014.6815195"}],"container-title":["ACM Transactions on Internet Technology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3093894","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3093894","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:30:16Z","timestamp":1750217416000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3093894"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,22]]},"references-count":59,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,5,31]]}},"alternative-id":["10.1145\/3093894"],"URL":"https:\/\/doi.org\/10.1145\/3093894","relation":{},"ISSN":["1533-5399","1557-6051"],"issn-type":[{"type":"print","value":"1533-5399"},{"type":"electronic","value":"1557-6051"}],"subject":[],"published":{"date-parts":[[2018,1,22]]},"assertion":[{"value":"2016-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}