{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:13:16Z","timestamp":1750219996628,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,30]],"date-time":"2024-04-30T00:00:00Z","timestamp":1714435200000},"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":["ACM Trans. Cyber-Phys. Syst."],"published-print":{"date-parts":[[2024,4,30]]},"abstract":"<jats:p>Automotive cyber-physical systems consist of multiple control subsystems working under resource limitations, and the trend is to run the corresponding control tasks on a shared platform. The resource requirements of the tasks are usually variable at runtime due to the uncertainties in the environment, necessitating some kinds of adaptation to deal with the resource limitations. Such adaptations may positively or negatively affect the control performance of several subsystems. Since there might be some thresholds on the control performances as quality constraints, this matter should be considered carefully to avoid any quality attribute constraint violation. This article proposes a scalable control performance constraint verification method for such a system that works based on a feedback scheduler. The scalability is the result of a control-aware pruning method. In case of a constraint violation, the designer may change the system configuration and perform re-verification. Our evaluations show that the proposed method scales well while preserving the verification soundness.<\/jats:p>","DOI":"10.1145\/3576046","type":"journal-article","created":{"date-parts":[[2022,12,14]],"date-time":"2022-12-14T12:13:39Z","timestamp":1671020019000},"page":"1-19","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Control Performance Analysis of Automotive Cyber-physical Systems: A Study on Efficient Formal Verification"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5612-0832","authenticated-orcid":false,"given":"Vahid","family":"Panahi","sequence":"first","affiliation":[{"name":"School of Electrical and Computer Engineering, College of Engineering, University of Tehran, Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9300-4665","authenticated-orcid":false,"given":"Mehdi","family":"Kargahi","sequence":"additional","affiliation":[{"name":"School of Electrical and Computer Engineering, College of Engineering, University of Tehran and School of Computer Science, Institute for Research in Fundamental Sciences (IPM), Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8877-6895","authenticated-orcid":false,"given":"Fathiyeh","family":"Faghih","sequence":"additional","affiliation":[{"name":"School of Electrical and Computer Engineering, College of Engineering, University of Tehran, Tehran, Iran"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382217"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_3_2_4_2","first-page":"1758","article-title":"An efficient reachability-based framework for provably safe autonomous navigation in unknown environments","author":"Bajcsy Andrea","year":"2019","unstructured":"Andrea Bajcsy, Somil Bansal, Eli Bronstein, Varun Tolani, and Claire J. Tomlin. 2019. An efficient reachability-based framework for provably safe autonomous navigation in unknown environments. In Proceedings of the IEEE 58th Conference on Decision and Control (CDC\u201919). 1758\u20131765.","journal-title":"Proceedings of the IEEE 58th Conference on Decision and Control (CDC\u201919)"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2015.26"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA48506.2021.9561949"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/12.919277"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55089-9_2"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-0676-1"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2006.24"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2010.2053205"},{"key":"e_1_3_2_12_2","volume-title":"Reachability Analysis of Non-linear Hybrid Systems using Taylor Models","author":"Chen Xin","year":"2015","unstructured":"Xin Chen. 2015. Reachability Analysis of Non-linear Hybrid Systems using Taylor Models. Master\u2019s thesis. RWTH Aachen University."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.29007\/1w4t"},{"key":"e_1_3_2_14_2","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"Chen Xin","year":"2013","unstructured":"Xin Chen, Erika \u00c1brah\u00e1m, and Sriram Sankaranarayanan. 2013. Flow*: An analyzer for non-linear hybrid systems. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer, Berlin, 258\u2013263."},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2015.28"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/MEMOCODE51338.2020.9314994"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2014.28"},{"key":"e_1_3_2_19_2","volume-title":"Formal Verification of Collision Avoidance for Nonlinear Autonomous Vehicle Models","author":"Gu Rong","year":"2021","unstructured":"Rong Gu, Cristina Seceleanu, Eduard Paul Enoiu, and Kristina Lundqvist. 2021. Formal Verification of Collision Avoidance for Nonlinear Autonomous Vehicle Models. Technical Report."},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA48506.2021.9561561"},{"key":"e_1_3_2_21_2","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/978-3-030-53288-8_26","volume-title":"Computer Aided Verification","author":"Huang Chao","year":"2020","unstructured":"Chao Huang, Kai-Chieh Chang, Chung-Wei Lin, and Qi Zhu. 2020. SAW: A tool for safety analysis of weakly-hard systems. In Computer Aided Verification. Springer International Publishing, Cham, 543\u2013555."},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3302504.3311811"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3313151.3313165"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/3437539.3437620"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/IV47402.2020.9304710"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","unstructured":"Vahid Panahi and Mehdi Kargahi. 2018. Performance adaptation of real-time control tasks by dynamic scheduling: A self-triggered control approach. 80\u201387. 10.1109\/RTEST.2018.8397082","DOI":"10.1109\/RTEST.2018.8397082"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2012.6176523"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.5555\/248504"},{"key":"e_1_3_2_29_2","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/978-3-319-89963-3_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Schupp Stefan","year":"2018","unstructured":"Stefan Schupp and Erika \u00c1brah\u00e1m. 2018. Efficient dynamic error reduction for hybrid systems reachability analysis. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 287\u2013302."},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2021.3131607"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415676"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2020.3037561"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC42340.2020.9304431"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456643"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-60508-7_28"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/3394885.3431623"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3400302.3415768"}],"container-title":["ACM Transactions on Cyber-Physical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576046","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3576046","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:49:40Z","timestamp":1750182580000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3576046"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,30]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4,30]]}},"alternative-id":["10.1145\/3576046"],"URL":"https:\/\/doi.org\/10.1145\/3576046","relation":{},"ISSN":["2378-962X","2378-9638"],"issn-type":[{"type":"print","value":"2378-962X"},{"type":"electronic","value":"2378-9638"}],"subject":[],"published":{"date-parts":[[2024,4,30]]},"assertion":[{"value":"2021-07-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-09-20","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}