Navegar

Colección

Datos Estadísticas

Artículo

De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S. "Abstractions for validation in action" (2012) 12th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2012. 7320 LNCS:192-218
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Many software engineering artefacts, such as source code or specifications, define a set of operations and impose restrictions to the ordering on which they have to be invoked. Enabledness Preserving Abstractions (EPAs) are concise representations of the behaviour space for such artefacts. In this paper, we exemplify how EPAs might be used for validation of software engineering artefacts by showing the use of EPAs to support some programming tasks on a simple C# class. © 2012 Springer-Verlag.

Registro:

Documento: Artículo
Título:Abstractions for validation in action
Autor:De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S.
Ciudad:Bertinoro
Filiación:Departamento de Computación, FCEyN, Universidad de Buenos Aires, Buenos Aires, Argentina
Department of Computing, Imperial College, London, United Kingdom
Palabras clave:Behaviour validation; enabledness-preserving abstractions; Behaviour validation; Concise representations; enabledness-preserving abstractions; Programming tasks; Source codes; Abstracting; Communication; Computer software; Design; Formal methods
Año:2012
Volumen:7320 LNCS
Página de inicio:192
Página de fin:218
DOI: http://dx.doi.org/10.1007/978-3-642-30982-3_6
Título revista:12th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2012
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7320LNCS_n_p192_DeCaso

Referencias:

  • Alur, R., Černý, P., Madhusudan, P., Nam, W., Synthesis of interface specifications for Java classes (2005) POPL 2005, pp. 98-109
  • Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Yovine, S., The algorithmic analysis of hybrid systems (1995) Theoretical Computer Science, 138 (1), pp. 3-34
  • Andersen, M., Barnett, M., Fahndrich, M., Grunkemeyer, B., King, K., Logozzo, F., Patel, V., Zuniga, D., (2009) Code Contracts, , http://research.microsoft.com/en-us/projects/contracts/
  • Beckman, N., Nori, A., Probabilistic, modular and scalable inference of typestate specifications (2011) PLDI
  • Beschastnikh, I., Brun, Y., Sloan, S., Ernst, M., Leveraging existing instrumentation to automatically infer invariant-constrained models (2011) FSE 2011
  • Beyer, D., Henzinger, T., Jhala, R., Majumdar, R., The software model checker Blast (2007) STTT, 9, pp. 505-525. , http://www.springerlink.com/index/10.1007/s10009-007-0044-z
  • Bierhoff, K., Aldrich, J., Plural: Checking protocol compliance under aliasing (2008) ICSE, pp. 971-972. , ACM
  • De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S., Automated abstractions for contract validation (2012) IEEE Transactions on Software Engineering, 38 (1), pp. 141-162
  • De Caso, G., Braberman, V.A., Garbervetsky, D., Uchitel, S., Program abstractions for behaviour validation (2011) Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu, HI, USA, May 21-28, pp. 381-390
  • Chalin, P., James, P.R., Non-null References by Default in Java: Alleviating the Nullity Annotation Burden (2007) LNCS, 4609, pp. 227-247. , Bateni, M. (ed.) ECOOP 2007. Springer, Heidelberg
  • Dallmeier, V., Lindig, C., Wasylkowski, A., Zeller, A., Mining object behavior with ADABU (2006) Workshop on Dynamic Systems Analysis 2006
  • Dallmeier, V., Knopp, N., Mallon, C., Hack, S., Zeller, A., Generating test cases for specification mining (2010) ISSTA 2010
  • DeLine, R., Fahndrich, M., Enforcing high-level protocols in low-level software (2001) PLDI 2001, pp. 59-69
  • Demsky, B., Rinard, M., Automatic extraction of heap reference properties in object-oriented programs (2009) IEEE Transactions on Software Engineering, 35, pp. 305-324
  • Ernst, M., Perkins, J., Guo, P., McCamant, S., Pacheco, C., Tschantz, M., Xiao, C., The Daikon system for dynamic detection of likely invariants (2007) Science of Computer Programming, 69, pp. 35-45. , http://linkinghub.elsevier.com/retrieve/pii/S016764230700161X
  • Esparza, J., Decidability of model checking for infinite-state concurrent systems (1997) Acta Informatica, 34, pp. 85-107. , http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/ s002360050074
  • Flanagan, C., Leino, K., Houdini, an Annotation Assistant for ESC/Java (2001) LNCS, 2021, pp. 500-517. , Oliveira, J.N., Zave, P. (eds.) FME 2001. Springer, Heidelberg
  • Gabel, M., Su, Z., Symbolic mining of temporal specifications (2008) ICSE 2008, pp. 51-60. , http://portal.acm.org/citation.cfm?id=1368096
  • Ghezzi, C., Mocci, A., Monga, M., Synthesizing intensional behavior models by graph transformation (2009) ICSE 2009, pp. 430-440
  • Giannakopoulou, D., Pǎsǎreanu, C.S., Interface Generation and Compositional Verification in JavaPathfinder (2009) LNCS, 5503, pp. 94-108. , Chechik, M., Wirsing, M. (eds.) FASE 2009. Springer, Heidelberg
  • Graf, S., Saïdi, H., Construction of Abstract State Graphs with PVS (1997) LNCS, 1254, pp. 72-83. , Grumberg, O. (ed.) CAV 1997. Springer, Heidelberg
  • Grieskamp, W., Kicillof, N., MacDonald, D., Nandan, A., Stobie, K., Wurden, F., Model-based quality assurance of Windows protocol documentation (2008) ICST 2008, pp. 502-506. , http://ieeexplore.ieee.org/lpdocs/epic03/wrapper.htm?arnumber=4539580
  • Heitmeyer, C.L., Jeffords, R.D., Labaw, B.G., Automated consistency checking of requirements specifications (1996) ACM Transactions on Software Engineering and Methodology (TOSEM), 5 (3), pp. 231-261
  • Henzinger, T., Jhala, R., Majumdar, R., Permissive interfaces (2005) ESEC/FSE 2005, pp. 31-40
  • (1990) IEEE Standard Glossary of Software Engineering Terminology, , IEEE: September
  • Kramer, J., Is abstraction the key to computing? (2007) Commun. ACM, 50, pp. 36-42. , http://doi.acm.org/10.1145/1232743.1232745
  • Kwiatkowska, M., Norman, G., Parker, D., PRISM 4.0: Verification of Probabilistic Real-Time Systems (2011) LNCS, 6806, pp. 585-591. , Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. Springer, Heidelberg
  • Lee, D., Yannakakis, M., Online minimization of transition systems (1992) STOC 1992, pp. 264-274. , http://portal.acm.org/citation.cfm?doid=129712.129738, (extended abstract)
  • Liu, L., Meyer, B., Schoeller, B., Using Contracts and Boolean Queries to Improve the Quality of Automatic Test Generation (2007) LNCS, 4454, pp. 114-130. , Gurevich, Y., Meyer, B. (eds.) TAP 2007. Springer, Heidelberg
  • Lorenzoli, D., Mariani, L., Pezzè, M., Automatic generation of software behavioral models (2008) ICSE 2008, pp. 501-510
  • Nanda, M., Grothoff, C., Chandra, S., Deriving object typestates in the presence of inter-object references (2005) ACM SIGPLAN Notices, 40 (10), pp. 77-96
  • Nipkow, T., Paulson, L.C., Wenzel, M., Isabelle/HOL - A Proof Assistant for Higher-Order Logic (2002) LNCS, 2283. , Springer, Heidelberg
  • Pradel, M., Gross, T.R., Automatic Generation of Object Usage Specifications from Large Method Traces (2009) ASE 2009, pp. 371-382. , http://ieeexplore.ieee.org/lpdocs/epic03/wrapper.htm?arnumber=5431756, IEEE November
  • Sasnauskas, R., Dustmann, O.S., Kaminski, B.L., Wehrle, K., Weise, C., Kowalewski, S., Scalable symbolic execution of distributed systems (2011) Proceedings of the 2011 31st International Conference on Distributed Computing Systems, ICDCS 2011, pp. 333-342. , http://dx.doi.org/10.1109/ICDCS.2011.28, IEEE Computer Society, Washington, DC
  • Strom, R., Yemini, S., Typestate: A programming language concept for enhancing software reliability (1986) IEEE TSE, 12 (1), pp. 157-171
  • Uribe, T., (1999) Abstraction-based Deductive-algorithmic Verification of Reactive Systems, , Stanford University, Dept. of Computer Science
  • Valmari, A., The State Explosion Problem (1998) LNCS, 1491, pp. 429-528. , Reisig, W., Rozenberg, G. (eds.) APN 1998. Springer, Heidelberg
  • 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 2011, pp. 44-47. , http://doi.acm.org/10.1145/1984708.1984721, ACM, New York

Citas:

---------- APA ----------
De Caso, G., Braberman, V., Garbervetsky, D. & Uchitel, S. (2012) . Abstractions for validation in action. 12th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2012, 7320 LNCS, 192-218.
http://dx.doi.org/10.1007/978-3-642-30982-3_6
---------- CHICAGO ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. "Abstractions for validation in action" . 12th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2012 7320 LNCS (2012) : 192-218.
http://dx.doi.org/10.1007/978-3-642-30982-3_6
---------- MLA ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. "Abstractions for validation in action" . 12th International School on Formal Methods for the Design of Computer, Communication and Software Systems, SFM 2012, vol. 7320 LNCS, 2012, pp. 192-218.
http://dx.doi.org/10.1007/978-3-642-30982-3_6
---------- VANCOUVER ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. Abstractions for validation in action. Lect. Notes Comput. Sci. 2012;7320 LNCS:192-218.
http://dx.doi.org/10.1007/978-3-642-30982-3_6