Model and Program Repair via SAT Solving

Eshmun Tool

Barrier Synchronization with 4 Barriers.

Click on the picture to view all the pictures in high quality.

4 Barriers Synchronization: Abstracted by Formula.

Click on the picture to view all the pictures in high quality.

Barrier Synchronization: 2 Barriers, 2 Processes (Full Paper).

Click on the picture to view all the pictures in high quality.

Dining Philosopher for 2 Philosophers.

Click on the picture to view all the pictures in high quality.

Eventually Serialized Data Service: Replica-Replica Pair Repaired.

Click on the picture to view all the pictures in high quality.

2 Process Mutual Exclusion with Liveness (Full Paper).

Click on the picture to view all the pictures in high quality.

5 Processes Mutual Exclusion Abstracted By Label

Click on the picture to view all the pictures in high quality.

5 Processes Mutual Exclusion

Click on the picture to view all the pictures in high quality.

Two Rounds Phone call Repaired (Full Paper).

Click on the picture to view all the pictures in high quality.

Concurrent Mutual Exclusion for 3 Pairs

Click on the picture to view all the pictures in high quality.

Abstract:

We consider the 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. 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 generate 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, i.e., repair a structure abstracted from M and then concretize the resulting repair to obtain a  repair of M , and (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. (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.

We successfully repaired the following (some of which is shown above in the pictures):

1. Mutual Exclusion.
2. Barrier Synchronization.
3. Dining Philosophers.
4. Eventually Serializable Data Service.
5. One and Two rounds Phone call.

Downloads:

 - The tool (version 0.2) can be downloaded here. It is a runnable jar file, it required java 7. Please notice that the tool is still under development and is not a final-release.

 - You can access the tool user-manual here. The tool user-manual is also available inside the tool, under the Help Menu (or by pressing F1).

 - The full paper can be accessed here.

 - The examples used in the paper, and benchmarks are available in the following zip archive. The archive contains two folders:

1. single: contains examples on single Kripke structures divided into folders: phone call, mutual exclusion, a simple dining philosophers (2 philosophers), and barrier synchronization.
2. concurrent: contains examples on concurrent Kripke structures and programs: ESDS, mutual exclusion, dining philosophers.
3. Every file is named with a number, representing the number of processes in the structure.

Technical References:

1. Synthesis of Large Dynamic Concurrent Programs from Dynamic Specifications, P. C. Attie.
2. Synthesis of Concurrent Systems with Many Similar Processes, P. C. Attie and E. A. Emerson.

3. Synthesis of Large Concurrent Programs via Pairwise Composition, P. C. Attie.

Currently Under Implementation:
The following are under implementation:

1. Decision Procedure, the form included in the jar is a placeholder.
2. Abstracting concurrent structures: currently it abstracts, but repair is not possible.
3. Making the repair traverse buttons more efficient: currently old repairs might reappear, sometimes the repair itself remains visible for few trials. This is due to having extra variables in the repair formula that don't immediately impact the visible repair.

Bug reports:
 
If a bug was encountered, please submit a bug report to the following email eshmuntool@gmail.com, please attach with it a saved copy of the structure causing the bug, or details on how to reproduce the bug on our machines to study it. Your feedback is highly appreciated and will help us deliver a better tool.