{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:59:08Z","timestamp":1776333548853,"version":"3.51.2"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2017,12,12]],"date-time":"2017-12-12T00:00:00Z","timestamp":1513036800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF CNS","award":["1116136 and 1350420"],"award-info":[{"award-number":["1116136 and 1350420"]}]},{"name":"NSF I\/UCRC Center for Embedded Systems"},{"DOI":"10.13039\/100000151","name":"NSF IIP","doi-asserted-by":"crossref","award":["1361926"],"award-info":[{"award-number":["1361926"]}],"id":[{"id":"10.13039\/100000151","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2018,3,31]]},"abstract":"<jats:p>A framework for the elicitation and debugging of formal specifications for Cyber-Physical Systems is presented. The elicitation of specifications is handled through a graphical interface. Two debugging algorithms are presented. The first checks for erroneous or incomplete temporal logic specifications without considering the system. The second can be utilized for the analysis of reactive requirements with respect to system test traces. The specification debugging framework is applied on a number of formal specifications collected through a user study. The user study establishes that requirement errors are common and that the debugging framework can resolve many insidious specification errors.<\/jats:p>","DOI":"10.1145\/3147451","type":"journal-article","created":{"date-parts":[[2017,12,13]],"date-time":"2017-12-13T14:50:37Z","timestamp":1513176637000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Formal Requirement Debugging for Testing and Verification of Cyber-Physical Systems"],"prefix":"10.1145","volume":"17","author":[{"given":"Adel","family":"Dokhanchi","sequence":"first","affiliation":[{"name":"Arizona State University, Tempe, AZ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bardh","family":"Hoxha","sequence":"additional","affiliation":[{"name":"Southern Illinois University, Carbondale, IL, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georgios","family":"Fainekos","sequence":"additional","affiliation":[{"name":"Arizona State University, Tempe, AZ, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,12]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2465787.2465797"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/227595.227602"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781152"},{"key":"e_1_2_1_5_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (LNCS)","author":"Rahul Annapureddy Yashwanth Singh","unstructured":"Yashwanth Singh Rahul Annapureddy , Che Liu , Georgios E. Fainekos , and Sriram Sankaranarayanan . 2011. S-TaLiRo: A tool for temporal logic falsification for hybrid systems . In Tools and Algorithms for the Construction and Analysis of Systems (LNCS) , Vol. 6605 . Springer , 254--257. Yashwanth Singh Rahul Annapureddy, Che Liu, Georgios E. Fainekos, and Sriram Sankaranarayanan. 2011. S-TaLiRo: A tool for temporal logic falsification for hybrid systems. In Tools and Algorithms for the Construction and Analysis of Systems (LNCS), Vol. 6605. Springer, 254--257."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-007-0012-6"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792786.1792789"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/196244.196575"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008779610539"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0221-0"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44522-8_7"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-015-0229-y"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.119.8"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0060-y"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787526.1787535"},{"key":"e_1_2_1_16_1","volume-title":"Peled","author":"Clarke Edmund M.","year":"1999","unstructured":"Edmund M. Clarke , Orna Grumberg , and Doron A . Peled . 1999 . Model Checking. MIT Press , Cambridge, MA. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.09.006"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2015.7340472"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/COASE.2017.8256286"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/298595.298598"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.157.12"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2012.6315384"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2011.5979895"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01702-5_7"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2944225.2944368"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita\/2015005"},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of Applied Verification for Continuous and Hybrid Systems.","author":"Hoxha Bardh","year":"2014","unstructured":"Bardh Hoxha , Houssam Abbas , and Georgios Fainekos . 2014 a. Benchmarks for temporal logic requirements for automotive systems . In Proceedings of Applied Verification for Continuous and Hybrid Systems. Bardh Hoxha, Houssam Abbas, and Georgios Fainekos. 2014a. Benchmarks for temporal logic requirements for automotive systems. In Proceedings of Applied Verification for Continuous and Hybrid Systems."},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the International Workshop on Design and Implementation of Formal Tools and Systems.","author":"Hoxha Bardh","year":"2014","unstructured":"Bardh Hoxha , Hoang Bach , Houssam Abbas , Adel Dokhanchi , Yoshihiro Kobayashi , and Georgios Fainekos . 2014 b. Towards formal specification visualization for testing and monitoring of cyber-physical systems . In Proceedings of the International Workshop on Design and Implementation of Formal Tools and Systems. Bardh Hoxha, Hoang Bach, Houssam Abbas, Adel Dokhanchi, Yoshihiro Kobayashi, and Georgios Fainekos. 2014b. Towards formal specification visualization for testing and monitoring of cyber-physical systems. In Proceedings of the International Workshop on Design and Implementation of Formal Tools and Systems."},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the IEEE\/RSJ International Conference on Intelligent Robots and Systems.","author":"Hoxha Bardh","year":"2015","unstructured":"Bardh Hoxha , Nikolaos Mavridis , and Georgios Fainekos . 2015 . ViSpec: A graphical tool for easy elicitation of MTL requirements . In Proceedings of the IEEE\/RSJ International Conference on Intelligent Robots and Systems. Bardh Hoxha, Nikolaos Mavridis, and Georgios Fainekos. 2015. ViSpec: A graphical tool for easy elicitation of MTL requirements. In Proceedings of the IEEE\/RSJ International Conference on Intelligent Robots and Systems."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461337"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the American Control Conference (ACC\u201915)","author":"Kapinski James","unstructured":"James Kapinski , Jyotirmoy V. Deshmukh , Xiaoqing Jin , Hisahiro Ito , and Kenneth R. Butts . 2015. Simulation-guided approaches for verification of automotive powertrain control systems . In Proceedings of the American Control Conference (ACC\u201915) . 4086--4095. James Kapinski, Jyotirmoy V. Deshmukh, Xiaoqing Jin, Hisahiro Ito, and Kenneth R. Butts. 2015. Simulation-guided approaches for verification of automotive powertrain control systems. In Proceedings of the American Control Conference (ACC\u201915). 4086--4095."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICRA.2012.6224826"},{"key":"e_1_2_1_34_1","first-page":"5","article-title":"Debugging formal specifications: A practical approach using model-based diagnosis and counterstrategies","volume":"15","author":"K\u00f6nighofer Robert","year":"2013","unstructured":"Robert K\u00f6nighofer , Georg Hofferek , and Roderick Bloem . 2013 . Debugging formal specifications: A practical approach using model-based diagnosis and counterstrategies . Journal on Software Tools for Technology Transfer 15 , 5 -- 6 (2013), 563--583. Robert K\u00f6nighofer, Georg Hofferek, and Roderick Bloem. 2013. Debugging formal specifications: A practical approach using model-based diagnosis and counterstrategies. Journal on Software Tools for Technology Transfer 15, 5--6 (2013), 563--583.","journal-title":"Journal on Software Tools for Technology Transfer"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062526"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01995674"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090100062"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2013.19"},{"key":"e_1_2_1_39_1","first-page":"152","article-title":"Monitoring temporal properties of continuous signals","volume":"3253","author":"Maler Oded","year":"2004","unstructured":"Oded Maler and Dejan Nickovic . 2004 . Monitoring temporal properties of continuous signals . In Proceedings of FORMATS-FTRTFT (LNCS) , Vol. 3253. 152 -- 166 . Oded Maler and Dejan Nickovic. 2004. Monitoring temporal properties of continuous signals. In Proceedings of FORMATS-FTRTFT (LNCS), Vol. 3253. 152--166.","journal-title":"Proceedings of FORMATS-FTRTFT (LNCS)"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0082-7"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2011.6051657"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032359"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220920.3221237"},{"key":"e_1_2_1_44_1","volume-title":"Testing Software and Systems","author":"Yang Hengyi","unstructured":"Hengyi Yang , Bardh Hoxha , and Georgios Fainekos . 2012. Querying parametric temporal logic properties on embedded systems . In Testing Software and Systems . Springer , 136--151. Hengyi Yang, Bardh Hoxha, and Georgios Fainekos. 2012. Querying parametric temporal logic properties on embedded systems. In Testing Software and Systems. Springer, 136--151."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2009.09.013"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3147451","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3147451","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:16Z","timestamp":1750212676000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3147451"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,12]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3,31]]}},"alternative-id":["10.1145\/3147451"],"URL":"https:\/\/doi.org\/10.1145\/3147451","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,12]]},"assertion":[{"value":"2016-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-12-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}