column

Automated model repair for distributed programs

Authors:

Borzoo Bonakdarpour,

Sandeep S. KulkarniAuthors Info & Claims

ACM SIGACT News, Volume 43, Issue 2

Pages 85 - 107

https://doi.org/10.1145/2261417.2261437

Published: 11 June 2012 Publication History

Abstract

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.

References

[1]

F. Abujarad, B. Bonakdarpour, and S. S. Kulkarni. Parallelizing deadlock resolution in symbolic synthesis of distributed programs. In Parallel and Distributed Methods in verifiCation (PDMC), 2009.

[2]

F. Abujarad and S. S. Kulkarni. Multicore constraint-based automated stabilization. In International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 47--61, 2009.

Digital Library

[3]

F. Abujarad and S. S. Kulkarni. Complexity issues in automated model revision without explicit legitimate states. In International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), pages 206--220, 2010.

Digital Library

[4]

K. Akesson, M. Fabian, H. Flordal, and A. Vahidi. Supremica a tool for verification and synthesis of discrete event supervisors. In Mediterranean Conference on Control and Automation, 2003.

[5]

B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21:181--185, 1985.

[6]

R. Alur, C. Courcoubetis, N. Halbwachs, D. L. Dill, and H. Wong-Toi. Minimization of timed transition systems. In International Conference on Concurrency Theory (CONCUR), pages 340--354, 1992.

Digital Library

[7]

R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183--235, 1994.

Digital Library

[8]

R. Alur and T.A. Henzinger. A really temporal logic. Journal of the ACM, 41(1):181--204, 1994.

Digital Library

[9]

A. Arora and S. S. Kulkarni. Detectors and correctors: A theory of fault-tolerance components. In International Conference on Distributed Computing Systems (ICDCS), pages 436--443, 1998.

Digital Library

[10]

E. Bartocci, R. Grosu, P. Katsaros, C. R. Ramakrishnan, and S. A. Smolka. Model repair for probabilistic systems. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 326--340, 2011.

Digital Library

[11]

R. Bloem, K. Chatterjee, T. A. Henzinger, and B. Jobstmann. Better quality in synthesis through quantitative objectives. In Computer Aided Verification (CAV), pages 140--156, 2009.

Digital Library

[12]

B. Bonakdarpour, A. Ebnenasir, and S. S. Kulkarni. Complexity results in revising UNITY programs. ACM Transactions on Autonomous and Adaptive Systems (TAAS), 4(1):1--28, January 2009.

Digital Library

[13]

B. Bonakdarpour and S. S. Kulkarni. Automated incremental synthesis of timed automata. In International Workshop on Formal Methods for Industrial Critical Systems (FMICS), LNCS 4346, pages 261--276, 2006.

Digital Library

[14]

B. Bonakdarpour and S. S. Kulkarni. Automated revision of legacy real-time programs:work in progress. In IEEE Real-Time and Embedded, Technology and Applications Symposium (RTAS), 2006.

[15]

B. Bonakdarpour and S. S. Kulkarni. Incremental synthesis of fault-tolerant real-time programs. In International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), LNCS 4280, pages 122--136, 2006.

Digital Library

[16]

B. Bonakdarpour and S. S. Kulkarni. Exploiting symbolic techniques in automated synthesis of distributed programs with large state space. In IEEE International Conference on Distributed Computing Systems (ICDCS), pages 3--10, 2007.

Digital Library

[17]

B. Bonakdarpour and S. S. Kulkarni. Revising distributed UNITY programs is NP-complete. In Principles of Distributed Systems (OPODIS), pages 408--427, 2008.

Digital Library

[18]

B. Bonakdarpour and S. S. Kulkarni. SYCRAFT: A tool for synthesizing fault-tolerant distributed programs. In Concurrency Theory (CONCUR), pages 167--171, 2008.

Digital Library

[19]

B. Bonakdarpour, S. S. Kulkarni, and F. Abujarad. Symbolic synthesis of masking fault-tolerant programs. Distributed Computing. To appear.

[20]

B. Bonakdarpour, S. S. Kulkarni, and Fuad Abujarad. Distributed synthesis of fault-tolerant programs in the high atomicity model. In International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS), LNCS 4838, pages 21--36, 2007.

Digital Library

[21]

R. E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 35(8):677--691, 1986.

Digital Library

[22]

F. Buccafurri, T. Eiter, G. Gottlob, and N. Leone. Enhancing model checking in verification by ai techniques. Artificial Intelligence, 112:57--104, 1999.

Digital Library

[23]

P. Cerny, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh. Quantitative synthesis for concurrent programs. In Computer Aided Verification (CAV), pages 243--259, 2011.

Digital Library

[24]

K. M. Chandy and J. Misra. Parallel program design: a foundation. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1988.

Digital Library

[25]

K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh. QUASY: Quantitative synthesis tool. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 267--271, 2011.

Digital Library

[26]

G. Chatzieleftheriou, B. Bonakdarpour, S. A. Smolka, and P. Katsaros. Abstract model repair. In NASA Formal Methods Symposium (NFM), 2012. To appear.

Digital Library

[27]

J. Chen and A. S. Kulkarni. Effectiveness of transition systems to model faults. In Logical Aspects of Fault-Tolerance (LAFT), 2011.

[28]

K. H. Cho and J. T. Lim. Synthesis of fault-tolerant supervisor for automated manufacturing systems: A case study on photolithography process. IEEE Transactions on Robotics and Automation, 14(2):348--351, 1998.

[29]

M. R. Clarkson and F. B. Schneider. Hyperproperties. Journal of Computer Security, 18(6):1157--1210, 2010.

Digital Library

[30]

E. W. Dijkstra. A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ., 1990.

[31]

A. Ebnenasir, S. S. Kulkarni, and A. Arora. FTSyn: a framework for automatic synthesis of faulttolerance. International Journal of Software Tools for Technology Transfer (STTT), 10(5):455--471, 2008.

Digital Library

[32]

E. A. Emerson. Handbook of Theoretical Computer Science, volume B, chapter 16: Temporal and Modal Logics, pages 995--1067. Elsevier Science Publishers B. V., Amsterdam, 1990.

Digital Library

[33]

E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241--266, 1982.

[34]

R. Fagin, J.Y. Halpern nad Y. Moses, and M. Vardi. Reasoning About Knowledge. The MIT Press, 1995.

Digital Library

[35]

L. Feng and W. M. Wonham. TCT: A computation tool for supervisory control synthesis. In International Workshop on Discrete Event Systems, pages 388--389, 2006.

[36]

A. Girault and É. Rutten. Automating the addition of fault tolerance with discrete controller synthesis. Formal Methods in System Design (FMSD), 35(2):190--225, 2009.

Digital Library

[37]

B. Jobstmann and R. Bloem. Lily - A LInear Logic Synthesizer. http://www.ist.tugraz.at/staff/jobstmann/lily/.

[38]

B. Jobstmann, S. Galler, M. Weiglhofer, and R. Bloem. Anzu: A tool for property synthesis. In Computer Aided Verification (CAV), pages 258--262, 2007.

Digital Library

[39]

B. Jobstmann, A. Griesmayer, and R. Bloem. Program repair as a game. In Computer Aided Verification (CAV), pages 226--238, 2005.

Digital Library

[40]

S. S. Kulkarni and A. Arora. Automating the addition of fault-tolerance. In Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), pages 82--93, 2000.

Digital Library

[41]

S. S. Kulkarni, A. Arora, and A. Chippada. Polynomial time synthesis of Byzantine agreement. In Symposium on Reliable Distributed Systems (SRDS), pages 130--140, 2001.

[42]

S. S. Kulkarni and M. Arumugam. Infuse: A TDMA based data dissemination protocol for sensor networks. International Journal on Distributed Sensor Networks (IJDSN), 2(1):55--78, 2006.

[43]

S. S. Kulkarni and A. Ebnenasir. The complexity of adding failsafe fault-tolerance. International Conference on Distributed Computing Systems (ICDCS), pages 337--344, 2002.

Digital Library

[44]

S. S. Kulkarni and A. Ebnenasir. Enhancing the fault-tolerance of nonmasking programs. International Conference on Distributed Computing Systems, 2003.

Digital Library

[45]

S. S. Kulkarni and A. Ebnenasir. Adding fault-tolerance using pre-synthesized components. In European Dependable Computing Conference (EDCC), pages 72--90, 2005.

Digital Library

[46]

L. Lamport, R. Shostak, and M. Pease. The Byzantine generals problem. ACM Transactions on Programming Languages and Systems (TOPLAS), 4(3):382--401, 1982.

Digital Library

[47]

L. Lamport, R. Shostak, and M. Pease. The Byzantine generals problem. ACM Transactions on Programming Languages and Systems, 1982.

Digital Library

[48]

G. Lowe. Breaking and fixing the needham-schroeder public-key protocol using FDR. In Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 147--166, 1996.

Digital Library

[49]

Z. Manna and P. Wolper. Synthesis of communicating processes from temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 6(1):68--93, 1984.

Digital Library

[50]

A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Principles of Programming Languages (POPL), pages 179--190, 1989.

Digital Library

[51]

P. J. Ramadge and W. M. Wonham. The control of discrete event systems. Proceedings of the IEEE, 77(1):81--98, 1989.

[52]

K. Raymond. A tree based algorithm for mutual exclusion. ACM Transactions on Computer Systems, 7:61--77, 1989.

Digital Library

[53]

R. Samanta, J. V. Deshmukh, and E. A. Emerson. Automatic generation of local repairs for boolean programs. In Formal Methods in Computer-Aided Design (FMCAD), pages 1--10, 2008.

Digital Library

[54]

R. D. Schlichting and F. B. Schneider. Fail-stop processors: An approach to designing fault-tolerant computing systems. ACM Transactions on Computers, 1(3):222--238, 1983.

Digital Library

[55]

A. Solar-Lezama, L. Tancau, R. Bodik, S. Seshia, and V. Saraswat. Combinatorial sketching for finite programs. ACM SIGPLAN Notices, 41(11):404--415, 2006.

Digital Library

[56]

W. Thomas. On the synthesis of strategies in infinite games. In Theoretical Aspects of Computer Science (STACS), pages 1--13, 1995.

[57]

Y. Zhang and Y. Ding. CTL model update for system modifications. Journal of Artificial Intelligence, 31:113--155, January 2008.

Digital Library

Cited By

Pacheco MHippel MWeintraub BGoldwasser DNita-Rotaru C(2022)Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833673(51-68)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833673
Gerasimou SCalinescu RTamburrelli G(2018)Synthesis of probabilistic models for quality-of-service software engineeringAutomated Software Engineering10.5555/3288647.328870925:4(785-831)Online publication date: 26-Dec-2018
https://dl.acm.org/doi/10.5555/3288647.3288709
Gerasimou SCalinescu RTamburrelli G(2018)Synthesis of probabilistic models for quality-of-service software engineeringAutomated Software Engineering10.1007/s10515-018-0235-825:4(785-831)Online publication date: 17-May-2018
https://doi.org/10.1007/s10515-018-0235-8
Show More Cited By

Automated model repair for distributed programs
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Trust in Automated Software Repair: The Effects of Repair Source, Transparency, and Programmer Experience on Perceived Trustworthiness and Trust
HCI for Cybersecurity, Privacy and Trust
Abstract
Automation and autonomous systems are becoming increasingly pervasive in society, as are the software systems that control them. There is a need for safe and secure software systems. Automated code repair provides a promising solution. The present ...
Automated Repair of Multi-fault Programs: Obstacles, Approaches, and Prospects
ASE '24: Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering

Modern automated program repair (APR) tools are well-tuned at repairing single fault programs (i.e., programs in which only one fault can occur at time). However, real-world software projects typically contain multiple bugs at the same time, which can ...
Do automated program repair techniques repair hard and important bugs?

Existing evaluations of automated repair techniques focus on the fraction of the defects for which the technique can produce a patch, the time needed to produce patches, and how well patches generalize to the intended specification. However, these ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGACT News

ACM SIGACT News Volume 43, Issue 2

June 2012

134 pages

ISSN:0163-5700

DOI:10.1145/2261417

Issue’s Table of Contents

Copyright © 2012 Authors.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 June 2012

Published in SIGACT Volume 43, Issue 2

Check for updates

Qualifiers

Column

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
140
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pacheco MHippel MWeintraub BGoldwasser DNita-Rotaru C(2022)Automated Attack Synthesis by Extracting Finite State Machines from Protocol Specification Documents2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833673(51-68)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833673
Gerasimou SCalinescu RTamburrelli G(2018)Synthesis of probabilistic models for quality-of-service software engineeringAutomated Software Engineering10.5555/3288647.328870925:4(785-831)Online publication date: 26-Dec-2018
https://dl.acm.org/doi/10.5555/3288647.3288709
Gerasimou SCalinescu RTamburrelli G(2018)Synthesis of probabilistic models for quality-of-service software engineeringAutomated Software Engineering10.1007/s10515-018-0235-825:4(785-831)Online publication date: 17-May-2018
https://doi.org/10.1007/s10515-018-0235-8
Gerasimou STamburrelli GCalinescu RCohen MGrunske LWhalen M(2015)Search-based synthesis of probabilistic models for quality-of-service software engineeringProceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2015.22(319-330)Online publication date: 9-Nov-2015
https://dl.acm.org/doi/10.1109/ASE.2015.22

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents