Navegar

Colección

Datos Estadísticas

Conferencia

Rosner, N.; Bengolea, V.; Ponzio, P.; Khalek, S.A.; Aguirre, N.; Frias, M.F.; Khurshid, S. "Bounded exhaustive test input generation from hybrid invariants" (2014) 2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014:655-674
Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor

Abstract:

We present a novel technique for producing bounded exhaustive test suites from hybrid invariants, i.e., invariants that are expressed imperatively, declaratively, or as a combination of declarative and imperative predicates. Hybrid specifications are processed using known mechanisms for the imperative and declarative parts, but combined in a way that enables us to exploit information from the declarative side, such as tight bounds computed from the declarative specification, to improve the search both on the imperative and declarative sides. Moreover, our technique automatically evaluates different possible ways of processing the imperative side, and the alternative settings (imperative or declarative) for parts of the invariant available both declaratively and imperatively, to decide the most convenient invariant configuration with respect to efficiency in test generation. This is achieved by transcoping, i.e., by assessing the efficiency of the different alternatives on small scopes (where generation times are negligible), and then extrapolating the results to larger scopes. Copyright 2014 ACM. We also show experiments involving collection classes that support the effectiveness of our technique, by demonstrating that (i) bounded exhaustive suites can be computed from hybrid invariants significantly more efficiently than doing so using state-of-the-art purely imperative and purely declarative approaches, and (ii) our technique is able to automatically determine efficient hybrid invariants, in the sense that they lead to an efficient computation of bounded exhaustive suites, using transcoping.

Registro:

Documento: Conferencia
Título:Bounded exhaustive test input generation from hybrid invariants
Autor:Rosner, N.; Bengolea, V.; Ponzio, P.; Khalek, S.A.; Aguirre, N.; Frias, M.F.; Khurshid, S.
Filiación:Dept. of Computer Science FCEyN, University of Buenos Aires, Buenos Aires, Argentina
Dept. of Computer Science FCEFQyN, University of Rio Cuarto, Rio-Cuarto, Argentina
Google, United States
Dept. of Computer Science FCEFQyN, University of Rio Cuarto and CONICET, Rio-Cuarto, Argentina
Dept. of Software Engineering, Instituto Tecnólogico de Buenos Aires and CONICET, Buenos Aires, Argentina
Electrical and Computer Engineering, University of Texas at Austin, Austin, United States
Palabras clave:Alloy; Automated test generation; Bounded exhaustive testing; Korat; SAT solving; Transcoping; Alloying; Computer programming languages; Computer systems programming; Software testing; Specifications; Automated test generations; Bounded exhaustive testing; Korat; SAT-solving; Transcoping; Object oriented programming
Año:2014
Página de inicio:655
Página de fin:674
DOI: http://dx.doi.org/10.1145/2660193.2660232
Título revista:2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014
Título revista abreviado:Proc Conf Object Orient Program Syst Lang Appl OOPSLA
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_97814503_v_n_p655_Rosner

Referencias:

  • Abad, P., Aguirre, N., Bengolea, V.S., Ciolek, D., Frias, M.F., Galeotti, J.P., Maibaum, T., Vissani, I., Improving test generation under rich contracts by tight bounds and incremental SAT solving (2013) ICST
  • Boyapati, C., Khurshid, S., Marinov, D., Korat: Automated testing based on Java predicates (2002) ISSTA
  • Burdy, L., Cheon, Y., Cok, D.R., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Rustan, K., Poll, E., An overview of JML tools and applications (2005) STTT 7, 3. , Springer
  • Chang, F.S.-H., Jackson, D., Symbolic model checking of declarative relational models (2006) ICSE
  • Claessen, K., Hughes, J., QuickCheck: A lightweight tool for random testing of Haskell programs (2000) ICFP
  • De Moura, L., Bjørner, N., Z3: An efficient SMT solver (2008) TACAS
  • Dennis, G., Chang, F., Jackson, D., Verification of code with SAT (2006) ISSTA 2006, , ACM
  • Dutertre, B., Moura, L.D., (2006) The Yices SMT Solver, , Technical report
  • Een, N., Sorensson, N., An extensible SAT-solver (2003) SAT
  • Frias, M., Galeotti, J., Pombo, C., Aguirre, N., DynAlloy: Upgrading alloy with actions (2005) ICSE
  • Galeotti, J.P., Rosner, N., López Pombo, C., Frias, M., TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds (2013) IEEE TSE, 39 (9), pp. 1283-1307
  • Ganov, S., Khurshid, S., Perry, D.E., Annotations for alloy: Automated incremental analysis using domain specific solvers (2012) ICFEM
  • Geldenhuys, J., Aguirre, N., Frias, M.F., Visser, W., Bounded lazy initialization (2013) NFM 2013, LNCS, , Springer
  • Gligoric, M., Gvero, T., Jagannath, V., Khurshid, S., Kuncak, V., Marinov, D., Test generation through programming in UDITA (2010) ICSE, , Cape Town, South Africa
  • Holzmann, G.J., The model checker SPIN (1997) IEEE TSE
  • Jackson, D., (2006) Software Abstractions: Logic, Language and Analysis, , The MIT Press
  • Kaner, C., Bach, J., Pettichord, B., (2001) Lessons Learned in Software Testing, , Wiley
  • Khalek, S.A., (2011) Systematic Testing Using Test Summaries: Effective and Efficient Testing of Relational Applications, , Ph.D. Thesis. University of Texas at Austin
  • Khalek, S.A., Narayanan, V.P., Khurshid, S., Mixed constraints for test input generation-An initial exploration ASE 2011, , (Short paper)
  • Khalek, S.A., Yang, G., Zhang, L., Marinov, D., Khurshid, S., TestEra: A tool for testing Java programs using alloy specifications (2011) ASE 2011, , IEEE
  • Khurshid, S., Marinov, D., TestEra: Specification-based testing of Java programs using sat (2004) Automated Software Engineering, 11 (4). , Springer
  • Koksal, A.S., Kuncak, V., Suter, P., Constraints as control (2012) POPL
  • Liskov, B., Guttag, J., (2000) Program Development in Java: Abstraction, Specification, and Object-oriented Design, , Addison-Wesley
  • Milicevic, A., Misailovic, S., Marinov, D., Khurshid, S., Korat: A tool for generating structurally complex test inputs (2007) ICSE 2007, , IEEE Press
  • Milicevic, A., Rayside, D., Yessenov, K., Jackson, D., Unifying execution of imperative and declarative code (2011) ICSE
  • Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T., Feedback-directed random test generation (2007) ICSE 2007, , IEEE
  • Rosner, N., López Pombo, C.G., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F., Parallel bounded verification of alloy models by transcoping (2013) VSTTE 2014, LNCS, , Springer
  • Samimi, H., Aung, E.D., Millstein, T.D., Falling back on executable specifications (2010) ECOOP
  • Siddiqui, J., Khurshid, S., An empirical study of structural constraint solving techniques (2009) ICFEM 2009, , LNCS, Springer
  • Uzuncaova, E., (2008) Efficient Specification-based Testing Using Incremental Techniques, , PhD thesis, UT@Austin
  • Uzuncaova, E., Khurshid, S., Constraint prioritization for efficient analysis of declarative models (2008) FM
  • Visser, W., Pəsəreanu, C., Khurshid, S., Test input generation with Java PathFinder (2004) ISSTA 2004, , ACM
  • Xie, T., Marinov, D., Notkin, D., Rostra: A framework for detecting redundant object-oriented unit tests (2004) ASE 2004, , IEEE
  • Zaeem, R.N., Khurshid, S., Contract-based data structure repair using Alloy (2010) ECOOP
  • The HyTeK Distribution Can Be Downloaded, , http://bonnie.exp.dc.uba.ar/hytek-oopsla.tar.gz
  • http://alloy.mit.edu/A4 - ACM SIGPLAN

Citas:

---------- APA ----------
Rosner, N., Bengolea, V., Ponzio, P., Khalek, S.A., Aguirre, N., Frias, M.F. & Khurshid, S. (2014) . Bounded exhaustive test input generation from hybrid invariants. 2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014, 655-674.
http://dx.doi.org/10.1145/2660193.2660232
---------- CHICAGO ----------
Rosner, N., Bengolea, V., Ponzio, P., Khalek, S.A., Aguirre, N., Frias, M.F., et al. "Bounded exhaustive test input generation from hybrid invariants" . 2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014 (2014) : 655-674.
http://dx.doi.org/10.1145/2660193.2660232
---------- MLA ----------
Rosner, N., Bengolea, V., Ponzio, P., Khalek, S.A., Aguirre, N., Frias, M.F., et al. "Bounded exhaustive test input generation from hybrid invariants" . 2014 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2014, 2014, pp. 655-674.
http://dx.doi.org/10.1145/2660193.2660232
---------- VANCOUVER ----------
Rosner, N., Bengolea, V., Ponzio, P., Khalek, S.A., Aguirre, N., Frias, M.F., et al. Bounded exhaustive test input generation from hybrid invariants. Proc Conf Object Orient Program Syst Lang Appl OOPSLA. 2014:655-674.
http://dx.doi.org/10.1145/2660193.2660232