Validation of contracts using enabledness preserving finite state abstractions

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 th...

Descripción completa

Detalles Bibliográficos
Autores principales: de Caso, Guido, Braberman, Víctor Adrián, Garbervetsky, Diego
Publicado: 2009
Materias:
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
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p452_DeCaso
http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p452_DeCaso
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_02705257_v_n_p452_DeCaso
record_format dspace
spelling paper:paper_02705257_v_n_p452_DeCaso2023-06-08T15:24:40Z Validation of contracts using enabledness preserving finite state abstractions de Caso, Guido Braberman, Víctor Adrián Garbervetsky, Diego 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 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. Fil:De Caso, G. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Garbervetsky, D. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2009 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p452_DeCaso http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p452_DeCaso
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic 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
spellingShingle 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
de Caso, Guido
Braberman, Víctor Adrián
Garbervetsky, Diego
Validation of contracts using enabledness preserving finite state abstractions
topic_facet 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
description 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.
author de Caso, Guido
Braberman, Víctor Adrián
Garbervetsky, Diego
author_facet de Caso, Guido
Braberman, Víctor Adrián
Garbervetsky, Diego
author_sort de Caso, Guido
title Validation of contracts using enabledness preserving finite state abstractions
title_short Validation of contracts using enabledness preserving finite state abstractions
title_full Validation of contracts using enabledness preserving finite state abstractions
title_fullStr Validation of contracts using enabledness preserving finite state abstractions
title_full_unstemmed Validation of contracts using enabledness preserving finite state abstractions
title_sort validation of contracts using enabledness preserving finite state abstractions
publishDate 2009
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02705257_v_n_p452_DeCaso
http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p452_DeCaso
work_keys_str_mv AT decasoguido validationofcontractsusingenablednesspreservingfinitestateabstractions
AT brabermanvictoradrian validationofcontractsusingenablednesspreservingfinitestateabstractions
AT garbervetskydiego validationofcontractsusingenablednesspreservingfinitestateabstractions
_version_ 1768542125176127488

Ejemplares similares