{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T18:23:07Z","timestamp":1762280587680,"version":"build-2065373602"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"5s","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>\n                    Real-time scheduling of multiple control tasks in a\n                    <jats:italic toggle=\"yes\">weakly hard<\/jats:italic>\n                    setting is an emerging research direction, as it offers a more flexible and feasible environment for task scheduling. This is especially pertinent for resource-constrained embedded applications where tasks are allowed to miss a few deadlines for prudent sharing of computational resources. However, a control task missing its deadline could result in the system being unsafe or unstable. A significant amount of research efforts have been reported in the literature addressing the schedulability of control tasks while preserving the stability or safety. However, all of them focus on a stable schedule or a safe schedule, but not both the safety and stability aspects together. In this work, we ensure both control stability and control safety to generate a\n                    <jats:italic toggle=\"yes\">safe and stable schedule<\/jats:italic>\n                    for a weakly hard task system. In particular, we gradually endorse stability, safety, and schedulability, where we first synthesize a weakly hard constraint that preserves the desired stability of each control task. Next, we correlate stability with control safety and establish some mathematical results that guarantee control safety for an unbounded time horizon, unlike the existing methods. Finally, by leveraging\n                    <jats:italic toggle=\"yes\">Satisfiability Modulo Theories (SMT)<\/jats:italic>\n                    , we synthesize the schedule that ensures control stability and safety while minimizing the\n                    <jats:italic toggle=\"yes\">worst-case response time<\/jats:italic>\n                    of all the tasks, in a time-efficient way. To our knowledge, this is the first work to address\n                    <jats:italic toggle=\"yes\">stability, safety, and schedulability<\/jats:italic>\n                    together for weakly hard control task systems. We validate our method through extensive experiments using standard automotive benchmarks. In addition, we demonstrate the efficiency of the proposed method in comparison with some of the state-of-the-art techniques, as well as highlight its scalability, thereby establishing its applicability in real-world scenarios.\n                  <\/jats:p>","DOI":"10.1145\/3760528","type":"journal-article","created":{"date-parts":[[2025,8,12]],"date-time":"2025-08-12T11:29:26Z","timestamp":1754998166000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Formal Approach towards Safe and Stable Schedule Synthesis in Weakly Hard Control Systems"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-6193-4716","authenticated-orcid":false,"given":"Debarpita","family":"Banerjee","sequence":"first","affiliation":[{"name":"Computer and Communication Sciences Division, Indian Statistical Institute","place":["Kolkata-700108, India"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8871-0298","authenticated-orcid":false,"given":"Parasara Sridhar","family":"Duggirala","sequence":"additional","affiliation":[{"name":"Computer Science, University of North Carolina at Chapel Hill College of Arts and Sciences","place":["Chapel Hill, United States"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1371-2803","authenticated-orcid":false,"given":"Bineet","family":"Ghosh","sequence":"additional","affiliation":[{"name":"Computer Science, The University of Alabama System","place":["Tuscaloosa, United States"]}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5999-3313","authenticated-orcid":false,"given":"Sumana","family":"Ghosh","sequence":"additional","affiliation":[{"name":"Computer and Communication Sciences Division, Indian Statistical Institute","place":["Kolkata-700108, India"]}]}],"member":"320","published-online":{"date-parts":[[2025,9,26]]},"reference":[{"key":"e_1_3_1_2_2","first-page":"81","volume-title":"Proceedings of the CPS&IoT Security and Privacy (CPSIoTSec)","year":"2020","unstructured":"Sunandan Adhikary, Ipsita Koley, Saurav Kumar Ghosh, Sumana Ghosh, Soumyajit Dey, and Debdeep Mukhopadhyay. 2020. Skip to secure: Securing cyber-physical control loops with intentionally skipped executions. In Proceedings of the CPS&IoT Security and Privacy (CPSIoTSec). 81\u201386."},{"doi-asserted-by":"publisher","key":"e_1_3_1_3_2","DOI":"10.1109\/RTSS55097.2022.00025"},{"doi-asserted-by":"publisher","key":"e_1_3_1_4_2","DOI":"10.1109\/12.919277"},{"doi-asserted-by":"publisher","key":"e_1_3_1_5_2","DOI":"10.1109\/CDC.2015.7403405"},{"doi-asserted-by":"publisher","key":"e_1_3_1_6_2","DOI":"10.1587\/transinf.2016EDP7374"},{"doi-asserted-by":"publisher","key":"e_1_3_1_7_2","DOI":"10.1109\/JIOT.2021.3058215"},{"key":"e_1_3_1_8_2","first-page":"327","volume-title":"Proceedings of the Real-Time and Embedded Technology and Applications Symposium (RTAS)","year":"2018","unstructured":"Hoon Sung Chwa, Kang G. Shin, and Jinkyu Lee. 2018. Closing the gap between stability and schedulability: A new task model for cyber-physical systems. In Proceedings of the Real-Time and Embedded Technology and Applications Symposium (RTAS). 327\u2013337."},{"key":"e_1_3_1_9_2","first-page":"11","volume-title":"Proceedings of the Embedded and Real-Time Computing Systems and Applications (RTCSA)","year":"2022","unstructured":"Bineet Ghosh, Clara Hobbs, Shengjie Xu, Parasara Sridhar Duggirala, James H. Anderson, P. S. Thiagarajan, and Samarjit Chakraborty. 2022. Statistical hypothesis testing of controller implementations under timing uncertainties. In Proceedings of the Embedded and Real-Time Computing Systems and Applications (RTCSA). IEEE, 11\u201320."},{"doi-asserted-by":"publisher","key":"e_1_3_1_10_2","DOI":"10.1109\/VLSID57277.2023.00018"},{"key":"e_1_3_1_11_2","first-page":"189:1\u2013189:22","article-title":"A structured methodology for pattern based adaptive scheduling in embedded control","volume":"16","year":"2017","unstructured":"Sumana Ghosh, Souradeep Dutta, Soumyajit Dey, and Pallab Dasgupta. 2017. A structured methodology for pattern based adaptive scheduling in embedded control. ACM Transactions on Embedded Computing Systems 16, 5s (2017), 189:1\u2013189:22.","journal-title":"ACM Transactions on Embedded Computing Systems"},{"doi-asserted-by":"publisher","key":"e_1_3_1_12_2","DOI":"10.1049\/iet-cdt.2019.0030"},{"doi-asserted-by":"publisher","key":"e_1_3_1_13_2","DOI":"10.1145\/3372134"},{"key":"e_1_3_1_14_2","first-page":"306","volume-title":"Proceedings of the Real-Time and Embedded Technology and Applications Symposium (RTAS)","year":"2024","unstructured":"Robert Gifford, Felipe Galarza-Jimenez, Linh Thi Xuan_Phan, and Majid Zamani. 2024. Decntr: Optimizing safety and schedulability with multi-mode control and resource allocation co-design. In Proceedings of the Real-Time and Embedded Technology and Applications Symposium (RTAS). IEEE, 306\u2013319."},{"doi-asserted-by":"publisher","key":"e_1_3_1_15_2","DOI":"10.1145\/3356865"},{"doi-asserted-by":"publisher","key":"e_1_3_1_16_2","DOI":"10.1109\/TCAD.2022.3198905"},{"doi-asserted-by":"publisher","key":"e_1_3_1_17_2","DOI":"10.1049\/iet-cta.2016.0871"},{"volume-title":"Proceedings of the Euromicro Conference on Real-Time Systems (ECRTS)","year":"2020","unstructured":"Martina Maggio, Arne Hamann, Eckart Mayer-John, and Dirk Ziegenbein. 2020. Control-system stability under consecutive deadline misses constraints. In Proceedings of the Euromicro Conference on Real-Time Systems (ECRTS). Schloss-Dagstuhl-Leibniz Zentrum f\u00fcr Informatik.","key":"e_1_3_1_18_2"},{"doi-asserted-by":"publisher","key":"e_1_3_1_19_2","DOI":"10.1007\/978-3-540-78800-3_24"},{"doi-asserted-by":"publisher","key":"e_1_3_1_20_2","DOI":"10.1145\/3126497"},{"doi-asserted-by":"publisher","key":"e_1_3_1_21_2","DOI":"10.1109\/LCSYS.2022.3179960"},{"issue":"1","key":"e_1_3_1_22_2","first-page":"112","article-title":"An improved smt-based scheduling for overloaded real-time systems","volume":"28","year":"2020","unstructured":"Shimin Wang, Xiaojuan Liao, Min Wang, Luyue Chang, Huan Yang, and Tao Wang. 2020. An improved smt-based scheduling for overloaded real-time systems. Engineering Letters 28, 1 (2020), 112\u2013122.","journal-title":"Engineering Letters"},{"doi-asserted-by":"publisher","key":"e_1_3_1_23_2","DOI":"10.1109\/TCAD.2021.3068940"},{"key":"e_1_3_1_24_2","first-page":"46","volume-title":"Proceedings of the Asia and South Pacific Design Automation Conference (ASP-DAC)","year":"2023","unstructured":"Shengjie Xu, Bineet Ghosh, Clara Hobbs, P. S. Thiagarajan, and Samarjit Chakraborty. 2023. Safety-aware flexible schedule synthesis for cyber-physical systems using weakly-hard constraints. In Proceedings of the Asia and South Pacific Design Automation Conference (ASP-DAC). 46\u201351."},{"key":"e_1_3_1_25_2","first-page":"196","volume-title":"Proceedings of the Embedded and Real-Time Computing Systems and Applications (RTCSA)","year":"2023","unstructured":"Shengjie Xu, Bineet Ghosh, Clara Hobbs, P. S. Thiagarajan, Prachi Joshi, and Samarjit Chakraborty. 2023. Safety-aware implementation of control tasks via scheduling with period boosting and compressing. In Proceedings of the Embedded and Real-Time Computing Systems and Applications (RTCSA). IEEE, 196\u2013205."},{"key":"e_1_3_1_26_2","first-page":"312","volume-title":"Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA)","year":"2023","unstructured":"Shengjie Xu, Bineet Ghosh, Clara Hobbs, Enrico Fraccaroli, Parasara Sridhar Duggirala, and Samarjit Chakraborty. 2023. Statistical approach to efficient and deterministic schedule synthesis for cyber-physical systems. In Proceedings of the International Symposium on Automated Technology for Verification and Analysis (ATVA). Springer, 312\u2013333."},{"doi-asserted-by":"publisher","key":"e_1_3_1_27_2","DOI":"10.1109\/VLSID60093.2024.00052"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3760528","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T18:18:46Z","timestamp":1762280326000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3760528"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,26]]},"references-count":26,"journal-issue":{"issue":"5s","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3760528"],"URL":"https:\/\/doi.org\/10.1145\/3760528","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2025,9,26]]},"assertion":[{"value":"2025-07-30","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-03","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}