Abstract
We present a novel algorithm for repairing structurally complex data. Given an assertion that represents desired structural integrity constraints and a structure that violates them, the algorithm performs repair actions that mutate the given structure to generate a new structure that satisfies the constraints. Assertions are written as imperative predicates, which can express rich structural properties. Since these properties can be arbitrarily complex, our algorithm is sound but not complete, and it may not terminate in certain cases. Experimental results with our prototype implementation, Juzi, show that it is feasible to efficiently repair a variety of complex data structures that are routinely used in library code. Juzi can often repair structures comprising of over a hundred objects (even when majority of the objects have some corrupted field) in less than one second. Our algorithm is based on systematic backtracking but does not require storing states and can easily be implemented in a variety of software model checkers, such as the Java PathFinder, SPIN, and VeriSoft.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Adjie-Winoto, W., Schwartz, E., Balakrishnan, H., Lilley, J.: The design and implementation of an intentional naming system. In: Proc. 17th ACM Symposium on Operating Systems Principles (SOSP), Kiawah Island (December 1999)
Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515–518. Springer, Heidelberg (2004)
Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proc. 36thConference on Design Automation (DAC), New Orleans, LA (1999)
Boyapati, C., Khurshid, S., Marinov, D.: Korat: Automated testing based on Java predicates. In: Proc. International Symposium on Software Testing and Analysis (ISSTA), July 2002, pp. 123–133 (2002)
Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: The JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, p. 231. Springer, Heidelberg (2002)
Chiba, S.: Javassist—a reflection-based programming wizard for Java. In: Proceedings of the ACM OOPSLA 1998 Workshop on Reflective Programming in C++ and Java (October 1998)
Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., Zheng, H.: Bandera: Extracting finite-state models from Java source code. In: Proc. 22nd International Conference on Software Engineering (ICSE) (June 2000)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)
Demsky, B., Rinard, M.: Automatic detection and repair of errors in data structures. In: Proc. ACM SIGPLAN 2003 Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 78–95 (2003)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 234–245 (2002)
García, I.: Enabling symbolic execution of Java programs using bytecode instrumentation. Master’s thesis, Department of Electrical and Computer Engineering, The University of Texas at Austin (May 2005)
Godefroid, P.: Model checking for programming languages using VeriSoft. In: Proc. 24th Annual ACM Symposium on the Principles of Programming Languages (POPL), Paris, France, January 1997, pp. 174–186 (1997)
Haugk, G., Lax, F., Royer, R., Williams, J.: The 5ESS(TM) switching system: Maintenance capabilities. AT&T Technical Journal 64(6 part 2), 1385–1416 (1985)
Holzmann, G.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5) (May 1997)
Jackson, D.: Micromodels of software: Modelling and analysis with Alloy (2001), http://sdg.lcs.mit.edu/alloy/book.pdf
Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: Proc. International Symposium on Software Testing and Analysis (ISSTA), Portland, OR (August 2000)
Khurshid, S.: Generating Structurally Complex Tests from Declarative Constraints. PhD thesis, Dept. of Electrical Engineering and Computer Science, Massachusetts Institute of Technology (December 2003)
Khurshid, S., Pasareanu, C., Visser, W.: Generalized symbolic execution for model checking and testing. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 553–568. Springer, Heidelberg (2003)
King, J.C.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR 98-06i, Department of Computer Science, Iowa State University (June 1998)
Liskov, B., Guttag, J.: Program Development in Java: Abstraction, Specification, and Object-Oriented Design. Addison-Wesley, Reading (2000)
Marinov, D.: Automatic Testing of Software with Structurally Complex Inputs. PhD thesis, Computer Science and Artificial Intelligence Laboratory, Massachusetts Institute of Technology (2004)
Marinov, D., Khurshid, S.: TestEra: A novel framework for automated testing of Java programs. In: Proc. 16th IEEE International Conference on Automated Software Engineering (ASE), San Diego, CA (November 2001)
Mourad, S., Andrews, D.: On the reliability of the IBM MVS/XA operating system. IEEE Transactions on Software Engineering 13(10), 1135–1139 (1987)
Rinard, M.: Resilient computing. Technical report, MIT Computer Science and Artificial Intelligence Laboratory (2003) (research abstract)
Smirnov, A., Chiueh, T.C.: DIRA: Automatic detection, identification, and repair of control-hijacking attacks. In: The 12th Annual Network and Distributed System Security Symposium, San Diego, CA (February 2005)
Suen, Y.L.: Automatically repairing structurally complex data. Master’s thesis, Department of Electrical and Computer Engineering, The University of Texas at Austin (May 2005)
United States Nuclear Regulatory Commission. Fault Tree Handbook 1981. NUREG-0492 (1981)
Visser, W., Havelund, K., Brat, G., Park, S.: Model checking programs. In: Proc. 15th IEEE International Conference on Automated Software Engineering (ASE), Grenoble, France (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Khurshid, S., García, I., Suen, Y.L. (2005). Repairing Structurally Complex Data. In: Godefroid, P. (eds) Model Checking Software. SPIN 2005. Lecture Notes in Computer Science, vol 3639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11537328_12
Download citation
DOI: https://doi.org/10.1007/11537328_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28195-5
Online ISBN: 978-3-540-31899-6
eBook Packages: Computer ScienceComputer Science (R0)