Navegar

Colección

Datos Estadísticas

Artículo

De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S. "Enabledness-based program abstractions for behavior validation" (2013) ACM Transactions on Software Engineering and Methodology. 22(3)
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

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. © 2013 ACM.

Registro:

Documento: Artículo
Título:Enabledness-based program abstractions for behavior validation
Autor:De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S.
Filiación:Departamento de Computacion, FCEyN, Universidad de Buenos Aires, Argentina
Universidad de Buenos Aires, Imperial College, Argentina
Palabras clave:Enabledness abstractions; Source-code validation
Año:2013
Volumen:22
Número:3
DOI: http://dx.doi.org/10.1145/2491509.2491519
Título revista:ACM Transactions on Software Engineering and Methodology
Título revista abreviado:ACM Trans. Software Eng. Methodol.
ISSN:1049331X
CODEN:ATSME
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_1049331X_v22_n3_p_DeCaso

Referencias:

  • Alur, R., Cerny, P., Madhusudan, P., Nam, W., Synthesis of interface specifications for java classes (2005) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Panguages (POPL'05)., pp. 98-109
  • Andersen, M., Barnett, M., Fahndrich, M., Grunkemeyer, B., King, K., Logozzo, F., Patel, V., Zuniga, D., (2009) Code Contracts., , http://research.microsoft.com/enus/projects/contracts
  • Barrett, C., Berezin, S., Cvc lite: A new implementation of the cooperating validity checker (2004) Proceedings of the 16th International Conference on Computer Aided Verification (CAV'04)., pp. 515-518
  • Beckman, N., Nori, A., Probabilistic, modular and scalable inference of typestate specifications (2011) Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'11
  • Beckman, N.E., Kim, D., Aldrich, J., An empirical study of object protocols in the wild (2011) Proceedings of the 25th European Conference on Object-Oriented Programming (ECOOP'11
  • Beschastnikh, I., Brun, Y., Sloan, S., Ernst, M., Leveraging existing instrumentation to automatically infer invariant-constrained models (2011) Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software Engineering (FSE'11
  • Beyer, D., Henzinger, T., Jhala, R., Majumdar, R., The software model checker blast (2007) Int. J. Softw. Tools Technol. Transfer, 9 (5), pp. 505-525
  • Bierhoff, K., Aldrich, J., Plural: Checking protocol compliance under aliasing (2008) Companion of the 30th International Conference on Software Engineering (ICSE'08)., pp. 971-972. , ACM Press, New York
  • Cok, D., Kiniry, J., Esc/java2: Uniting esc/java and jml (2005) Proceedings of the International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, 3362, pp. 108-128. , Lecture Notes in Computer Science. Springer
  • Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A., Generating test cases for specification mining (2010) Proceedings of the International Symposium on Software Testing and Analysis
  • Dallmeier, V., Lindig, C., Wasylkowski, A., Zeller, A., Mining object behavior with adabu (2006) Proceedings of the Workshop on Dynamic Systems Analysis
  • De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S., Automated abstractions for contract validation (2010) IEEE Trans. Softw. Engin., 38 (1), pp. 141-162
  • Deline, R., Fahndrich, M., Enforcing high-level protocols in low-level software (2001) Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01)., pp. 59-69
  • Demsky, B., Rinard, M., Automatic extraction of heap reference properties in object-oriented programs (2009) IEEE Trans. Softw. Engin., 35, pp. 305-324
  • Dijkstra, E., Guarded commands, nondeterminacy and formal derivation of programs (1975) Comm. ACM, 18 (8), pp. 453-457
  • Ernst, M., Perkins, J., Guo, P., Mccamant, S., Pacheco, C., Tschantz, M., Xiao, C., The daikon system for dynamic detection of likely invariants (2007) Sci. Comput. Program., 69, pp. 35-45
  • Gabel, M., Su, Z., Symbolic mining of temporal specifications (2008) Companion of the 30th International Conference on Software Engineering (ICSE'08)., pp. 51-60
  • Ghezzi, C., Mocci, A., Monga, M., Synthesizing intensional behavior models by graph transformation (2009) Companion of the 31st International Conference on Software Engineering (ICSE'09)., pp. 430-440
  • Giannakopoulou, D., Pasa Reanu, C., Interface generation and compositional verification in javapathfinder (2009) Proceedings of the 12th 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)., pp. 94-108
  • Graf, S., Saidi, H., Construction of abstract state graphs with pvs (1997) Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97)., pp. 72-83
  • Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M., Generating finite state machines from abstract state machines (2002) Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA'02)., pp. 112-122
  • Grieskamp, W., Kicillof, N., Macdonald, D., Nandan, A., Stobie, K., Wurden, F., Model-based quality assurance of windows protocol documentation (2008) Proceedings of the 1st International Conference on Software Testing, Verification, and Validation (ICST'08)., pp. 502-506
  • Grieskamp, W., Kicillof, N., Stobie, K., Braberman, V., Model-based quality assurance of protocol documentation: Tools and methodology (2011) Softw. Testing Verif. Reliabil., 21 (1), pp. 55-71
  • Henzinger, T., Jhala, R., Majumdar, R., Permissive interfaces (2005) Proceedings of the 10th European Software Engineering Conference held jointly with the 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE'05)., pp. 31-40
  • Hodges, W., (1997) A Shorter Model Theory, , Cambridge University Press
  • Khurshid, S., Pasa Reanu, C., Visser, W., Generalized symbolic execution for model checking and testing (2003) Tools and Algorithms for the Construction and Analysis of Systems, pp. 553-568
  • Klensin, J., Freed, N., Rose, M., Stefferud, E., Crocker, D., (1995) Smtp Service Extensions., , Tech. rep., RFC 2846
  • Leavens, G., Leino, K., Muller, P., Specification and verification challenges for sequential objectoriented programs (2007) Formal Aspects Comput., 19 (2), pp. 159-189
  • Lee, D., Yannakakis, M., Online minimization of transition systems (extended abstract) (1992) Proceedings of the 24th Annual ACM Symposium on Theory of Computing (STOC'92)., pp. 264-274
  • Liu, L., Meyer, B., Schoeller, B., Using contracts and boolean queries to improve the quality of automatic test generation (2007) Proceedings of the 1st International Conference on Tests and Proofs (TAP'07)., pp. 114-130
  • Lorenzoli, D., Mariani, L., Pezze, M., Automatic generation of software behavioral models (2008) Companion of the 30th International Conference on Software Engineering (ICSE'08)., pp. 501-510
  • Nanda, M., Grothoff, C., Chandra, S., Deriving object typestates in the presence of interobject references (2005) ACM SIGPLAN Not., 40 (10), pp. 77-96
  • Pacheco, C., Ernst, M., Randoop: Feedback-directed random testing for java (2007) Proceeding of the Companion to the 22nd ACM SIGPLAN Conference on Object-Oriented Programming Systems and Applications Companion (OOPSLA'07)., pp. 815-816. , ACM Press, New York
  • Pradel, M., Gross, T.R., Automatic generation of object usage specifications from large method traces (2009) Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE'09)., pp. 371-382. , IEEE
  • Strom, R., Yemini, S., Typestate: A programming language concept for enhancing software reliability (1986) IEEE Trans. Softw. Engin., 12 (1), pp. 157-171
  • Uribe, T., (1999) Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems., , http://wwwstep.stanford.edu/papers/dissertations/tomas.pdf
  • Zoppi, E., Braberman, V., De Caso, G., Garbervetsky, D., Uchitel, S., Contractor.net: Inferring typestate properties to enrich code contracts (2011) Proceedings of the 1st Workshop on Developing Tools as Plug-ins (TOPI'11)., pp. 44-47. , ACM Press, New York

Citas:

---------- APA ----------
De Caso, G., Braberman, V., Garbervetsky, D. & Uchitel, S. (2013) . Enabledness-based program abstractions for behavior validation. ACM Transactions on Software Engineering and Methodology, 22(3).
http://dx.doi.org/10.1145/2491509.2491519
---------- CHICAGO ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. "Enabledness-based program abstractions for behavior validation" . ACM Transactions on Software Engineering and Methodology 22, no. 3 (2013).
http://dx.doi.org/10.1145/2491509.2491519
---------- MLA ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. "Enabledness-based program abstractions for behavior validation" . ACM Transactions on Software Engineering and Methodology, vol. 22, no. 3, 2013.
http://dx.doi.org/10.1145/2491509.2491519
---------- VANCOUVER ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. Enabledness-based program abstractions for behavior validation. ACM Trans. Software Eng. Methodol. 2013;22(3).
http://dx.doi.org/10.1145/2491509.2491519