{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:26:28Z","timestamp":1750220788859,"version":"3.41.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2020,5,18]],"date-time":"2020-05-18T00:00:00Z","timestamp":1589760000000},"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. Embed. Comput. Syst."],"published-print":{"date-parts":[[2020,5,31]]},"abstract":"<jats:p>Given the widespread deployment of cyber-physical systems and their safety-critical nature, reliability and security guarantees offered by such systems are of paramount importance. While the security of such systems against sensor attacks have garnered significant attention from researchers in recent times, improving the reliability of a control software implementation against transient environmental disturbances need to be investigated further. Scalable formal methods for verification of actual control performance guarantee offered by software implementations of control laws in the face of sensory faults have been explored in recent work [20]. However, the formal verification of the improvement of system reliability by incorporating sensor fault mitigation techniques like Kalman filtering [29] and sensor fusion [18, 52] remains to be explored. Moreover, system designers face complex tradeoff choices for deciding upon the usage of fault and attack mitigation techniques and scheduling them on available system resources as they incur extra computation load.<\/jats:p>\n          <jats:p>In the present work, our contributions are threefold. We formally analyze the actual performance guarantee of control software implementations enabled with additional fault mitigation techniques. We consider task-level models of such implementations enabled with security and fault tolerance primitives and construct a timed automata-based model which checks for schedulability on heterogeneous multi-core platforms. We leverage these methodologies in the context of a novel Design-Space-Exploration (DSE) framework that considers target reliability and security guarantees for a control system and computes schedulable design options while considering well-known platform-level security improvement and fault mitigation techniques. We validate our contributions over several case studies from the automotive domain.<\/jats:p>","DOI":"10.1145\/3387927","type":"journal-article","created":{"date-parts":[[2020,5,25]],"date-time":"2020-05-25T18:00:15Z","timestamp":1590429615000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Reliable and Secure Design-Space-Exploration for Cyber-Physical Systems"],"prefix":"10.1145","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9049-9455","authenticated-orcid":false,"given":"Saurav Kumar","family":"Ghosh","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Kharagpur, WB, India"}]},{"given":"Jaffer Sheriff","family":"R C","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur, WB, India"}]},{"given":"Vibhor","family":"Jain","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur, WB, India"}]},{"given":"Soumyajit","family":"Dey","sequence":"additional","affiliation":[{"name":"Indian Institute of Technology Kharagpur, WB, India"}]}],"member":"320","published-online":{"date-parts":[[2020,5,18]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.018"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"volume-title":"Principles of Model Checking","author":"Baier Christel","key":"e_1_2_1_3_1","unstructured":"Christel Baier , Joost-Pieter Katoen , and Kim Guldstrand Larsen . 2008. Principles of Model Checking . MIT Press , New York, NY . Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. 2008. Principles of Model Checking. MIT Press, New York, NY."},{"key":"e_1_2_1_4_1","volume-title":"John Hakansson, Paul Petterson, Wang Yi, and Martijn Hendriks.","author":"Behrmann Gerd","year":"2006","unstructured":"Gerd Behrmann , Alexandre David , Kim Guldstrand Larsen , John Hakansson, Paul Petterson, Wang Yi, and Martijn Hendriks. 2006 . UPPAAL 4.0. In QEST. IEEE Computer Society , Washington, DC, 125--126. Gerd Behrmann, Alexandre David, Kim Guldstrand Larsen, John Hakansson, Paul Petterson, Wang Yi, and Martijn Hendriks. 2006. UPPAAL 4.0. In QEST. IEEE Computer Society, Washington, DC, 125--126."},{"key":"e_1_2_1_5_1","volume-title":"International Hybrid Systems Workshop. Springer","author":"Bengtsson Johan","year":"1995","unstructured":"Johan Bengtsson , Kim Larsen , Fredrik Larsson , Paul Pettersson , and Wang Yi . 1995 . UPPAAL\u2014A tool suite for automatic verification of real-time systems . In International Hybrid Systems Workshop. Springer , Berlin, 232--243. Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. 1995. UPPAAL\u2014A tool suite for automatic verification of real-time systems. In International Hybrid Systems Workshop. Springer, Berlin, 232--243."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2012.226"},{"key":"e_1_2_1_7_1","unstructured":"Alvaro Cardenas Saurabh Amin Bruno Sinopoli Annarita Giani Adrian Perrig and Shankar Sastry. 2009. Challenges for Securing Cyber Physical Systems. DHS.  Alvaro Cardenas Saurabh Amin Bruno Sinopoli Annarita Giani Adrian Perrig and Shankar Sastry. 2009. Challenges for Securing Cyber Physical Systems. DHS."},{"key":"e_1_2_1_8_1","volume-title":"USENIX Conference on Security","volume":"4","author":"Checkoway Stephen","year":"2011","unstructured":"Stephen Checkoway , Damon McCoy , Brian Kantor , Danny Anderson , Hovav Shacham , Stefan Savage , Karl Koscher , Alexei Czeskis , Franziska Roesner , Tadayoshi Kohno , et\u00a0al. 2011 . Comprehensive experimental analyses of automotive attack surfaces . In USENIX Conference on Security , Vol. 4 . USENIX Association, San Francisco, CA, 447--462. Stephen Checkoway, Damon McCoy, Brian Kantor, Danny Anderson, Hovav Shacham, Stefan Savage, Karl Koscher, Alexei Czeskis, Franziska Roesner, Tadayoshi Kohno, et\u00a0al. 2011. Comprehensive experimental analyses of automotive attack surfaces. In USENIX Conference on Security, Vol. 4. USENIX Association, San Francisco, CA, 447--462."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2013.02.014"},{"key":"e_1_2_1_10_1","volume-title":"Junkins","author":"Crassidis John L.","year":"2011","unstructured":"John L. Crassidis and John L . Junkins . 2011 . Optimal Estimation of Dynamic Systems. CRC Press , Boca Raton, FL. John L. Crassidis and John L. Junkins. 2011. Optimal Estimation of Dynamic Systems. CRC Press, Boca Raton, FL."},{"volume-title":"Software Engineering and Formal Methods","author":"Cuoq Pascal","key":"e_1_2_1_11_1","unstructured":"Pascal Cuoq , Florent Kirchner , Nikolai Kosmatov , Virgile Prevosto , Julien Signoles , and Boris Yakobowski . 2012. Frama-c . In Software Engineering and Formal Methods . Springer , Berlin , 233--247. Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. 2012. Frama-c. In Software Engineering and Formal Methods. Springer, Berlin, 233--247."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2003.04.003"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2009.2039550"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2014.12.004"},{"volume-title":"Scheduling a steel plant with timed automata","author":"Fehnker Ansgar","key":"e_1_2_1_16_1","unstructured":"Ansgar Fehnker . 1999. Scheduling a steel plant with timed automata . In RTCSA. IEEE , New York, NY , 280--286. Ansgar Fehnker. 1999. Scheduling a steel plant with timed automata. In RTCSA. IEEE, New York, NY, 280--286."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.019"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/7.913685"},{"volume-title":"Design and validation of fault-tolerant embedded controllers","author":"Ghosh Saurav Kumar","key":"e_1_2_1_19_1","unstructured":"Saurav Kumar Ghosh , Soumyajjit Dey , Dip Goswami , Daniel Mueller-Gritschneder , and Samarjit Chakraborty . 2018. Design and validation of fault-tolerant embedded controllers . In DATE. IEEE , New York, NY , 1283--1288. Saurav Kumar Ghosh, Soumyajjit Dey, Dip Goswami, Daniel Mueller-Gritschneder, and Samarjit Chakraborty. 2018. Design and validation of fault-tolerant embedded controllers. In DATE. IEEE, New York, NY, 1283--1288."},{"key":"e_1_2_1_20_1","volume-title":"Work-in-progress: Verifying stability guarantees of control software implementations in the presence of sensor level faults","author":"Ghosh Saurav Kumar","year":"2017","unstructured":"Saurav Kumar Ghosh , Debasmita Lohar , Dibyendu Das , and Soumyajit Dey . 2017 . Work-in-progress: Verifying stability guarantees of control software implementations in the presence of sensor level faults . In EMSOFT. IEEE , New York, NY , 1--2. Saurav Kumar Ghosh, Debasmita Lohar, Dibyendu Das, and Soumyajit Dey. 2017. Work-in-progress: Verifying stability guarantees of control software implementations in the presence of sensor level faults. In EMSOFT. IEEE, New York, NY, 1--2."},{"volume-title":"Fault-tolerant embedded control systems for unreliable hardware","author":"Goswami Dip","key":"e_1_2_1_21_1","unstructured":"Dip Goswami , D. Muller-Gritschneder , Twan Basten , Ulf Schlichtmann , and Samarjit Chakraborty . 2014. Fault-tolerant embedded control systems for unreliable hardware . In ISIC. IEEE , New York, NY , 464--467. Dip Goswami, D. Muller-Gritschneder, Twan Basten, Ulf Schlichtmann, and Samarjit Chakraborty. 2014. Fault-tolerant embedded control systems for unreliable hardware. In ISIC. IEEE, New York, NY, 464--467."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2014.2301795"},{"key":"e_1_2_1_23_1","first-page":"21","article-title":"Hackers remotely kill a jeep on the highway\u2014with me in it","volume":"7","author":"Greenberg Andy","year":"2015","unstructured":"Andy Greenberg . 2015 . Hackers remotely kill a jeep on the highway\u2014with me in it . Wired 7 (2015), 21 . Andy Greenberg. 2015. Hackers remotely kill a jeep on the highway\u2014with me in it. Wired 7 (2015), 21.","journal-title":"Wired"},{"volume-title":"IFIP WG 10.2 International Workshop","author":"Guan Nan","key":"e_1_2_1_24_1","unstructured":"Nan Guan , Zonghua Gu , Qingxu Deng , Shuaihong Gao , and Ge Yu. 2007. Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking . In IFIP WG 10.2 International Workshop , SEUS. Springer , Berlin , 263--272. Nan Guan, Zonghua Gu, Qingxu Deng, Shuaihong Gao, and Ge Yu. 2007. Exact schedulability analysis for static-priority global multiprocessor scheduling using model-checking. In IFIP WG 10.2 International Workshop, SEUS. Springer, Berlin, 263--272."},{"volume-title":"Deadline analysis of AUTOSAR OS periodic tasks in the presence of interrupts","author":"Huang Yanhong","key":"e_1_2_1_25_1","unstructured":"Yanhong Huang , Joao F. Ferreira , Guanhua He , Shengchao Qin , and Jifeng He. 2013. Deadline analysis of AUTOSAR OS periodic tasks in the presence of interrupts . In ICFEM. Springer , Berlin , 165--181. Yanhong Huang, Joao F. Ferreira, Guanhua He, Shengchao Qin, and Jifeng He. 2013. Deadline analysis of AUTOSAR OS periodic tasks in the presence of interrupts. In ICFEM. Springer, Berlin, 165--181."},{"key":"e_1_2_1_26_1","volume-title":"Huss","author":"Jhumka Arshad","year":"2005","unstructured":"Arshad Jhumka , Stephan Klaus , and Sorin A . Huss . 2005 . A dependability-driven system-level design approach for embedded systems. In DATE. IEEE, New York, NY , 372--377. Arshad Jhumka, Stephan Klaus, and Sorin A. Huss. 2005. A dependability-driven system-level design approach for embedded systems. In DATE. IEEE, New York, NY, 372--377."},{"volume-title":"RTNS","author":"Jiang Ke","key":"e_1_2_1_27_1","unstructured":"Ke Jiang , Adrian Lifa , Petru Eles , Zebo Peng , and Wei Jiang . 2013. Energy-aware design of secure multi-mode real-time embedded systems with FPGA co-processors . In RTNS . ACM , New York, NY , 109--118. Ke Jiang, Adrian Lifa, Petru Eles, Zebo Peng, and Wei Jiang. 2013. Energy-aware design of secure multi-mode real-time embedded systems with FPGA co-processors. In RTNS. ACM, New York, NY, 109--118."},{"volume-title":"Sporadic data integrity for secure state estimation","author":"Jovanov Ilija","key":"e_1_2_1_28_1","unstructured":"Ilija Jovanov and Miroslav Pajic . 2017. Sporadic data integrity for secure state estimation . In CDC. IEEE , New York, NY , 163--169. Ilija Jovanov and Miroslav Pajic. 2017. Sporadic data integrity for secure state estimation. In CDC. IEEE, New York, NY, 163--169."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1115\/1.3662552"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1002\/rob.21513"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.34"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2011.67"},{"volume-title":"Network scheduling for secure cyber-physical systems","author":"Lesi Vuk","key":"e_1_2_1_33_1","unstructured":"Vuk Lesi , Ilija Jovanov , and Miroslav Pajic . 2017. Network scheduling for secure cyber-physical systems . In RTSS. IEEE , New York, NY , 45--55. Vuk Lesi, Ilija Jovanov, and Miroslav Pajic. 2017. Network scheduling for secure cyber-physical systems. In RTSS. IEEE, New York, NY, 45--55."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126518"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2803174"},{"key":"e_1_2_1_37_1","volume-title":"Retrieved on","author":"MDA.","year":"2020","unstructured":"MDA. 2020 . Measure Data Analyzer . Retrieved on September 10, 2019 from https:\/\/www.etas.com\/en\/products\/mda.php. MDA. 2020. Measure Data Analyzer. Retrieved on September 10, 2019 from https:\/\/www.etas.com\/en\/products\/mda.php."},{"key":"e_1_2_1_38_1","unstructured":"William C. Messner Dawn M. Tilbury and Rick Hill. 1999. Control Tutorials for MATLAB\u00ae and Simulink\u00ae.  William C. Messner Dawn M. Tilbury and Rick Hill. 1999. Control Tutorials for MATLAB\u00ae and Simulink\u00ae."},{"volume-title":"Allerton","author":"Mo Yilin","key":"e_1_2_1_39_1","unstructured":"Yilin Mo and Bruno Sinopoli . 2009. Secure control against replay attacks . In Allerton . IEEE , New York, NY , 911--918. Yilin Mo and Bruno Sinopoli. 2009. Secure control against replay attacks. In Allerton. IEEE, New York, NY, 911--918."},{"key":"e_1_2_1_40_1","volume-title":"Preprints of the First Workshop on Secure Control Systems. ACM","author":"Mo Yilin","year":"2010","unstructured":"Yilin Mo and Bruno Sinopoli . 2010 . False data injection attacks in cyber physical systems . In Preprints of the First Workshop on Secure Control Systems. ACM , New York, NY, 1--6. Yilin Mo and Bruno Sinopoli. 2010. False data injection attacks in cyber physical systems. In Preprints of the First Workshop on Secure Control Systems. ACM, New York, NY, 1--6."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.637146"},{"volume-title":"ICCPS","author":"Park Junkil","key":"e_1_2_1_42_1","unstructured":"Junkil Park , Radoslav Ivanov , James Weimer , Miroslav Pajic , and Insup Lee . 2015. Sensor attack detection in the presence of transient faults . In ICCPS . ACM , New York, NY , 1--10. Junkil Park, Radoslav Ivanov, James Weimer, Miroslav Pajic, and Insup Lee. 2015. Sensor attack detection in the presence of transient faults. In ICCPS. ACM, New York, NY, 1--10."},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2014.2364725"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/LES.2014.2367100"},{"volume-title":"Non-invasive spoofing attacks for anti-lock braking systems","author":"Shoukry Yasser","key":"e_1_2_1_45_1","unstructured":"Yasser Shoukry , Paul Martin , Paulo Tabuada , and Mani Srivastava . 2013. Non-invasive spoofing attacks for anti-lock braking systems . In CHES. Springer , Berlin , 55--72. Yasser Shoukry, Paul Martin, Paulo Tabuada, and Mani Srivastava. 2013. Non-invasive spoofing attacks for anti-lock braking systems. In CHES. Springer, Berlin, 55--72."},{"volume-title":"IFIP WG 11.10 International Conference","author":"Slay Jill","key":"e_1_2_1_46_1","unstructured":"Jill Slay and Michael Miller . 2007. Lessons learned from the maroochy water breach . In IFIP WG 11.10 International Conference , CIP. Springer , Berlin , 73--82. Jill Slay and Michael Miller. 2007. Lessons learned from the maroochy water breach. In IFIP WG 11.10 International Conference, CIP. Springer, Berlin, 73--82."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2007.03.019"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2014.10.067"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2000.858698"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2013.23"},{"key":"e_1_2_1_51_1","volume-title":"International Journal of Simulation--Systems, Science 8 Technology 11, 5","author":"Wei Tan Chee","year":"2010","unstructured":"Tan Chee Wei , Hazlina Selamat , and Ahmad Jais Alimin . 2010. Modeling and control of an engine fuel injection system . International Journal of Simulation--Systems, Science 8 Technology 11, 5 ( 2010 ), 48--60. Tan Chee Wei, Hazlina Selamat, and Ahmad Jais Alimin. 2010. Modeling and control of an engine fuel injection system. International Journal of Simulation--Systems, Science 8 Technology 11, 5 (2010), 48--60."},{"volume-title":"A scheme for robust distributed sensor fusion based on average consensus","author":"Xiao Lin","key":"e_1_2_1_52_1","unstructured":"Lin Xiao , Stephen Boyd , and Sanjay Lall . 2005. A scheme for robust distributed sensor fusion based on average consensus . In IPSN. IEEE , New York, NY , 63--70. Lin Xiao, Stephen Boyd, and Sanjay Lall. 2005. A scheme for robust distributed sensor fusion based on average consensus. In IPSN. IEEE, New York, NY, 63--70."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2016.2523937"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387927","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3387927","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:42Z","timestamp":1750200102000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3387927"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,5,18]]},"references-count":52,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,5,31]]}},"alternative-id":["10.1145\/3387927"],"URL":"https:\/\/doi.org\/10.1145\/3387927","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2020,5,18]]},"assertion":[{"value":"2019-05-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-05-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}