Navegar

Colección

Datos Estadísticas

Artículo

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) ACM SIGPLAN Notices. 49(10):655-674
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:

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. 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. Copyright © 2014 ACM.

Registro:

Documento: Artículo
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
CONICET, Rio Cuarto, Argentina
Dept. of Software Engineering, Instituto Tecnólogico de Buenos Aires, 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; Specifications; Automated test generations; Bounded exhaustive testing; Korat; SAT-solving; Transcoping; Software testing
Año:2014
Volumen:49
Número:10
Página de inicio:655
Página de fin:674
DOI: http://dx.doi.org/10.1145/2660193.2660232
Título revista:ACM SIGPLAN Notices
Título revista abreviado:ACM SIGPLAN Not.
ISSN:15232867
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_15232867_v49_n10_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 ICSE 2005
  • Galeotti, J.P., Rosner, N., Lopez 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 ICFEM 2012
  • 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 (2011) ASE, , (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
  • http://bonnie.exp.dc.uba.ar/hytek-oopsla.tar.gz, The HyTeK distribution can be downloaded from; http://alloy.mit.edu/

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. ACM SIGPLAN Notices, 49(10), 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" . ACM SIGPLAN Notices 49, no. 10 (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" . ACM SIGPLAN Notices, vol. 49, no. 10, 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. ACM SIGPLAN Not. 2014;49(10):655-674.
http://dx.doi.org/10.1145/2660193.2660232