research-article

Enabledness-based program abstractions for behavior validation

Authors:

Victor Braberman,

Diego Garbervetsky,

Sebastian UchitelAuthors Info & Claims

ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 22, Issue 3

Article No.: 25, Pages 1 - 46

https://doi.org/10.1145/2491509.2491519

Published: 30 July 2013 Publication History

Abstract

Code artifacts that have nontrivial requirements with respect to the ordering in which their methods or procedures ought to be called are common and appear, for instance, in the form of API implementations and objects. This work addresses the problem of validating if API implementations provide their intended behavior when descriptions of this behavior are informal, partial, or nonexistent. The proposed approach addresses this problem by generating abstract behavior models which resemble typestates. These models are statically computed and encode all admissible sequences of method calls. The level of abstraction at which such models are constructed has shown to be useful for validating code artifacts and identifying findings which led to the discovery of bugs, adjustment of the requirements expected by the engineer to the requirements implicit in the code, and the improvement of available documentation.

References

[1]

Alur, R., Cerny, P., Madhusudan, P., and Nam, W. 2005. Synthesis of interface specifications for java classes. In Proceedings of the 32^nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Panguages (POPL'05). 98--109.

Digital Library

[2]

Andersen, M., Barnett, M., Fahndrich, M., Grunkemeyer, B., King, K., Logozzo, F., Patel, V., and Zuniga, D. 2009. Code contracts. http://research.microsoft.com/enus/projects/contracts.

[3]

Barrett, C. and Berezin, S. 2004. CVC Lite: A new implementation of the cooperating validity checker. In Proceedings of the 16^th International Conference on Computer Aided Verification (CAV'04). 515--518.

[4]

Beckman, N. and Nori, A. 2011. Probabilistic, modular and scalable inference of typestate specifications. In Proceedings of the 32^nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'11).

Digital Library

[5]

Beckman, N. E., Kim, D., and Aldrich, J. 2011. An empirical study of object protocols in the wild. In Proceedings of the 25^th European Conference on Object-Oriented Programming (ECOOP'11).

Digital Library

[6]

Beschastnikh, I., Brun, Y., Sloan, S., and Ernst, M. 2011. Leveraging existing instrumentation to automatically infer invariant-constrained models. In Proceedings of the 19^th ACM SIGSOFT Symposium and the 13^th European Conference on Foundations of Software Engineering (FSE'11).

Digital Library

[7]

Beyer, D., Henzinger, T., Jhala, R., and Majumdar, R. 2007. The software model checker blast. Int. J. Softw. Tools Technol. Transfer 9, 5, 505--525.

Digital Library

[8]

Bierhoff, K. and Aldrich, J. 2008. Plural: Checking protocol compliance under aliasing. In Companion of the 30^th International Conference on Software Engineering (ICSE'08). ACM Press, New York, 971--972.

Digital Library

[9]

Cok, D. and Kiniry, J. 2005. ESC/Java2: Uniting esc/java and jml. In Proceedings of the International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices. Lecture Notes in Computer Science, vol. 3362. Springer, 108--128.

Digital Library

[10]

Dallmeier, V., Knopp, N., Mallon, C., Hack, S., and Zeller, A. 2010. Generating test cases for specification mining. In Proceedings of the International Symposium on Software Testing and Analysis.

Digital Library

[11]

Dallmeier, V., Lindig, C., Wasylkowski, A., and Zeller, A. 2006. Mining object behavior with ADABU. In Proceedings of the Workshop on Dynamic Systems Analysis.

Digital Library

[12]

De Caso, G., Braberman, V., Garbervetsky, D., and Uchitel, S. 2010. Automated abstractions for contract validation. IEEE Trans. Softw. Engin. 38, 1, 141--162.

Digital Library

[13]

Deline, R. and Fahndrich, M. 2001. Enforcing high-level protocols in low-level software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01). 59--69.

Digital Library

[14]

Demsky, B. and Rinard, M. 2009. Automatic extraction of heap reference properties in object-oriented programs. IEEE Trans. Softw. Engin. 35, 305--324.

Digital Library

[15]

Dijkstra, E. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM 18, 8, 453--457.

Digital Library

[16]

Ernst, M., Perkins, J., Guo, P., Mccamant, S., Pacheco, C., Tschantz, M., and Xiao, C. 2007. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69, 35--45.

Digital Library

[17]

Gabel, M. and Su, Z. 2008. Symbolic mining of temporal specifications. In Companion of the 30^th International Conference on Software Engineering (ICSE'08). 51--60.

Digital Library

[18]

Ghezzi, C., Mocci, A., and Monga, M. 2009. Synthesizing intensional behavior models by graph transformation. In Companion of the 31^st International Conference on Software Engineering (ICSE'09). 430--440.

Digital Library

[19]

Giannakopoulou, D. and Pasa Reanu, C. 2009. Interface generation and compositional verification in javapathfinder. In Proceedings of the 12^th International Conference on Fundamental Approaches to Software Engineering (FASE'09): Held as Part of the Joint European Conferences on Theory and Practice of Software (ETAPS'09). 94--108.

Digital Library

[20]

Graf, S. and Saidi, H. 1997. Construction of abstract state graphs with pvs. In Proceedings of the 9^th International Conference on Computer Aided Verification (CAV'97). 72--83.

Digital Library

[21]

Grieskamp, W., Gurevich, Y., Schulte, W., and Veanes, M. 2002. Generating finite state machines from abstract state machines. In Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'02). 112--122.

Digital Library

[22]

Grieskamp, W., Kicillof, N., Macdonald, D., Nandan, A., Stobie, K., and Wurden, F. 2008. Model-based quality assurance of windows protocol documentation. In Proceedings of the 1^st International Conference on Software Testing, Verification, and Validation (ICST'08). 502--506.

Digital Library

[23]

Grieskamp, W., Kicillof, N., Stobie, K., and Braberman, V. 2011. Model-based quality assurance of protocol documentation: Tools and methodology. Softw. Testing Verif. Reliabil. 21, 1, 55--71.

Digital Library

[24]

Henzinger, T., Jhala, R., and Majumdar, R. 2005. Permissive interfaces. In Proceedings of the 10^th European Software Engineering Conference held jointly with the 13^th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE'05). 31--40.

Digital Library

[25]

Hodges, W. 1997. A Shorter Model Theory. Cambridge University Press.

Digital Library

[26]

Khurshid, S., Pasa Reanu, C., and Visser, W. 2003. Generalized symbolic execution for model checking and testing. In Tools and Algorithms for the Construction and Analysis of Systems, 553--568.

Digital Library

[27]

Klensin, J., Freed, N., Rose, M., Stefferud, E., and Crocker, D. 1995. Smtp service extensions. Tech. rep., RFC 2846.

[28]

Leavens, G., Leino, K., and Muller, P. 2007. Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19, 2, 159--189.

[29]

Lee, D. and Yannakakis, M. 1992. Online minimization of transition systems (extended abstract). In Proceedings of the 24^th Annual ACM Symposium on Theory of Computing (STOC'92). 264--274.

Digital Library

[30]

Liu, L., Meyer, B., and Schoeller, B. 2007. Using contracts and boolean queries to improve the quality of automatic test generation. In Proceedings of the 1^st International Conference on Tests and Proofs (TAP'07). 114--130.

Digital Library

[31]

Lorenzoli, D., Mariani, L., and Pezze, M. 2008. Automatic generation of software behavioral models. In Companion of the 30^th International Conference on Software Engineering (ICSE'08). 501--510.

Digital Library

[32]

Nanda, M., Grothoff, C., and Chandra, S. 2005. Deriving object typestates in the presence of interobject references. ACM SIGPLAN Not. 40, 10, 77--96.

Digital Library

[33]

Pacheco, C. and Ernst, M. 2007. Randoop: Feedback-directed random testing for java. In Proceeding of the Companion to the 22^nd ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications Companion (OOPSLA'07). ACM Press, New York, 815--816.

Digital Library

[34]

Pradel, M. and Gross, T. R. 2009. Automatic generation of object usage specifications from large method traces. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE'09). IEEE, 371--382.

Digital Library

[35]

Strom, R. and Yemini, S. 1986. Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Engin. 12, 1, 157--171.

Digital Library

[36]

Uribe, T. 1999. Abstraction-based deductive-algorithmic verification of reactive systems. http://www-step.stanford.edu/papers/dissertations/tomas.pdf.

Digital Library

[37]

Zoppi, E., Braberman, V., De Caso, G., Garbervetsky, D., and Uchitel, S. 2011. Contractor.net: Inferring typestate properties to enrich code contracts. In Proceedings of the 1^st Workshop on Developing Tools as Plug-ins (TOPI'11). ACM Press, New York, 44--47.

Digital Library

Cited By

Nolasco AMolina FDegiovanni RGorla AGarbervetsky DPapadakis MUchitel SAguirre NFrias M(2024)Abstraction-Aware Inference of Metamorphic RelationsProceedings of the ACM on Software Engineering10.1145/36437471:FSE(450-472)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643747
Clerissi DDenaro GMobilio MMariani L(2024)Guess the State: Exploiting Determinism to Improve GUI Exploration EfficiencyIEEE Transactions on Software Engineering10.1109/TSE.2024.336658650:4(836-853)Online publication date: Apr-2024
https://doi.org/10.1109/TSE.2024.3366586
Molina Fd'Amorim MAguirre NDwyer MDamian DZeller A(2022)Fuzzing class specificationsProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510120(1008-1020)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510120
Show More Cited By

Index Terms

Enabledness-based program abstractions for behavior validation

Recommendations

Program abstractions for behaviour validation
ICSE '11: Proceedings of the 33rd International Conference on Software Engineering

Code artefacts that have non-trivial requirements with respect to the ordering in which their methods or procedures ought to be called are common and appear, for instance, in the form of API implementations and objects. This work addresses the problem ...
Deriving behavior of multi-user processes from interactive requirements validation
ASE '10: Proceedings of the 25th IEEE/ACM International Conference on Automated Software Engineering

In this tool demonstration we present an implementation for interactively validating requirements for multi-user software systems and the processes they support with end users. The tool combines the advantages of requirements animation and scenario ...
Automated Abstractions for Contract Validation

Pre/postcondition-based specifications are commonplace in a variety of software engineering activities that range from requirements through to design and implementation. The fragmented nature of these specifications can hinder validation as it is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Software Engineering and Methodology

ACM Transactions on Software Engineering and Methodology Volume 22, Issue 3

In memoriam, fault detection and localization, formal methods, modeling and design

July 2013

414 pages

ISSN:1049-331X

EISSN:1557-7392

DOI:10.1145/2491509

Issue’s Table of Contents

Copyright © 2013 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 30 July 2013

Accepted: 01 May 2012

Revised: 01 May 2012

Received: 01 June 2011

Published in TOSEM Volume 22, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Consejo Nacional de Investigaciones Científicas y Técnicas
UBACyT 20020100100813
PIP112-200801-00955KA4
PICT-PAE 37279
PICT 2010-2351
European Research Council
UBACyt 20020090300064

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
377
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Nolasco AMolina FDegiovanni RGorla AGarbervetsky DPapadakis MUchitel SAguirre NFrias M(2024)Abstraction-Aware Inference of Metamorphic RelationsProceedings of the ACM on Software Engineering10.1145/36437471:FSE(450-472)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643747
Clerissi DDenaro GMobilio MMariani L(2024)Guess the State: Exploiting Determinism to Improve GUI Exploration EfficiencyIEEE Transactions on Software Engineering10.1109/TSE.2024.336658650:4(836-853)Online publication date: Apr-2024
https://doi.org/10.1109/TSE.2024.3366586
Molina Fd'Amorim MAguirre NDwyer MDamian DZeller A(2022)Fuzzing class specificationsProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510120(1008-1020)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510120
Riganelli OMottadelli SRota CMicucci DMariani LKhurshid SPăsăreanu C(2020)Data loss detector: automatically revealing data loss bugs in Android appsProceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3395363.3397379(141-152)Online publication date: 18-Jul-2020
https://dl.acm.org/doi/10.1145/3395363.3397379
Radhakrishna ALewchenko NMeier SMover SSripada KZufferey DChang BČerný PChaudron MCrnkovic IChechik MHarman M(2018)DroidStarProceedings of the 40th International Conference on Software Engineering10.1145/3180155.3180232(1160-1170)Online publication date: 27-May-2018
https://dl.acm.org/doi/10.1145/3180155.3180232
Yang WXu CPan MCao CMa XLu J(2018)Efficient validation of self-adaptive applications by counterexample probability maximizationJournal of Systems and Software10.1016/j.jss.2017.12.009138(82-99)Online publication date: Apr-2018
https://doi.org/10.1016/j.jss.2017.12.009
Howar FGiannakopoulou DMues MNavas J(2018)Generating Component Interfaces by Integrating Static and Symbolic Analysis, Learning, and Runtime MonitoringLeveraging Applications of Formal Methods, Verification and Validation. Verification10.1007/978-3-030-03421-4_9(120-136)Online publication date: 5-Nov-2018
https://dl.acm.org/doi/10.1007/978-3-030-03421-4_9
Klimovic ALitz HKozyrakis C(2017)ReFlexACM SIGPLAN Notices10.1145/3093336.303773252:4(345-359)Online publication date: 4-Apr-2017
https://dl.acm.org/doi/10.1145/3093336.3037732
Crafa SPadovani L(2017)The Chemical Approach to Typestate-Oriented ProgrammingACM Transactions on Programming Languages and Systems10.1145/306484939:3(1-45)Online publication date: 26-May-2017
https://dl.acm.org/doi/10.1145/3064849
Vasconcelos CRavara AShin SShin DLencastre M(2017)From object-oriented code with assertions to behavioural typesProceedings of the Symposium on Applied Computing10.1145/3019612.3019733(1492-1497)Online publication date: 3-Apr-2017
https://dl.acm.org/doi/10.1145/3019612.3019733
Show More Cited By

View Options

Get Access

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 Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents