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

Guardado en:
Detalles Bibliográficos
Autores principales: De Caso, G., Braberman, V., Garbervetsky, D., Uchitel, S.
Formato: CONF
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: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 todo:paper_02705257_v_n_p452_DeCaso
record_format dspace
spelling todo:paper_02705257_v_n_p452_DeCaso2023-10-03T15:14:31Z Validation of contracts using enabledness preserving finite state abstractions De Caso, G. Braberman, V. Garbervetsky, D. Uchitel, S. 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. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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, G.
Braberman, V.
Garbervetsky, D.
Uchitel, S.
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.
format CONF
author De Caso, G.
Braberman, V.
Garbervetsky, D.
Uchitel, S.
author_facet De Caso, G.
Braberman, V.
Garbervetsky, D.
Uchitel, S.
author_sort De Caso, G.
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
url http://hdl.handle.net/20.500.12110/paper_02705257_v_n_p452_DeCaso
work_keys_str_mv AT decasog validationofcontractsusingenablednesspreservingfinitestateabstractions
AT brabermanv validationofcontractsusingenablednesspreservingfinitestateabstractions
AT garbervetskyd validationofcontractsusingenablednesspreservingfinitestateabstractions
AT uchitels validationofcontractsusingenablednesspreservingfinitestateabstractions
_version_ 1807317342841995264

Ejemplares similares