{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:26:51Z","timestamp":1750307211050,"version":"3.41.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2012,6,11]],"date-time":"2012-06-11T00:00:00Z","timestamp":1339372800000},"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":["SIGACT News"],"published-print":{"date-parts":[[2012,6,11]]},"abstract":"<jats:p>Model repair is a formal method that aims at fixing bugs in models automatically. Typically, these models are finite state automata that can be compactly represented using guarded commands or variations thereof. The bugs in these models can be identified using traditional techniques, such as verification, testing, or runtime monitoring. However, these techniques do not assist in fixing bugs automatically. The goal in model repair is to automatically transform an input model into another model that satisfies additional properties (e.g., a property that the original model fails to satisfy). Moreover, such transformation should preserve the existing specification of the input model. In this article, we review the efforts in the past decade on developing model repair algorithms in different domains. These domains include distributed computing, fault-tolerance and self-stabilization, and real-time systems. We present the results on complexity analysis, techniques for tackling intractability of the problem and scalability, and related tools. The techniques and tools discussed in this article demonstrate the feasibility of automated synthesis of well-known protocols such as Byzantine agreement, token ring, fault-tolerant mutual exclusion, etc.<\/jats:p>","DOI":"10.1145\/2261417.2261437","type":"journal-article","created":{"date-parts":[[2012,6,15]],"date-time":"2012-06-15T15:31:37Z","timestamp":1339774297000},"page":"85-107","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Automated model repair for distributed programs"],"prefix":"10.1145","volume":"43","author":[{"given":"Borzoo","family":"Bonakdarpour","sequence":"first","affiliation":[{"name":"University of Waterloo, Waterloo, ON, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sandeep S.","family":"Kulkarni","sequence":"additional","affiliation":[{"name":"Michigan State University, East Lansing, MI"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,6,11]]},"reference":[{"volume-title":"Parallel and Distributed Methods in verifiCation (PDMC)","year":"2009","author":"Abujarad F.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05118-0_4"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1926829.1926849"},{"volume-title":"Mediterranean Conference on Control and Automation","year":"2003","author":"Akesson K.","key":"e_1_2_1_4_1"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/646727.703209"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/174644.174651"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/850926.851714"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987428"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462187.1462192"},{"key":"e_1_2_1_13_1","first-page":"261","volume-title":"International Workshop on Formal Methods for Industrial Critical Systems (FMICS), LNCS 4346","author":"Bonakdarpour B.","year":"2006"},{"volume-title":"Technology and Applications Symposium (RTAS)","year":"2006","author":"Bonakdarpour B.","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1759076.1759087"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.2007.109"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-92221-6_26"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_16"},{"key":"e_1_2_1_19_1","unstructured":"B. Bonakdarpour S. S. Kulkarni and F. Abujarad. Symbolic synthesis of masking fault-tolerant programs. Distributed Computing. To appear.  B. Bonakdarpour S. S. Kulkarni and F. Abujarad. Symbolic synthesis of masking fault-tolerant programs. Distributed Computing. To appear."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1785110.1785115"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00039-9"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/2032305.2032325"},{"volume-title":"Inc.","year":"1988","author":"Chandy K. M.","key":"e_1_2_1_24_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987420"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_32"},{"volume-title":"Logical Aspects of Fault-Tolerance (LAFT)","year":"2011","author":"Chen J.","key":"e_1_2_1_27_1"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/70.681255"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"volume-title":"NJ.","year":"1990","author":"Dijkstra E. W.","key":"e_1_2_1_30_1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0083-0"},{"key":"e_1_2_1_32_1","first-page":"995","volume-title":"Temporal and Modal Logics","author":"Emerson E. A.","year":"1990"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"volume-title":"The MIT Press","year":"1995","author":"Fagin R.","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/WODES.2006.382399"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-009-0084-y"},{"key":"e_1_2_1_37_1","unstructured":"B. Jobstmann and R. Bloem. Lily - A LInear Logic Synthesizer. http:\/\/www.ist.tugraz.at\/staff\/jobstmann\/lily\/.  B. Jobstmann and R. Bloem. Lily - A LInear Logic Synthesizer. http:\/\/www.ist.tugraz.at\/staff\/jobstmann\/lily\/."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770351.1770390"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_23"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/646846.706965"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/RELDIS.2001.969767"},{"volume-title":"International Journal on Distributed Sensor Networks (IJDSN), 2(1):55--78","year":"2006","author":"Kulkarni S. S.","key":"e_1_2_1_42_1"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/850928.851854"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/850929.851948"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/11408901_6"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357176"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.5555\/646480.693776"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/357233.357237"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.21072"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/58564.59295"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.5555\/1517424.1517451"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/357369.357371"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168917.1168907"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59042-0_57"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622655.1622659"}],"container-title":["ACM SIGACT News"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2261417.2261437","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2261417.2261437","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T10:06:37Z","timestamp":1750241197000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2261417.2261437"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,11]]},"references-count":57,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2012,6,11]]}},"alternative-id":["10.1145\/2261417.2261437"],"URL":"https:\/\/doi.org\/10.1145\/2261417.2261437","relation":{},"ISSN":["0163-5700"],"issn-type":[{"type":"print","value":"0163-5700"}],"subject":[],"published":{"date-parts":[[2012,6,11]]},"assertion":[{"value":"2012-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}