Specification patterns can be formal and still easy

Property specification is still one of the most challenging tasks for transference of software verification technology like model checking. The use of patterns has been proposed in order to hide the complicated handling of formal languages from the developer. However, this goal is not entirely satis...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Braberman, Víctor Adrián
Publicado:	2010
Materias:	Behavioral properties Modifiability Property Specification Quality attributes Response patterns Scenario-based languages Software verification Specification patterns Formal languages Knowledge engineering Software engineering Specification languages Specifications Model checking
Acceso en línea:	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_18917062_v_n_p430_Asteasuain http://hdl.handle.net/20.500.12110/paper_18917062_v_n_p430_Asteasuain
Aporte de:	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires

id	paper:paper_18917062_v_n_p430_Asteasuain
record_format	dspace
spelling	paper:paper_18917062_v_n_p430_Asteasuain2023-06-08T16:30:21Z Specification patterns can be formal and still easy Braberman, Víctor Adrián Behavioral properties Modifiability Property Specification Quality attributes Response patterns Scenario-based languages Software verification Specification patterns Formal languages Knowledge engineering Software engineering Specification languages Specifications Model checking Property specification is still one of the most challenging tasks for transference of software verification technology like model checking. The use of patterns has been proposed in order to hide the complicated handling of formal languages from the developer. However, this goal is not entirely satisfied. When validating the pattern the developer may have to deal with the pattern expressed in some particular formalism. For this reason, we identify three desirable quality attributes for the underlying specification language: succinctness, ease of validation and modifiability. We show that typical formalisms such as temporal logics or automata fail at some extent to support these features. In this work we propose FVS, a graphical scenario-based language, as a possible alternative to specify behavioral properties. We illustrate FVS' features by describing one of the most commonly used pattern, the Response Pattern, and several variants of it. Other known patterns such as the Precedence pattern and the Constrained Chain pattern are also discussed. We also thoroughly compare FVS against other used approaches. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2010 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_18917062_v_n_p430_Asteasuain http://hdl.handle.net/20.500.12110/paper_18917062_v_n_p430_Asteasuain
institution	Universidad de Buenos Aires
institution_str	I-28
repository_str	R-134
collection	Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic	Behavioral properties Modifiability Property Specification Quality attributes Response patterns Scenario-based languages Software verification Specification patterns Formal languages Knowledge engineering Software engineering Specification languages Specifications Model checking
spellingShingle	Behavioral properties Modifiability Property Specification Quality attributes Response patterns Scenario-based languages Software verification Specification patterns Formal languages Knowledge engineering Software engineering Specification languages Specifications Model checking Braberman, Víctor Adrián Specification patterns can be formal and still easy
topic_facet	Behavioral properties Modifiability Property Specification Quality attributes Response patterns Scenario-based languages Software verification Specification patterns Formal languages Knowledge engineering Software engineering Specification languages Specifications Model checking
description	Property specification is still one of the most challenging tasks for transference of software verification technology like model checking. The use of patterns has been proposed in order to hide the complicated handling of formal languages from the developer. However, this goal is not entirely satisfied. When validating the pattern the developer may have to deal with the pattern expressed in some particular formalism. For this reason, we identify three desirable quality attributes for the underlying specification language: succinctness, ease of validation and modifiability. We show that typical formalisms such as temporal logics or automata fail at some extent to support these features. In this work we propose FVS, a graphical scenario-based language, as a possible alternative to specify behavioral properties. We illustrate FVS' features by describing one of the most commonly used pattern, the Response Pattern, and several variants of it. Other known patterns such as the Precedence pattern and the Constrained Chain pattern are also discussed. We also thoroughly compare FVS against other used approaches.
author	Braberman, Víctor Adrián
author_facet	Braberman, Víctor Adrián
author_sort	Braberman, Víctor Adrián
title	Specification patterns can be formal and still easy
title_short	Specification patterns can be formal and still easy
title_full	Specification patterns can be formal and still easy
title_fullStr	Specification patterns can be formal and still easy
title_full_unstemmed	Specification patterns can be formal and still easy
title_sort	specification patterns can be formal and still easy
publishDate	2010
url	https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_18917062_v_n_p430_Asteasuain http://hdl.handle.net/20.500.12110/paper_18917062_v_n_p430_Asteasuain
work_keys_str_mv	AT brabermanvictoradrian specificationpatternscanbeformalandstilleasy
_version_	1768542055478329344

Specification patterns can be formal and still easy

Ejemplares similares