More Web Proxy on the site http://driver.im/

research-article

Testing of concurrent and imperative software using CLP

Authors:

Miguel Gómez-ZamalloaAuthors Info & Claims

PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

Pages 1 - 8

https://doi.org/10.1145/2967973.2968593

Published: 05 September 2016 Publication History

Abstract

Testing is a vital part of the software development process. In static testing, instead of executing the program on normal values (e.g., numbers), typically the program is executed on symbolic variables representing arbitrary values. Constraints on the symbolic variables are used to represent the conditions under which the execution paths are taken. Testing tools can uncover issues such as memory leaks, buffer overflows, and also concurrency errors like deadlocks or data races. Due to its inherent symbolic execution mechanism and the availability of constraint solvers, Constraint Logic Programming (CLP) has a big potential in the field of testing. In this talk, we will describe a fully CLP-based framework to testing of a today's imperative language. We will also discuss the extension of this framework to handle actor-based concurrency, used in languages such as Go, Actor-Foundry, Erlang, and Scala, among others.

References

[1]

Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos F. Sagonas. Optimal Dynamic Partial Order Reduction. In Proc. of POPL'14, pages 373--384. ACM, 2014.

Digital Library

[2]

G. Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, 1986.

Digital Library

[3]

E. Albert, P. Arenas, S. Genaim, G. Puebla, and D. Zanardini. Cost Analysis of Java Bytecode. In Procs. of ESOP'07, volume 4421 of LNCS, pages 157--172. Springer, 2007.

Digital Library

[4]

Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Symbolic Execution of Concurrent Objects in CLP. In Proc. of PADL'12, volume 7149 of LNCS, pages 123--137. Springer, 2012.

Digital Library

[5]

Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Actor- and Task-Selection Strategies for Pruning Redundant State-Exploration in Testing. In Proc. of FORTE'14, volume 8461 of LNCS, pages 49--65. Springer, 2014.

[6]

Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Test Case Generation of Actor Systems. In Proc. of ATVA'15, volume 9364 of LNCS, pages 259--275. Springer, 2015.

[7]

Elvira Albert, Puri Arenas, Miguel Gómez-Zamalloa, and Peter Y.H. Wong. aPET: A Test Case Generation Tool for Concurrent Objects. In Proc. of ESEC/FSE'13, pages 595--598. ACM, 2013.

Digital Library

[8]

Elvira Albert, Israel Cabañas, Antonio Flores-Montoya, Miguel Gómez-Zamalloa, and Sergio Gutiérrez. jPET: an Automatic Test-Case Generator for Java. In Proc. of WCRE'11, pages 441--442. IEEE Computer Society, 2011.

Digital Library

[9]

Elvira Albert, María García de la Banda, Miguel Gómez-Zamalloa, José Miguel Rojas, and Peter Stuckey. A CLP Heap Solver for Test Case Generation. Theory and Practice of Logic Programming, 13(4-5):721--735, July 2013.

[10]

Elvira Albert, Miguel Gómez-Zamalloa, Laurent Hubert, and Germán Puebla. Verification of Java Bytecode using Analysis and Transformation of Logic Programs. In Proc. of PADL'07, volume 4354 of LNCS, pages 124--139. Springer, 2007.

Digital Library

[11]

Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. Combining Static Analysis and Testing for Deadlock Detection. In Proc. of IFM'16, volume 9681 of LNCS, pages 409--424. Springer, 2016.

Digital Library

[12]

Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. SYCO: A Systematic Testing Tool for Concurrent Objects. In Proc. of CC'16, pages 269--270. ACM, 2016.

Digital Library

[13]

Elvira Albert, Miguel Gómez-Zamalloa, and Germán Puebla. Test Data Generation of Bytecode by CLP Partial Evaluation. In Proc. of LOPSTR'08, volume 5438 of LNCS, pages 4--23. Springer, 2009.

Digital Library

[14]

Elvira Albert, Miguel Gómez-Zamalloa, and Germán Puebla. PET: A Partial Evaluation-based Test Case Generation Tool for Java Bytecode. In Proc. of PEPM'10, pages 25--28. ACM Press, 2010.

Digital Library

[15]

Maria Christakis, Alkis Gotovos, and Konstantinos F. Sagonas. Systematic Testing for Detecting Concurrency Errors in Erlang Programs. In Proc. of ICST'13, pages 154--163. IEEE Computer Society, 2013.

Digital Library

[16]

Lori A. Clarke. A System to Generate Test Data and Symbolically Execute Programs. IEEE Transactions on Software Engineering, 2(3):215--222, 1976.

Digital Library

[17]

F. Degrave, T. Schrijvers, and W. Vanhoof. Towards a Framework for Constraint-Based Test Case Generation. In Proc. of LOPSTR'09, volume 6037 of LNCS, pages 128--142. Springer, 2010.

Digital Library

[18]

C. Engel and R. Hähnle. Generating Unit Tests from Formal Proofs. In Proc. of TAP'07, volume 4454 of LNCS, pages 169--188. Springer, 2007.

Digital Library

[19]

J. Esparza. Model checking using net unfoldings. Sci. Comput. Program., 23(2-3):151--195, 1994.

Digital Library

[20]

Roger Ferguson and Bogdan Korel. The Chaining Approach for Software Test Data Generation. ACM Trans. Softw. Eng. Methodol., 5(1):63--86, 1996.

Digital Library

[21]

C. Flanagan and P. Godefroid. Dynamic Partial-Order Reduction for Model Checking Software. In Proc. of POPL'05, pages 110--121. ACM, 2005.

Digital Library

[22]

P. Godefroid. Using Partial Orders to Improve Automatic Verification Methods. In Proc. of CAV'91, volume 531 of LNCS, pages 176--185. Springer, 1991.

Digital Library

[23]

Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of LNCS. Springer, 1996.

Digital Library

[24]

M. Gómez-Zamalloa, E. Albert, and G. Puebla. Decompilation of Java Bytecode to Prolog by Partial Evaluation. JIST, 51:1409--1427, October 2009.

Digital Library

[25]

Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. Decompilation of Java Bytecode to Prolog by Partial Evaluation. Information and Software Technology, 51(10):1409--1427, October 2009.

Digital Library

[26]

Miguel Gómez-Zamalloa, Elvira Albert, and Germán Puebla. Test Case Generation for Object-Oriented Imperative Languages in CLP. Theory and Practice of Logic Programming, ICLP'10 Special Issue, 10(4-6):659--674, 2010.

Digital Library

[27]

A. Gotlieb, B. Botella, and M. Rueher. A CLP Framework for Computing Structural Test Data. In Proc. CL'00, volume 1861 of LNAI, pages 399--413. Springer, 2000.

Digital Library

[28]

Neelam Gupta, Aditya P. Mathur, and Mary Lou Soffa. Generating Test Data for Branch Coverage. In Proc. of ASE'00, pages 219--228. IEEE Computer Society, 2000.

Digital Library

[29]

P. Haller and M. Odersky. Scala Actors: Unifying Thread-based and Event-based Programming. Theor. Comput. Sci., 410(2-3):202--220, 2009.

Digital Library

[30]

James C. King. Symbolic Execution and Program Testing. Communications of the ACM, 19(7):385--394, 1976.

Digital Library

[31]

Steven Lauterburg, Rajesh K. Karmani, Darko Marinov, and Gul Agha. Evaluating Ordering Heuristics for Dynamic Partial-Order Reduction Techniques. In Proc. of FASE'10, volume 6013 of LNCS, pages 308--322. Springer, 2010.

Digital Library

[32]

Christophe Meudec. ATGen: Automatic Test Data Generation using Constraint Logic Programming and Symbolic Execution. Softw. Test., Verif. Reliab., 11(2):81--96, 2001.

[33]

Roger A. Müller, Christoph Lembeck, and Herbert Kuchen. A Symbolic Java Virtual Machine for Test Case Generation. In Proc. of IASTEDSE'04, pages 365--371. ACTA Press, 2004.

[34]

Jose M. Rojas and Miguel Gómez-Zamalloa. A Framework for Guided Test Case Generation in Constraint Logic Programming. In Proc. of LOPSTR'12, volume 7844 of LNCS. Springer, 2013.

[35]

N. Rungta, E.G. Mercer, and W. Visser. Efficient Testing of Concurrent Programs with Abstraction-Guided Symbolic Execution. In Proc. of SPIN'09, volume 5578 of LNCS. Springer, 2009.

Digital Library

[36]

Olli Saarikivi, Kari Kahkonen, and Keijo Heljanko. Improving Dynamic Partial Order Reductions for Concolic Testing. In Proc. of ACSD'12, pages 132--141. IEEE Computer Society, 2012.

Digital Library

[37]

Koushik Sen and Gul Agha. Automated Systematic Testing of Open Distributed Programs. In Proc. of FASE'06, volume 3922 of LNCS, pages 339--356. Springer, 2006.

Digital Library

[38]

S. Tasharofi, R. K. Karmani, S. Lauterburg, A. Legay, D. Marinov, and G. Agha. TransDPOR: A Novel Dynamic Partial-Order Reduction Technique for Testing Actor Programs. In Proc. of FMOODS/FORTE'12, volume 7273 of LNCS, pages 219--234. Springer, 2012.

Digital Library

[39]

H. Zhu, P. A. V. Hall, and J. H. R. May. Software Unit Test Coverage and Adequacy. ACM Comput. Surv., 29(4):366--427, 1997.

Digital Library

Cited By

Albert ECañizares PGuerra Ede Lara JMarcos ENúñez MRomán-Díez GVara JZanardini D(2018)SICOMORo-CM: Development of Trustworthy Systems via Models and Advanced ToolsSoftware Technologies: Applications and Foundations10.1007/978-3-319-74730-9_32(367-374)Online publication date: 23-Jan-2018
https://doi.org/10.1007/978-3-319-74730-9_32

Index Terms

Testing of concurrent and imperative software using CLP
1. Computing methodologies
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Sophisticated Testing of Concurrent Programs
SSBSE '10: Proceedings of the 2nd International Symposium on Search Based Software Engineering

Search-based techniques were successfully applied to many different areas of testing but according to our knowledge there are no works that applies search-based techniques to testing of concurrent software, yet. This PhD paper describes plans and ...
Testing atomicity of composed concurrent operations
OOPSLA '11: Proceedings of the 2011 ACM international conference on Object oriented programming systems languages and applications

We address the problem of testing atomicity of composed concurrent operations. Concurrent libraries help programmers exploit parallel hardware by providing scalable concurrent operations with the illusion that each operation is executed atomically. ...
A Scala library for testing student assignments on concurrent programming
SCALA 2016: Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala

We present a lightweight library for testing concurrent Scala programs by systematically exploring multiple interleavings between user-specified operations on shared objects. Our library is targeted at beginners of concurrent programming in Scala, runs ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

PPDP '16: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming

September 2016

249 pages

ISBN:9781450341486

DOI:10.1145/2967973

Conference Chair:
James Cheney
University of Edinburgh, UK
,
Program Chair:
Germán Vidal
Universitat Politècnica de València, Spain

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 September 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Spanish MINECO project
EU project
CM project

Conference

PPDP '16

PPDP '16: 18th International Symposium on Principles and Practice of Declarative Programming

September 5 - 7, 2016

Edinburgh, United Kingdom

Acceptance Rates

PPDP '16 Paper Acceptance Rate 17 of 37 submissions, 46%;

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
60
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Albert ECañizares PGuerra Ede Lara JMarcos ENúñez MRomán-Díez GVara JZanardini D(2018)SICOMORo-CM: Development of Trustworthy Systems via Models and Advanced ToolsSoftware Technologies: Applications and Foundations10.1007/978-3-319-74730-9_32(367-374)Online publication date: 23-Jan-2018
https://doi.org/10.1007/978-3-319-74730-9_32

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents