Navegar

Colección

Datos Estadísticas

Artículo

De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S. "Automated abstractions for contract validation" (2012) IEEE Transactions on Software Engineering. 38(1):141-162
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:

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 difficult to understand if the specifications for the various operations fit together well. In this paper, we propose a novel technique for automatically constructing abstractions in the form of behavior models from pre/postcondition-based specifications. Abstraction techniques have been used successfully for addressing the complexity of formal artifacts in software engineering; however, the focus has been, up to now, on abstractions for verification. Our aim is abstraction for validation and hence, different and novel trade-offs between precision and tractability are required. More specifically, in this paper, we define and study enabledness-preserving abstractions, that is, models in which concrete states are grouped according to the set of operations that they enable. The abstraction results in a finite model that is intuitive to validate and which facilitates tracing back to the specification for debugging. The paper also reports on the application of the approach to two industrial strength protocol specifications in which concerns were identified. © 2006 IEEE.

Registro:

Documento: Artículo
Título:Automated abstractions for contract validation
Autor:De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S.
Filiación:Departamento de Computación, FCEyN, Ciudad Autónoma de Buenos Aires (C1428EGA), Intendente Güiraldes 2160, Argentina
Department of Computing, Imperial College, London, United Kingdom
Palabras clave:automated abstraction; Requirements/specifications; validation; Abstraction techniques; automated abstraction; Behavior model; Concrete state; Engineering activities; Finite model; Industrial strength; Novel techniques; Protocol specifications; Requirements/specifications; validation; Software engineering; Specifications; Abstracting
Año:2012
Volumen:38
Número:1
Página de inicio:141
Página de fin:162
DOI: http://dx.doi.org/10.1109/TSE.2010.98
Título revista:IEEE Transactions on Software Engineering
Título revista abreviado:IEEE Trans Software Eng
ISSN:00985589
CODEN:IESED
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v38_n1_p141_DeCaso

Referencias:

  • Polikarpova, N., Ciupa, I., Meyer, B., A comparative study of programmer-written and automatically inferred contracts (2009) Proc. 18th Int'l Symp. Software Testing and Analysis, pp. 93-104
  • Van, H.T., Van Lamsweerde, A., Massonet, P., Ponsard, C., Goal-oriented requirements animation (2004) Proceedings of the IEEE International Conference on Requirements Engineering, pp. 218-228. , Proceedings - 12th IEEE International Requirements Engineering Conference. RE 2004
  • Meyer, B., Applying design by contract (1992) Computer, 25 (10), pp. 40-51. , Oct
  • Rosenblum, D.S., A practical approach to programming with assertions (1995) IEEE Trans. Software Eng., 21 (1), pp. 19-31. , Jan
  • Grieskamp, W., Kicillof, N., Tillmann, N., Action machines: A framework for encoding and composing partial behaviors (2006) International Journal of Software Engineering and Knowledge Engineering, 16 (5), pp. 705-726. , DOI 10.1142/S0218194006002963, PII S0218194006002963
  • Letier, E., Kramer, J., Magee, J., Uchitel, S., Deriving event-based transition systems from goal-oriented requirements models (2008) Automated Software Eng. J., 15 (2), pp. 175-206
  • Whittle, J., Schumann, J., Generating statechart designs from scenarios (2000) Proc. Int'l Conf. Software Eng., pp. 314-323
  • Uribe, T., (1999) Abstraction-Based Deductive-Algorithmic Verification of Reactive Systems, , C.S. Dept University S. Stanford Univ., Dept. of Computer Science
  • DeLine, R., Fahndrich, M., Typestates for objects (2004) Proc. 18th European Conf. Object-Oriented Programming, , June
  • Clarke, E., Grumberg, O., Peled, D., (1999) Model Checking., , MIT Press
  • Esparza, J., Decidability of model checking for infinite-state concurrent systems (1997) Acta Informatica, 34 (2), pp. 85-107
  • De Caso, G., Braberman, V.A., Garbervetsky, D., Uchitel, S., Validation of contracts using enabledness preserving finite state abstractions (2009) Proc. 31st Int'l Conf. Software Eng., pp. 452-462
  • Barrett, C., Berezin, S., CVC lite: A new implementation of the cooperating validity checker (2004) Proc. 16th Int'l Conf. Computer Aided Verification, , July
  • Harel, D., StateCharts: A visual formalism for complex systems (1987) Science of Computer Programming, 8 (3), pp. 231-274. , DOI 10.1016/0167-6423(87)90035-9
  • Milner, R., (1980) A Calculus of Communicating Systems., , Springer-Verlag
  • Grieskamp, W., Kicillof, N., MacDonald, D., Nandan, A., Stobie, K., Wurden, F.L., Model-based quality assurance of windows protocol documentation (2008) Proc. Int'l Conf. Software Testing, Verification, and Validation, pp. 502-506
  • (2008) [MS-NNS]: .NET NegotiateStream Protocol Specification v2.0, , http://msdn.microsoft.com/en-us/library/cc236723.aspx, July
  • Linn, J., (1993) RFC1508: Generic Security Service Application Program Interface, , RFC Editor United States
  • (2009) [MS-WINSRA]: Windows Internet Naming Service (WINS) Replication and Autodiscovery Protocol Specification, , http://msdn.microsoft.com/en-us/library/dd304175, (PROT.13).aspx, May
  • Campbell, C., Grieskamp, W., Nachmanson, L., Schulte, W., Tillmann, N., Veanes, M., (2005) Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer, , Technical Report MSR-TR-2005-59, Microsoft Research May
  • Ball, T., Rajamani, S., The SLAM project: Debugging system software via static analysis (2002) Proc. 29th ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages
  • Sun, J., Dong, J., Design synthesis from interaction and state-based specifications (2006) IEEE Trans. Software Eng., 32 (6), pp. 349-369. , June
  • Liu, L., Meyer, B., Schoeller, B., Using contracts and boolean queries to improve the quality of automatic test generation (2007) Proc. First Int'l Conf. Tests and Proofs, 4454, pp. 114-130
  • Graf, S., Saidi, H., Construction of abstract state graphs with PVS (1997) Proc. Ninth Int'l Conf. Computer Aided Verification, (1254), pp. 72-83. , Computer Aided Verification
  • Leuschel, M., Butler, M., ProB: An automated analysis toolset for the B method (2008) International Journal on Software Tools for Technology Transfer, 10 (2), pp. 185-203. , DOI 10.1007/s10009-007-0063-9
  • Nebut, C., Fleurey, F., Le Traon, Y., Jézéquel, J., Automatic test generation: A use case driven approach (2006) IEEE Trans. Software Eng., 32 (3), pp. 140-155. , Mar
  • Lee David, Yannakakis Mihalis, Online minimization of transition systems (1992) Conference Proceedings of the Annual ACM Symposium on Theory of Computing, pp. 264-274
  • Tripakis, S., Yovine, S., Analysis of timed systems using time-abstracting bisimulations (2001) Formal Methods in System Design, 18 (1), pp. 25-68. , DOI 10.1023/A:1008734703554
  • Strom, R.E., Yemini, S., Typestate: A programming language concept for enhancing software reliability (1986) IEEE Transactions on Software Engineering, SE-12 (1), pp. 157-171
  • DeLine, R., Fahndrich, M., Enforcing high-level protocols in low-level software (2001) Proc. ACM SIGPLAN, pp. 59-69
  • Alur, R., Ĉerný, P., Madhusudan, P., Nam, W., Synthesis of interface specifications for java classes (2005) Proc. 32nd ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, pp. 98-109
  • Giannakopoulou, D., Pásáreanu, C., Interface generation and compositional verification in javapathfinder (2009) Proc. 12th Int'l Conf. Fundamental Approaches to Software Eng.: Held as Part of the Joint European Conf. Theory and Practice of Software, pp. 94-108
  • Henzinger, T.A., Jhala, R., Majumdar, R., Permissive interfaces (2005) ESEC/FSE'05 - Proceedings of the Joint 10th European Software Engineering Conference (ESEC) and 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-13), pp. 31-40. , ESEC/FSE'05 - Proceedings of the Joint 10th European Software Engineering Conference (ESEC) and 13th ACM SIGSOFT Symposium on the Foundations of Software Engineering (FSE-13)
  • Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C., The Daikon system for dynamic detection of likely invariants (2007) Science of Computer Programming, 69 (1-3), pp. 35-45. , DOI 10.1016/j.scico.2007.01.015, PII S016764230700161X, Experimental Software and Toolkits
  • Gabel, M., Su, Z., Symbolic mining of temporal specifications (2008) Proc. 13th Int'l Conf. Software Eng., pp. 51-60
  • Dallmeier, V., Lindig, C., Wasylkowski, A., Zeller, A., Mining object behavior with ADABU (2006) Proc. Int'l workshop Dynamic Systems Analysis
  • Ghezzi, C., Mocci, A., Monga, M., Synthesizing intensional behavior models by graph transformation (2009) Proc. IEEE 31st Int'l Conf. Software Eng., pp. 430-440
  • Lorenzoli, D., Mariani, L., Pezzè, M., Automatic generation of software behavioral models (2008) Proc. 30th Int'l Conf. Software Eng., pp. 501-510

Citas:

---------- APA ----------
De Caso, G., Braberman, V., Garbervetsky, D. & Uchitel, S. (2012) . Automated abstractions for contract validation. IEEE Transactions on Software Engineering, 38(1), 141-162.
http://dx.doi.org/10.1109/TSE.2010.98
---------- CHICAGO ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. "Automated abstractions for contract validation" . IEEE Transactions on Software Engineering 38, no. 1 (2012) : 141-162.
http://dx.doi.org/10.1109/TSE.2010.98
---------- MLA ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. "Automated abstractions for contract validation" . IEEE Transactions on Software Engineering, vol. 38, no. 1, 2012, pp. 141-162.
http://dx.doi.org/10.1109/TSE.2010.98
---------- VANCOUVER ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. Automated abstractions for contract validation. IEEE Trans Software Eng. 2012;38(1):141-162.
http://dx.doi.org/10.1109/TSE.2010.98