Navegar

Colección

Datos Estadísticas

Conferencia

De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S. "Validation of contracts using enabledness preserving finite state abstractions" (2009) 2009 31st International Conference on Software Engineering, ICSE 2009:452-462
La versión final de este artículo es de uso interno de la institución.
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Pre/post condition-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 behaviour models from pre/post condition-based specifications. The level of abstraction at which such models are constructed preserves enabledness of sets of operations, resulting 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 an industrial strength protocol specification in which concerns were identified. © 2009 IEEE.

Registro:

Documento: Conferencia
Título:Validation of contracts using enabledness preserving finite state abstractions
Autor:De Caso, G.; Braberman, V.; Garbervetsky, D.; Uchitel, S.
Ciudad:Vancouver, BC
Filiación:Departamento de Computación, FCEyN, UBA, Buenos Aires, Argentina
Department of Computing, Imperial College, London, United Kingdom
Palabras clave:Based specification; Behaviour models; Finite model; Finite-state abstraction; Industrial strength; Level of abstraction; Novel techniques; Pre/post conditions; Protocol specifications; Abstracting; Computer software; Specifications
Año:2009
Página de inicio:452
Página de fin:462
DOI: http://dx.doi.org/10.1109/ICSE.2009.5070544
Título revista:2009 31st International Conference on Software Engineering, ICSE 2009
Título revista abreviado:Proc Int Conf Software Eng
ISSN:02705257
CODEN:PCSED
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p452_DeCaso

Referencias:

  • MS-NNS]: .NET NegotiateStream Protocol Specification v2.0, , http://msdn.microsoft.com/enus/library/cc236723.aspx, July 2008
  • Alur, R., Černỳ, 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 languages, pp. 98-109
  • Ball, T., Rajamani, S., The SLAM project: Debugging system software via static analysis (2002) Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages
  • 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), , July, Boston, Massachusetts
  • DeLine, R., Fahndrich, M., Typestates for Objects (2004); 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
  • Gabel, M., Su, Z., Symbolic mining of temporal specifications (2008) Proceedings of the 13th international conference on Software engineering, pp. 51-60
  • Grieskamp, W., Kicillof, N., MacDonald, D., Nandan, A., Stobie, K., Wurden, F.L., Model-based quality assurance of Windows protocol documentation (2008) ICST, pp. 502-506. , IEEE Computer Society
  • 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
  • Lee, D., Yannakakis, M., Online minimization of transition systems (extended abstract) (1992) Proceedings of the twenty-fourth annual ACM symposium on Theory of computing, pp. 264-274
  • Letier, E., Kramer, J., Magee, J., Uchitel, S., Deriving event-based transition systems from goal-oriented requirements models (2008) Automated Software Engineering Journal, 15 (2), pp. 175-206
  • Leuschel, M., Butler, M., ProB: An automated analysis toolset for the B method (2008) International Journal on Software Tools for Technology Transfer (STTT), 10 (2), pp. 185-203
  • Linn, J., RFC1508: Generic Security Service Application Program Interface (1993) RFC Editor United States
  • Meyer, B., Applying design by contract (1992) Computer, 25 (10), pp. 40-51
  • Nebut, C., Fleurey, F., Le Traon, Y., Jézéquel, J., Automatic Test Generation: A Use Case Driven Approach (2006) IEEE TSE, pp. 140-155
  • Polikarpova, N., Ciupa, I., Meyer, B., A comparative study of programmer-written and automatically inferred contracts (2008) month, 9 (608), p. 11
  • Rosenblum, D.S., A practical approach to programming with assertions (1995) IEEE Transactions on Software Engineering, 21 (1), pp. 19-31
  • Sun, J., Dong, J., Design Synthesis from Interaction and State-Based Specifications (2006) IEEE TSE
  • Tripakis, S., Yovine, S., Analysis of Timed Systems Using Time-Abstracting Bisimulations (2001) Formal Methods in System Design, 18 (1), pp. 25-68
  • T. Uribe, C. S. Dept, and S. University. Abstraction-based Deductive-algorithmic Verification of Reactive Systems. Stanford University, Dept. of Computer Science, 1999; Van, H., van Lamsweerde, A., Massonet, P., Ponsard, C., Goal-oriented requirements animation (2004) Requirements Engineering Conference, 2004, pp. 218-228
  • Whittle, J., Schumann, J., Generating Statechart Designs from Scenarios (2000) ICSE'00, pp. 314-323A4 - ACM - Association for Computing Machinery; IEEE; IEEE Computer Society; SIGSOFT - Special Interest Group on Software Engineering

Citas:

---------- APA ----------
De Caso, G., Braberman, V., Garbervetsky, D. & Uchitel, S. (2009) . Validation of contracts using enabledness preserving finite state abstractions. 2009 31st International Conference on Software Engineering, ICSE 2009, 452-462.
http://dx.doi.org/10.1109/ICSE.2009.5070544
---------- CHICAGO ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. "Validation of contracts using enabledness preserving finite state abstractions" . 2009 31st International Conference on Software Engineering, ICSE 2009 (2009) : 452-462.
http://dx.doi.org/10.1109/ICSE.2009.5070544
---------- MLA ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. "Validation of contracts using enabledness preserving finite state abstractions" . 2009 31st International Conference on Software Engineering, ICSE 2009, 2009, pp. 452-462.
http://dx.doi.org/10.1109/ICSE.2009.5070544
---------- VANCOUVER ----------
De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S. Validation of contracts using enabledness preserving finite state abstractions. Proc Int Conf Software Eng. 2009:452-462.
http://dx.doi.org/10.1109/ICSE.2009.5070544