Abstract
In the concurrent objects model, objects have conceptually dedicated processors and live in a distributed environment with unordered communication by means of asynchronous method calls. Method callers may decide at runtime when to synchronize with the reply from a call. This paper presents a CLP-based approach to symbolic execution of concurrent OO programs. Developing a symbolic execution engine for concurrent objects is challenging because it needs to combine the OO features of the language, concurrency and backtracking. Our approach consists in, first, transforming the OO program into an equivalent CLP program which contains calls to specific builtins that handle the concurrency model. The builtins are implemented in CLP and include primitives to handle asynchronous calls synchronization operations and scheduling policies, among others. Interestingly, symbolic execution of the transformed programs then relies simply on the standard sequential execution of CLP. We report on a prototype implementation within the PET system which shows the feasibility of our approach.
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.
References
Agha, G.A.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)
Aichernig, B.K., Griesmayer, A., Schlatte, R., Stam, A.: Modeling and Testing Multi-Threaded Asynchronous Systems with Creol. ENTCS 243, 3–14 (2009)
Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost Analysis of Java Bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157–172. Springer, Heidelberg (2007)
Albert, E., Genaim, S., Gómez-Zamalloa, M., Johnsen, E.B., Schlatte, R., Tarifa, S.L.T.: Simulating Concurrent Behaviors with Worst-Case Cost Bounds. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 353–368. Springer, Heidelberg (2011)
Armstrong, J., Virding, R., Wistrom, C., Williams, M.: Concurrent Programming in Erlang. Prentice Hall (1996)
de Boer, F.S., Clarke, D., Johnsen, E.B.: A Complete Guide to the Future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007)
Gómez-Zamalloa, M., Albert, E., Puebla, G.: Decompilation of Java Bytecode to Prolog by Partial Evaluation. JIST 51, 1409–1427 (2009)
Gómez-Zamalloa, M., Albert, E., Puebla, G.: Test Case Generation for Object-Oriented Imperative Languages in CLP. TPLP, ICLP 2010 Special Issue (2010)
Gotlieb, A., Botella, B., Rueher, M.: A CLP Framework for Computing Structural Test Data. In: Palamidessi, C., Moniz Pereira, L., Lloyd, J.W., Dahl, V., Furbach, U., Kerber, M., Lau, K.-K., Sagiv, Y., Stuckey, P.J. (eds.) CL 2000. LNCS (LNAI), vol. 1861, pp. 399–413. Springer, Heidelberg (2000)
Griesmayer, A., Aichernig, B.K., Johnsen, E.B., Schlatte, R.: Dynamic Symbolic Execution of Distributed Concurrent Objects. In: Lee, D., Lopes, A., Poetzsch-Heffter, A. (eds.) FMOODS 2009. LNCS, vol. 5522, pp. 225–230. Springer, Heidelberg (2009)
Gupta, G., Pontelli, E., Ali, K., Carlsson, M., Hermenegildo, M.: Parallel Execution of Prolog Programs: a Survey. ACM TOPLAS 23(4), 472–602 (2001)
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: A Core Language for Abstract Behavioral Specification. In: Proc. of FMCO 2010. Springer, Heidelberg (to appear, 2011)
Johnsen, E.B., Owe, O.: An Asynchronous Communication Model for Distributed concurrent objects. Software and Systems Modeling 6(1), 35–58 (2007)
Khurshid, S., Păsăreanu, C.S., 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. Commun. ACM 19(7), 385–394 (1976)
Meudec, C.: Atgen: Automatic Test Data Generation using Constraint Logic Programming and Symbolic Execution. Softw. Test., Verif. Reliab. 11(2), 81–96 (2001)
Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Inc., Upper Saddle River (1997)
Müller, R.A., Lembeck, C., Kuchen, H.: A Symbolic Java Virtual Machine for Test Case Generation. In: IASTED Conf. on Software Engineering, pp. 365–371 (2004)
Rungta, N., Mercer, E.G., Visser, W.: Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 174–191. Springer, Heidelberg (2009)
Schäfer, J., Poetzsch-Heffter, A.: Jcobox: Generalizing Active Objects to Concurrent Components. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 275–299. Springer, Heidelberg (2010)
Srinivasan, S., Mycroft, A.: Kilim: Isolation-Typed Actors for Java. In: Ryan, M. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 104–128. Springer, Heidelberg (2008)
Takahashi, J., Kojima, H., Furukawa, Z.: Coverage based Testing for Concurrent Software. In: ICDCS Workshops, pp. 533–538. IEEE Computer Society (2008)
Tillmann, N., de Halleux, J.: Pex–White Box Test Generation for.NET. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 134–153. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Albert, E., Arenas, P., Gómez-Zamalloa, M. (2012). Symbolic Execution of Concurrent Objects in CLP. In: Russo, C., Zhou, NF. (eds) Practical Aspects of Declarative Languages. PADL 2012. Lecture Notes in Computer Science, vol 7149. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-27694-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-27694-1_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-27693-4
Online ISBN: 978-3-642-27694-1
eBook Packages: Computer ScienceComputer Science (R0)