{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:24:33Z","timestamp":1750220673900,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,4,7]],"date-time":"2021-04-07T00:00:00Z","timestamp":1617753600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"United States Air Force","award":["FA8702-15-D-0002"],"award-info":[{"award-number":["FA8702-15-D-0002"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,4,7]]},"DOI":"10.1145\/3453417.3453431","type":"proceedings-article","created":{"date-parts":[[2021,7,22]],"date-time":"2021-07-22T22:18:55Z","timestamp":1626992335000},"page":"57-67","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of a Mixed-Trust Synchronization Protocol"],"prefix":"10.1145","author":[{"given":"Ruben","family":"Martins","sequence":"first","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"McCall","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dionisio","family":"de Niz","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amit","family":"Vasudevan","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bjorn","family":"Andersson","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Klein","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John P.","family":"Lehoczky","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hyoseung","family":"Kim","sequence":"additional","affiliation":[{"name":"UC Riverside, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,7,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.11.018"},{"volume-title":"ICALP(Lecture Notes in Computer Science, Vol.\u00a0443)","author":"Alur Rajeev","key":"e_1_3_2_1_2_1","unstructured":"Rajeev Alur and David\u00a0 L. Dill . 1990. Automata For Modeling Real-Time Systems . In ICALP(Lecture Notes in Computer Science, Vol.\u00a0443) . Springer , 322\u2013335. Rajeev Alur and David\u00a0L. Dill. 1990. Automata For Modeling Real-Time Systems. In ICALP(Lecture Notes in Computer Science, Vol.\u00a0443). Springer, 322\u2013335."},{"volume-title":"RV(Lecture Notes in Computer Science, Vol.\u00a010548)","author":"Andersson Bj\u00f6rn","key":"e_1_3_2_1_3_1","unstructured":"Bj\u00f6rn Andersson , Sagar Chaki , and Dionisio de Niz . 2017. Combining Symbolic Runtime Enforcers for Cyber-Physical Systems . In RV(Lecture Notes in Computer Science, Vol.\u00a010548) . Springer , 68\u201384. Bj\u00f6rn Andersson, Sagar Chaki, and Dionisio de Niz. 2017. Combining Symbolic Runtime Enforcers for Cyber-Physical Systems. In RV(Lecture Notes in Computer Science, Vol.\u00a010548). Springer, 68\u201384."},{"volume-title":"FORMATS(Lecture Notes in Computer Science, Vol.\u00a08711)","author":"Andrychowicz Marcin","key":"e_1_3_2_1_4_1","unstructured":"Marcin Andrychowicz , Stefan Dziembowski , Daniel Malinowski , and Lukasz Mazurek . 2014. Modeling Bitcoin Contracts by Timed Automata . In FORMATS(Lecture Notes in Computer Science, Vol.\u00a08711) . Springer , 7\u201322. Marcin Andrychowicz, Stefan Dziembowski, Daniel Malinowski, and Lukasz Mazurek. 2014. Modeling Bitcoin Contracts by Timed Automata. In FORMATS(Lecture Notes in Computer Science, Vol.\u00a08711). Springer, 7\u201322."},{"volume-title":"SFM(Lecture Notes in Computer Science, Vol.\u00a03185)","author":"Behrmann Gerd","key":"e_1_3_2_1_5_1","unstructured":"Gerd Behrmann , Alexandre David , and Kim\u00a0Guldstrand Larsen . 2004. A Tutorial on Uppaal . In SFM(Lecture Notes in Computer Science, Vol.\u00a03185) . Springer , 200\u2013236. Gerd Behrmann, Alexandre David, and Kim\u00a0Guldstrand Larsen. 2004. A Tutorial on Uppaal. In SFM(Lecture Notes in Computer Science, Vol.\u00a03185). Springer, 200\u2013236."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.75415"},{"volume-title":"RV(Lecture Notes in Computer Science, Vol.\u00a011237)","author":"Bouyer Patricia","key":"e_1_3_2_1_7_1","unstructured":"Patricia Bouyer , Samy Jaziri , and Nicolas Markey . 2018. Efficient Timed Diagnosis Using Automata with Timed Domains . In RV(Lecture Notes in Computer Science, Vol.\u00a011237) . Springer , 205\u2013221. Patricia Bouyer, Samy Jaziri, and Nicolas Markey. 2018. Efficient Timed Diagnosis Using Automata with Timed Domains. In RV(Lecture Notes in Computer Science, Vol.\u00a011237). Springer, 205\u2013221."},{"volume-title":"Models, Algorithms, Logics and Tools(Lecture Notes in Computer Science, Vol.\u00a010460)","author":"Bouyer Patricia","key":"e_1_3_2_1_8_1","unstructured":"Patricia Bouyer , Fran\u00e7ois Laroussinie , Nicolas Markey , Jo\u00ebl Ouaknine , and James Worrell . 2017. Timed Temporal Logics . In Models, Algorithms, Logics and Tools(Lecture Notes in Computer Science, Vol.\u00a010460) . Springer , 211\u2013230. Patricia Bouyer, Fran\u00e7ois Laroussinie, Nicolas Markey, Jo\u00ebl Ouaknine, and James Worrell. 2017. Timed Temporal Logics. In Models, Algorithms, Logics and Tools(Lecture Notes in Computer Science, Vol.\u00a010460). Springer, 211\u2013230."},{"key":"e_1_3_2_1_9_1","volume-title":"Kronos: A Model-Checking Tool for Real-Time Systems. In CAV(Lecture Notes in Computer Science, Vol.\u00a01427)","author":"Bozga Marius","year":"1998","unstructured":"Marius Bozga , Conrado Daws , Oded Maler , Alfredo Olivero , Stavros Tripakis , and Sergio Yovine . 1998 . Kronos: A Model-Checking Tool for Real-Time Systems. In CAV(Lecture Notes in Computer Science, Vol.\u00a01427) . Springer , 546\u2013550. Marius Bozga, Conrado Daws, Oded Maler, Alfredo Olivero, Stavros Tripakis, and Sergio Yovine. 1998. Kronos: A Model-Checking Tool for Real-Time Systems. In CAV(Lecture Notes in Computer Science, Vol.\u00a01427). Springer, 546\u2013550."},{"key":"e_1_3_2_1_10_1","volume-title":"A Survey of Research into Mixed Criticality Systems. ACM Comput. Surv. 50, 6","author":"Burns Alan","year":"2018","unstructured":"Alan Burns and Robert\u00a0 I. Davis . 2018. A Survey of Research into Mixed Criticality Systems. ACM Comput. Surv. 50, 6 ( 2018 ), 82:1\u201382:37. Alan Burns and Robert\u00a0I. Davis. 2018. A Survey of Research into Mixed Criticality Systems. ACM Comput. Surv. 50, 6 (2018), 82:1\u201382:37."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.07.011"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2005.12.021"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3126517"},{"volume-title":"CAV(Lecture Notes in Computer Science, Vol.\u00a011561)","author":"Cimatti Alessandro","key":"e_1_3_2_1_14_1","unstructured":"Alessandro Cimatti , Alberto Griggio , Enrico Magnago , Marco Roveri , and Stefano Tonetta . 2019. Extending nuXmv with Timed Transition Systems and Timed Temporal Properties . In CAV(Lecture Notes in Computer Science, Vol.\u00a011561) . Springer , 376\u2013386. Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, and Stefano Tonetta. 2019. Extending nuXmv with Timed Transition Systems and Timed Temporal Properties. In CAV(Lecture Notes in Computer Science, Vol.\u00a011561). Springer, 376\u2013386."},{"key":"e_1_3_2_1_15_1","volume-title":"Work-in-Progress: Toward Precomputation in Real-Time Mixed-Trust Scheduling. In Brief Presentation Session of IEEE Real-Time Systems Symposium (RTSS). IEEE.","author":"de Niz Dionisio","year":"2020","unstructured":"Dionisio de Niz , Bj\u00f6rn Andersson , Hyoseung Kim , Mark\u00a0 H. Klein , and John\u00a0 P. Lehoczky . 2020 . Work-in-Progress: Toward Precomputation in Real-Time Mixed-Trust Scheduling. In Brief Presentation Session of IEEE Real-Time Systems Symposium (RTSS). IEEE. Dionisio de Niz, Bj\u00f6rn Andersson, Hyoseung Kim, Mark\u00a0H. Klein, and John\u00a0P. Lehoczky. 2020. Work-in-Progress: Toward Precomputation in Real-Time Mixed-Trust Scheduling. In Brief Presentation Session of IEEE Real-Time Systems Symposium (RTSS). IEEE."},{"volume-title":"Mixed-Trust Computing for Real-Time Systems","author":"de Niz Dionisio","key":"e_1_3_2_1_16_1","unstructured":"Dionisio de Niz , Bj\u00f6rn Andersson , Mark\u00a0 H. Klein , John\u00a0 P. Lehoczky , A. Vasudevan , Hyoseung Kim , and Gabriel\u00a0 A. Moreno . 2019. Mixed-Trust Computing for Real-Time Systems . In RTCSA. IEEE , 1\u201311. Dionisio de Niz, Bj\u00f6rn Andersson, Mark\u00a0H. Klein, John\u00a0P. Lehoczky, A. Vasudevan, Hyoseung Kim, and Gabriel\u00a0A. Moreno. 2019. Mixed-Trust Computing for Real-Time Systems. In RTCSA. IEEE, 1\u201311."},{"volume-title":"Autonomous Systems: Sensors, Vehicles, Security, and the Internet of Everything, Vol.\u00a010643","author":"de Niz Dionisio","key":"e_1_3_2_1_17_1","unstructured":"Dionisio de Niz , Bjorn Andersson , and Gabriel Moreno . 2018. Safety enforcement for the verification of autonomous systems . In Autonomous Systems: Sensors, Vehicles, Security, and the Internet of Everything, Vol.\u00a010643 . International Society for Optics and Photonics, SPIE , 1 \u2013 10. Dionisio de Niz, Bjorn Andersson, and Gabriel Moreno. 2018. Safety enforcement for the verification of autonomous systems. In Autonomous Systems: Sensors, Vehicles, Security, and the Internet of Everything, Vol.\u00a010643. International Society for Optics and Photonics, SPIE, 1 \u2013 10."},{"volume-title":"On the Scheduling of Mixed-Criticality Real-Time Task Sets","author":"de Niz Dionisio","key":"e_1_3_2_1_18_1","unstructured":"Dionisio de Niz , Karthik Lakshmanan , and Ragunathan Rajkumar . 2009. On the Scheduling of Mixed-Criticality Real-Time Task Sets . In RTSS. IEEE Computer Society , 291\u2013300. Dionisio de Niz, Karthik Lakshmanan, and Ragunathan Rajkumar. 2009. On the Scheduling of Mixed-Criticality Real-Time Task Sets. In RTSS. IEEE Computer Society, 291\u2013300."},{"volume-title":"Compositional Schedulability Analysis of Hierarchical Real-Time Systems","author":"Easwaran Arvind","key":"e_1_3_2_1_19_1","unstructured":"Arvind Easwaran , Insup Lee , Insik Shin , and Oleg Sokolsky . 2007. Compositional Schedulability Analysis of Hierarchical Real-Time Systems . In ISORC. IEEE Computer Society , 274\u2013281. Arvind Easwaran, Insup Lee, Insik Shin, and Oleg Sokolsky. 2007. Compositional Schedulability Analysis of Hierarchical Real-Time Systems. In ISORC. IEEE Computer Society, 274\u2013281."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Arvind Easwaran Insik Shin Oleg Sokolsky and Insup Lee. 2006. Incremental schedulability analysis of hierarchical real-time components. In EMSOFT. ACM 272\u2013281. Arvind Easwaran Insik Shin Oleg Sokolsky and Insup Lee. 2006. Incremental schedulability analysis of hierarchical real-time components. In EMSOFT. ACM 272\u2013281.","DOI":"10.1145\/1176887.1176927"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231869"},{"volume-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels","author":"Gu Ronghui","key":"e_1_3_2_1_22_1","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan\u00a0(Newman) Wu, Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In OSDI. USENIX Association , 653\u2013669. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan\u00a0(Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In OSDI. USENIX Association, 653\u2013669."},{"volume-title":"FM(Lecture Notes in Computer Science, Vol.\u00a05850)","author":"Heidarian Faranak","key":"e_1_3_2_1_23_1","unstructured":"Faranak Heidarian , Julien Schmaltz , and Frits\u00a0 W. Vaandrager . 2009. Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks . In FM(Lecture Notes in Computer Science, Vol.\u00a05850) . Springer , 516\u2013531. Faranak Heidarian, Julien Schmaltz, and Frits\u00a0W. Vaandrager. 2009. Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks. In FM(Lecture Notes in Computer Science, Vol.\u00a05850). Springer, 516\u2013531."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_3_2_1_25_1","first-page":"119","article-title":"Using integer clocks to verify clock-synchronization protocols","volume":"7","author":"Huang Xiaowan","year":"2011","unstructured":"Xiaowan Huang , Anu Singh , and Scott\u00a0 A. Smolka . 2011 . Using integer clocks to verify clock-synchronization protocols . ISSE 7 , 2 (2011), 119 \u2013 130 . Xiaowan Huang, Anu Singh, and Scott\u00a0A. Smolka. 2011. Using integer clocks to verify clock-synchronization protocols. ISSE 7, 2 (2011), 119\u2013130.","journal-title":"ISSE"},{"volume-title":"Mapping Temporal Planning Constraints into Timed Automata","author":"Khatib Lina","key":"e_1_3_2_1_26_1","unstructured":"Lina Khatib , Nicola Muscettola , and Klaus Havelund . 2001. Mapping Temporal Planning Constraints into Timed Automata . In TIME. IEEE Computer Society , 21\u201327. Lina Khatib, Nicola Muscettola, and Klaus Havelund. 2001. Mapping Temporal Planning Constraints into Timed Automata. In TIME. IEEE Computer Society, 21\u201327."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Gerwin Klein Kevin Elphinstone Gernot Heiser June Andronick David Cock Philip Derrin Dhammika Elkaduwe Kai Engelhardt Rafal Kolanski Michael Norrish Thomas Sewell Harvey Tuch and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In SOSP. ACM 207\u2013220. Gerwin Klein Kevin Elphinstone Gernot Heiser June Andronick David Cock Philip Derrin Dhammika Elkaduwe Kai Engelhardt Rafal Kolanski Michael Norrish Thomas Sewell Harvey Tuch and Simon Winwood. 2009. seL4: formal verification of an OS kernel. In SOSP. ACM 207\u2013220.","DOI":"10.1145\/1629575.1629596"},{"volume-title":"SSIRI (Companion)","author":"Koltuksuz Ahmet","key":"e_1_3_2_1_28_1","unstructured":"Ahmet Koltuksuz , Burcu Kulahcioglu , and Murat Ozkan . 2010. Utilization of Timed Automata as a Verification Tool for Security Protocols . In SSIRI (Companion) . IEEE Computer Society , 86\u201393. Ahmet Koltuksuz, Burcu Kulahcioglu, and Murat Ozkan. 2010. Utilization of Timed Automata as a Verification Tool for Security Protocols. In SSIRI (Companion). IEEE Computer Society, 86\u201393."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2736348"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050010"},{"volume-title":"Timed Automata Model for Component-Based Real-Time Systems","author":"Macariu Georgiana","key":"e_1_3_2_1_31_1","unstructured":"Georgiana Macariu and Vladimir Cretu . 2010. Timed Automata Model for Component-Based Real-Time Systems . In ECBS. IEEE Computer Society , 121\u2013130. Georgiana Macariu and Vladimir Cretu. 2010. Timed Automata Model for Component-Based Real-Time Systems. In ECBS. IEEE Computer Society, 121\u2013130."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Enrique Mart\u00ednez Mar\u00eda-Emilia Cambronero Gregorio D\u00edaz and Gerardo Schneider. 2011. Timed Automata Semantics for Visual e-Contracts. In FLACOS(EPTCS Vol.\u00a068). 7\u201321. Enrique Mart\u00ednez Mar\u00eda-Emilia Cambronero Gregorio D\u00edaz and Gerardo Schneider. 2011. Timed Automata Semantics for Visual e-Contracts. In FLACOS(EPTCS Vol.\u00a068). 7\u201321.","DOI":"10.4204\/EPTCS.68.3"},{"volume-title":"Time and Petri Nets","author":"Popova-Zeugmann Louchka","key":"e_1_3_2_1_33_1","unstructured":"Louchka Popova-Zeugmann . 2013. Time and Petri Nets . Springer . Louchka Popova-Zeugmann. 2013. Time and Petri Nets. Springer."},{"key":"e_1_3_2_1_34_1","unstructured":"RTCA Special Committee. 2012. DO-178C software considerations in airborne systems and equipment certification. RTCA Special Committee. 2012. DO-178C software considerations in airborne systems and equipment certification."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"crossref","unstructured":"Robert\u00a0G. Sargent. 1998. Verification and Validation of Simulation Models. In WSC. WSC 121\u2013130. Robert\u00a0G. Sargent. 1998. Verification and Validation of Simulation Models. In WSC. WSC 121\u2013130.","DOI":"10.1109\/WSC.1998.744907"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2001.936213"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01667079"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.36"},{"key":"e_1_3_2_1_39_1","volume-title":"USENIX Security Symposium. USENIX Association, 87\u2013104","author":"Vasudevan Amit","year":"2016","unstructured":"Amit Vasudevan , Sagar Chaki , Petros Maniatis , Limin Jia , and Anupam Datta . 2016 . \u00fcberSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor . In USENIX Security Symposium. USENIX Association, 87\u2013104 . Amit Vasudevan, Sagar Chaki, Petros Maniatis, Limin Jia, and Anupam Datta. 2016. \u00fcberSpark: Enforcing Verifiable Object Abstractions for Automated Compositional Security Analysis of a Hypervisor. In USENIX Security Symposium. USENIX Association, 87\u2013104."}],"event":{"name":"RTNS'2021: 29th International Conference on Real-Time Networks and Systems","acronym":"RTNS'2021","location":"NANTES France"},"container-title":["29th International Conference on Real-Time Networks and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453417.3453431","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453417.3453431","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3453417.3453431","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:03:06Z","timestamp":1750197786000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3453417.3453431"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,4,7]]},"references-count":39,"alternative-id":["10.1145\/3453417.3453431","10.1145\/3453417"],"URL":"https:\/\/doi.org\/10.1145\/3453417.3453431","relation":{},"subject":[],"published":{"date-parts":[[2021,4,7]]},"assertion":[{"value":"2021-07-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}