Model and program repair via sat solving

Paul C. Attie, Kinan Dak Al Bab, Mouhammad Sakr

Research output: Contribution to journalArticle

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 η 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.

Original languageEnglish (US)
Article number32
JournalACM Transactions on Embedded Computing Systems
Volume17
Issue number2
DOIs
StatePublished - Dec 2017
Externally publishedYes

Keywords

  • Model checking
  • Model repair
  • Program repair
  • Temporal logic

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Model and program repair via sat solving'. Together they form a unique fingerprint.

  • Cite this