Automated abstractions for contract validation

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

Descripción completa

Guardado en:

Detalles Bibliográficos
Autores principales:	de Caso, Guido, Braberman, Víctor Adrián, Garbervetsky, Diego
Publicado:	2012
Materias:	automated abstraction Requirements/specifications validation Abstraction techniques Behavior model Concrete state Engineering activities Finite model Industrial strength Novel techniques Protocol specifications Software engineering Specifications Abstracting
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v38_n1_p141_DeCaso http://hdl.handle.net/20.500.12110/paper_00985589_v38_n1_p141_DeCaso
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_00985589_v38_n1_p141_DeCaso
record_format	dspace
spelling	paper:paper_00985589_v38_n1_p141_DeCaso2023-06-08T15:09:56Z Automated abstractions for contract validation de Caso, Guido Braberman, Víctor Adrián Garbervetsky, Diego 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 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. 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. 2012 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v38_n1_p141_DeCaso http://hdl.handle.net/20.500.12110/paper_00985589_v38_n1_p141_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	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
spellingShingle	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 de Caso, Guido Braberman, Víctor Adrián Garbervetsky, Diego Automated abstractions for contract validation
topic_facet	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
description	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.
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	Automated abstractions for contract validation
title_short	Automated abstractions for contract validation
title_full	Automated abstractions for contract validation
title_fullStr	Automated abstractions for contract validation
title_full_unstemmed	Automated abstractions for contract validation
title_sort	automated abstractions for contract validation
publishDate	2012
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v38_n1_p141_DeCaso http://hdl.handle.net/20.500.12110/paper_00985589_v38_n1_p141_DeCaso
work_keys_str_mv	AT decasoguido automatedabstractionsforcontractvalidation AT brabermanvictoradrian automatedabstractionsforcontractvalidation AT garbervetskydiego automatedabstractionsforcontractvalidation
_version_	1768545504037175296

Automated abstractions for contract validation

Ejemplares similares