Program Repair Suggestions from Graphical State-Transition Specifications

  • Farn Wang
  • Chih-Hong Cheng
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5048)


In software engineering, graphical formalisms, like state- transition tables and automata, are very often indispensable parts of the specifications. Such a formalism usually leads to specification refinement that maintains the simulation/bisimulation relation between an implementation and a specification. We investigate how to use formal techniques to generate suggestions for repairing a program that breaks the bisimulation relation with a graphical specification. We use state graphs as a unified representation of the program models and specifications. We propose a technique that may evaluate the cost of a repair. We present a PTIME heuristic algorithm that suggests how to repair a model state graph. We then explain how to derive repair suggestions for programs from the repair for state graphs. Finally, we report our experiment that checks the performance of our repair algorithms and the costs of our repairs.


state graph state transition relation repair graph theory cost evaluation equivalence bisimulation 


  1. 1.
    Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  2. 2.
    Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)CrossRefzbMATHGoogle Scholar
  3. 3.
    Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing Model Checking in Verification by AI Techniques. Artificial Intelligence 112(1), 55–93 (1999)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Bunke, H.: On a Relation between Graph Edit Distance and Maximum Common Subgraph. Pattern Recognition Letters 19, 255–259 (1997)CrossRefGoogle Scholar
  5. 5.
    Clarke, E., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching-Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  6. 6.
    Ding, Y., Zhang, Y.: A Logic Approach for LTL System Modification. In: Hacid, M.-S., Murray, N.V., Raś, Z.W., Tsumoto, S. (eds.) ISMIS 2005. LNCS (LNAI), vol. 3488, pp. 435–444. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  7. 7.
    Ding, Y., Zhang, Y.: Algorithms for CTL System Modification. In: Khosla, R., Howlett, R.J., Jain, L.C. (eds.) KES 2005. LNCS (LNAI), vol. 3682. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  8. 8.
    Fisler, K., Vardi, M.Y.: Bisimulation Minimization in an Automata-Theoretic Verification Framework. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  9. 9.
    Griesmayer, A., Bloem, R., Cook, B.: Repair of Boolean Programs with an Application to C. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, New York (1979)zbMATHGoogle Scholar
  11. 11.
  12. 12.
    Jobstmann, B., Griesmayer, A., Bloem, R.: Program Repair as a Game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  13. 13.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  14. 14.
    Myers, G.J., Sandler, C., Badgett, T., Thomas, T.M.: The Art of Software Testing. Wiley, Chichester (2004)Google Scholar
  15. 15.
    Paige, R., Tarjan, R.E.: Three Partition Refinement Algorithms. SIAM J. 6, 973–989 (1987)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
  17. 17.
    Tsay, Y.-K., Chen, Y.-F., Tsai, M.-H., Wu, K.-N., Chan, W.-C.: GOAL: A Graphical Tool for Manipulating Buchi Automata and Temporal Formulae. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424. Springer, Heidelberg (2007)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2008

Authors and Affiliations

  • Farn Wang
    • 1
    • 2
  • Chih-Hong Cheng
    • 1
  1. 1.Dept. of Electrical EngineeringNational Taiwan UniversityTaiwan, ROC
  2. 2.Grad. Inst. of Electronic EngineeringNational Taiwan UniversityTaiwan, ROC

Personalised recommendations