Model and Program Repair via SAT Solving
| Autor: | Paul C. Attie, Kinan Dak Al Bab, Mouhammad Sakr |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Model checking
Discrete mathematics True quantified Boolean formula Kripke structure Structure (category theory) 020207 software engineering 02 engineering and technology Set (abstract data type) CTL TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Hardware and Architecture 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Temporal logic Boolean satisfiability problem Software Mathematics |
| Zdroj: | ACM Transactions on Embedded Computing Systems. 17:1-25 |
| ISSN: | 1558-3465 1539-9087 |
| DOI: | 10.1145/3147426 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|