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
Autores principales:	Asteasuain, F., Braberman, V.
Formato:	CONF
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:	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	todo:paper_18917062_v_n_p430_Asteasuain
record_format	dspace
spelling	todo:paper_18917062_v_n_p430_Asteasuain2023-10-03T16:34:25Z Specification patterns can be formal and still easy Asteasuain, F. Braberman, V. 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. CONF info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar 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 Asteasuain, F. Braberman, V. 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.
format	CONF
author	Asteasuain, F. Braberman, V.
author_facet	Asteasuain, F. Braberman, V.
author_sort	Asteasuain, F.
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
url	http://hdl.handle.net/20.500.12110/paper_18917062_v_n_p430_Asteasuain
work_keys_str_mv	AT asteasuainf specificationpatternscanbeformalandstilleasy AT brabermanv specificationpatternscanbeformalandstilleasy
_version_	1807315962406371328

Specification patterns can be formal and still easy

Ejemplares similares