research-article

Model and Program Repair via SAT Solving

Authors:

Kinan Dak Al Bab,

Mouhammad SakrAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 17, Issue 2

Article No.: 32, Pages 1 - 25

https://doi.org/10.1145/3147426

Published: 07 December 2017 Publication History

Abstract

We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M^′ that satisfies η. Thus, M can be “repaired” to satisfy eta by deleting some transitions and states. We map an instance 〈 M,η 〉 of model repair to a Boolean formula repair(M,η) such that 〈 M,η 〉 has a solution iff repair(M,η) is satisfiable. Furthermore, a satisfying assignment determines which states and transitions must be removed from M to yield a model M^′ of η Thus, we can use any SAT solver to repair Kripke structures. Using a complete SAT solver yields a complete algorithm: it always finds a repair if one exists. We also show that CTL model repair is NP-complete. We extend the basic repair method in three directions: (1) the use of abstraction mappings, that is, repair a structure abstracted from M and then concretize the resulting repair to obtain a repair of M, (2) repair concurrent Kripke structures and concurrent programs: we use the pairwise method of Attie and Emerson to represent and repair the behavior of a concurrent program, as a set of “concurrent Kripke structures”, with only a quadratic increase in the size of the repair formula, and (3) repair hierarchical Kripke structures: we use a CTL formula to summarize the behavior of each “box,” and CTL deduction to relate the box formula with the overall specification.

References

[1]

R. Alur, T. A. Henzinger, and O. Kupferman. 2002. Alternating-time temporal logic. J. ACM 49 (2002), 672--713.

Digital Library

[2]

R. Alur and M. Yannakakis. 2001. Model checking of hierarchical state machines. ACM Trans. Program. Lang. Syst. 23, 3 (2001), 273--303.

Digital Library

[3]

P. C. Attie. 2016. Finite-state concurrent programs can be expressed in pairwise normal form. Theor. Comput. Sci. 619 (2016), 1--31.

Digital Library

[4]

P. C. Attie. 2016. Synthesis of large dynamic concurrent programs from dynamic specifications. Formal Methods Syst. Design 48, 1 (2016), 94--147.

Digital Library

[5]

P. C. Attie and E. A. Emerson. 1996. Synthesis of concurrent systems for an atomic read/atomic write model of computation. In Proceedings of the 15th Annual ACM Symposium on Principles of Distributed Computing (PODC’96). ACM, New York, NY, 111--120.

Digital Library

[6]

P. C. Attie and E. A. Emerson. 2001. Synthesis of concurrent programs for an atomic read/write model of computation. Trans. Program. Lang. Syst. 23, 2 (2001), 187--242.

Digital Library

[7]

P. C. Attie. 1999. Synthesis of large concurrent programs via pairwise composition. In Proceedings of the 10th International Conference on Concurrency Theory (CONCUR’99). Springer-Verlag, Eindhoven, The Netherlands, 130--145.

Digital Library

[8]

P. C. Attie and E. A. Emerson. 1998. Synthesis of concurrent systems with many similar processes. Trans. Program. Lang. Syst. 20, 1 (Jan. 1998), 51--115.

Digital Library

[9]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. 1999. Symbolic model checking without BDDs. In Proceedings of the Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’99), LNCS No. 1579. Springer-Verlag, Amsterdam, The Netherlands, 193--207.

Digital Library

[10]

M. C. Browne, E. M. Clarke, and O. Grumberg. 1988. Characterizing finite kripke structures in propositional temporal logic. Theoret. Comput. Sci. 59 (1988), 115--131.

Digital Library

[11]

F. Buccafurri, T. Eiter, G. Gottlob, and N. Leone. 1999. Enhancing model checking in verification by AI techniques. Artif. Intell. 112 (1999), 57--104.

Digital Library

[12]

M. Carrillo and D. A. Rosenblueth. 2009. A method for CTL model update, representing kripke structures as table systems. Int. J. Pure Appl. Math. 52 (2009), 401--431.

[13]

G. Chatzieleftheriou, B. Bonakdarpour, S. A. Smolka, and P. Katsaros. 2012. Abstract model repair. In NASA Formal Methods, Alwyn E. Goodloe and Suzette Person (Eds.). Lecture Notes in Computer Science, Vol. 7226. Springer, Berlin. 341--355.

Digital Library

[14]

E. M. Clarke, E. A. Emerson, and J. Sifakis. 2009. Model checking: Algorithmic verification and debugging. Commun. ACM 52, 11 (Nov. 2009), 74--84.

Digital Library

[15]

E. M. Clarke, O. Grumberg, and D. E. Long. 1994. Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16, 5 (Sept. 1994), 1512--1542.

Digital Library

[16]

E. M. Clarke and H. Veith. 2003. Counterexamples revisited: Principles, algorithms, applications. In Verification: Theory and Practice. Springer, 208--224.

[17]

E. M. Clarke, E. A. Emerson, and P. Sistla. 1986. Automatic verification of finite-state concurrent systems using temporal logic specifications. Trans. Program. Lang. Syst. 8, 2 (1986), 244--263.

Digital Library

[18]

E. M. Clarke, O. Grumberg, K. L. McMillan, and X. Zhao. 1995. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the Design Automation Conference. ACM Press, New York, NY, 427--432.

Digital Library

[19]

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

Digital Library

[20]

E. A. Emerson. 1990. Temporal and modal logic. Handbook of Theoretical Computer Science B (1990), 997--1072.

Digital Library

[21]

E. A. Emerson and E. M. Clarke. 1982. Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2, 3 (1982), 241--266.

[22]

A. Fekete, D. Gupta, V. Luchango, N. Lynch, and A. Shvartsman. 1999. Eventually-serializable data services. Theor. Comput. Sci. 220 (1999), 113--156.

Digital Library

[23]

S. Graf and H. Saidi. 1997. Construction of abstract state graphs with PVS. In Proceedings of the Conference on Computer Aided Verification (CAV’97). LNCS, Vol. 1254. Springer, London, UK, 72--83.

Digital Library

[24]

O. Grumberg and D. E. Long. 1994. Model checking and modular verification. Trans. Program. Lang. Syst. 16, 3 (1994), 843--871.

Digital Library

[25]

R. Hojati, R. K. Brayton, and R. P. Kurshan. 1993. BDD-based debugging of designs using language containment and fair CTL. In Proceedings of the Conference on Computer Aided Verification (CAV’93). Springer-Verlag, London, UK, 41--58. Springer LNCS No. 697.

Digital Library

[26]

B. Jobstmann, A. Griesmayer, and R. Bloem. 2005. Program repair as a game. In Proceedings of the Conference on Computer Aided Verification (CAV’05). Springer-Verlag, Berlin, Heidelberg, 226--238.

Digital Library

[27]

R. Ladin, B. Liskov, L. Shrira, and S. Ghemawat. 1992. Providing high availability using lazy replication. ACM Trans. Comput. Syst. 10, 4 (Nov. 1992), 360--391.

Digital Library

[28]

D. Le Berre, A. Parrain, et al. 2010. The sat4j library, release 2.2, system description. J. Satis. Boolean Model. Comput. 7 (2010), 59--64.

[29]

S. Shoham and O. Grumberg. 2003. A game-based framework for CTL counterexamples and 3-valued abstraction-refinement. In Proceedings of the Conference on Computer Aided Verification (CAV’03). ACM, New York, NY, 275--287.

[30]

S. Staber, B. Jobstmann, and R. Bloem. 2005. Finding and fixing faults. In Proceedings of the Conference on Correct Hardware Design and Verification Methods (CHARME’05). Springer-Verlag, Berlin, 35--49. Springer LNCS No. 3725.

Digital Library

[31]

C. Stirling and D. Walker. 1991. Local model checking in the modal mu-calculus. Theor. Comput. Sci. 89, 1 (1991), 161--177.

Digital Library

[32]

Y. Zhang and Y. Ding. 2008. CTL model update for system modifications. J. Artif. Int. Res. 31, 1 (Jan. 2008), 113--155.

Digital Library

Cited By

Attie PCocke W(2023)Model and Program Repair via Group ActionsFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_25(520-540)Online publication date: 21-Apr-2023
https://doi.org/10.1007/978-3-031-30829-1_25
Frenkel HGrumberg ORothenberg BSheinvald S(2022)Automated Program Repair Using Formal Verification TechniquesPrinciples of Systems Design10.1007/978-3-031-22337-2_25(511-534)Online publication date: 29-Dec-2022
https://doi.org/10.1007/978-3-031-22337-2_25
Rothenberg BGrumberg O(2020)Must Fault Localization for Program RepairComputer Aided Verification10.1007/978-3-030-53291-8_33(658-680)Online publication date: 21-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-53291-8_33

Index Terms

Model and Program Repair via SAT Solving
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Correctness
      2. Formal methods
        Model checking
    2. Software system structures
      1. Software system models
        Model-driven software engineering
        State systems

Recommendations

Model and Program Repair via Group Actions
Foundations of Software Science and Computation Structures
Abstract
Given a textual representation of a finite-state concurrent program $P$ , one can construct the corresponding Kripke structure $M$ . However, the size of $M$ can be exponentially larger than the textual size of $P$ . This state explosion can make model ... $\overset{}{}$ $\overset{}{}$
$\overset{}{}$ $\overset{}{}$ $\overset{}{}$ $\overset{}{}$
$\overset{}{}$ $\overset{}{}$
Model and program repair via SAT solving
MEMOCODE '15: Proceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign

We consider the subtractive model repair problem: given a finite Kripke structure M and a CTL formula η, determine if M contains a substructure M' that satisfies η. Thus, M can be repaired to satisfy η by deleting states and/or transitions. We give a ...
Automatic B-model repair using model checking and machine learning
Abstract
The B-method, which provides automated verification for the design of software systems, still requires users to manually repair faulty models. This paper proposes B-repair, an approach that supports automated repair of faulty models written in the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 17, Issue 2

Special Issue on MEMCODE 2015 and Regular Papers (Diamonds)

March 2018

640 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/3160927

Editor:
Sandeep K. Shukla
Indian Institute of Technology, India

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 07 December 2017

Accepted: 01 February 2017

Revised: 01 July 2016

Received: 01 January 2016

Published in TECS Volume 17, Issue 2

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
179
Total Downloads

Downloads (Last 12 months)11
Downloads (Last 6 weeks)2

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Attie PCocke W(2023)Model and Program Repair via Group ActionsFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_25(520-540)Online publication date: 21-Apr-2023
https://doi.org/10.1007/978-3-031-30829-1_25
Frenkel HGrumberg ORothenberg BSheinvald S(2022)Automated Program Repair Using Formal Verification TechniquesPrinciples of Systems Design10.1007/978-3-031-22337-2_25(511-534)Online publication date: 29-Dec-2022
https://doi.org/10.1007/978-3-031-22337-2_25
Rothenberg BGrumberg O(2020)Must Fault Localization for Program RepairComputer Aided Verification10.1007/978-3-030-53291-8_33(658-680)Online publication date: 21-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-53291-8_33

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 Article

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