Eshmun
v0.2 alpha
 From Structures to Models

Paul C. Attie <paul.attie [at] aub dot edu dot lb>
Jad Saklawi <jad.saklawi [at] aub dot edu dot lb>

Overview of the Eshmun Structure Repair Tool:

Our tool is named after Eshmun, the Phoenician god of healing. 


Eshmun is based on the repair algorithm given in "Model and Program Repair via SAT Solving".

Latest version of Eshmun can be found here.

To run Eshmun the following is required:

For the automatic filling in of propositional labels feature please see mutex page.

We now present an example of repair of the Barrier Synchronization example:

  • Create a structure that is to be model checked, and repaired if needed. Currently the structure is input by the user. Future extension will allow the user to input a concurrent program, and then the structure will be automatically generated, as the state transition diagram of the program.




  • Structure repair: a structure can be repaired with respect to a CTL formula eta by a call to repair. If succesful, the resulting model satisfies eta.
  • We now repair the above structure with respect to the following Computation Tree Logic (CTL) specification:
    1. Initially both processes are at the start of phase A: SA1 ∧ SA2
    2. P1 and P2 are never simultaneously at the start of different phases:
          AG(¬(SA1 ∧ SB2)) ∧AG(¬(SA2 ∧ SB1))
    3. P1 and P2 are never simultaneously at the end of different phases:
          AG(¬(EA1 ∧ EB2)) ∧AG(¬(EA2 ∧ EB1))

    • Invoking repair with respect to the above specification produces the following model: