Abstract
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.
Chapter PDF
Similar content being viewed by others
References
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)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing Model Checking in Verification by AI Techniques. Artificial Intelligence 112(1), 55–93 (1999)
Bunke, H.: On a Relation between Graph Edit Distance and Maximum Common Subgraph. Pattern Recognition Letters 19, 255–259 (1997)
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)
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)
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)
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)
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)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman, New York (1979)
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)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Myers, G.J., Sandler, C., Badgett, T., Thomas, T.M.: The Art of Software Testing. Wiley, Chichester (2004)
Paige, R., Tarjan, R.E.: Three Partition Refinement Algorithms. SIAM J. 6, 973–989 (1987)
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 IFIP International Federation for Information Processing
About this paper
Cite this paper
Wang, F., Cheng, CH. (2008). Program Repair Suggestions from Graphical State-Transition Specifications. In: Suzuki, K., Higashino, T., Yasumoto, K., El-Fakih, K. (eds) Formal Techniques for Networked and Distributed Systems – FORTE 2008. FORTE 2008. Lecture Notes in Computer Science, vol 5048. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68855-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-540-68855-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68854-9
Online ISBN: 978-3-540-68855-6
eBook Packages: Computer ScienceComputer Science (R0)