Specification Patterns: Formal and Easy

Property specification is still one of the most challenging tasks for transference of software verification technology. 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 validatin...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Braberman, Víctor Adrián
Publicado: 2015
Materias:
Behavioral modeling
requirements engineering
specification patterns
Computational linguistics
Computer hardware description languages
Formal languages
Requirements engineering
Semantics
Specification languages
Verification
Visual languages
Behavioral model
Behavioral properties
Graphical languages
Pattern representation
Pattern specifications
Property Specification
Software verification
Specification patterns
Specifications
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02181940_v25_n4_p669_Asteasuain
http://hdl.handle.net/20.500.12110/paper_02181940_v25_n4_p669_Asteasuain
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_02181940_v25_n4_p669_Asteasuain
record_format dspace
spelling paper:paper_02181940_v25_n4_p669_Asteasuain2023-06-08T15:21:21Z Specification Patterns: Formal and Easy Braberman, Víctor Adrián Behavioral modeling requirements engineering specification patterns Computational linguistics Computer hardware description languages Formal languages Requirements engineering Semantics Specification languages Verification Visual languages Behavioral model Behavioral properties Graphical languages Pattern representation Pattern specifications Property Specification Software verification Specification patterns Specifications Property specification is still one of the most challenging tasks for transference of software verification technology. 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 desired property the developer may have to deal with the pattern representation in some particular formalism. For this reason, we identify four desirable quality attributes for the underlying specification language: succinctness, comparability, complementariness, and modifiability. We show that typical formalisms such as temporal logics or automata fail at some extent to support these features. Given this context we introduce Featherweight Visual Scenarios (FVS), a declarative and graphical language based on scenarios, as a possible alternative to specify behavioral properties. We illustrate FVS applicability by modeling all the specification patterns and we thoroughly compare FVS to other known approaches, showing that FVS specifications are better suited for validation tasks. In addition, we augment pattern specification by introducing the concept of violating behavior. Finally we characterize the type of properties that can be written in FVS and we formally introduce its syntax and semantics. © 2015 World Scientific Publishing Company. Fil:Braberman, V. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2015 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02181940_v25_n4_p669_Asteasuain http://hdl.handle.net/20.500.12110/paper_02181940_v25_n4_p669_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 modeling
requirements engineering
specification patterns
Computational linguistics
Computer hardware description languages
Formal languages
Requirements engineering
Semantics
Specification languages
Verification
Visual languages
Behavioral model
Behavioral properties
Graphical languages
Pattern representation
Pattern specifications
Property Specification
Software verification
Specification patterns
Specifications
spellingShingle Behavioral modeling
requirements engineering
specification patterns
Computational linguistics
Computer hardware description languages
Formal languages
Requirements engineering
Semantics
Specification languages
Verification
Visual languages
Behavioral model
Behavioral properties
Graphical languages
Pattern representation
Pattern specifications
Property Specification
Software verification
Specification patterns
Specifications
Braberman, Víctor Adrián
Specification Patterns: Formal and Easy
topic_facet Behavioral modeling
requirements engineering
specification patterns
Computational linguistics
Computer hardware description languages
Formal languages
Requirements engineering
Semantics
Specification languages
Verification
Visual languages
Behavioral model
Behavioral properties
Graphical languages
Pattern representation
Pattern specifications
Property Specification
Software verification
Specification patterns
Specifications
description Property specification is still one of the most challenging tasks for transference of software verification technology. 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 desired property the developer may have to deal with the pattern representation in some particular formalism. For this reason, we identify four desirable quality attributes for the underlying specification language: succinctness, comparability, complementariness, and modifiability. We show that typical formalisms such as temporal logics or automata fail at some extent to support these features. Given this context we introduce Featherweight Visual Scenarios (FVS), a declarative and graphical language based on scenarios, as a possible alternative to specify behavioral properties. We illustrate FVS applicability by modeling all the specification patterns and we thoroughly compare FVS to other known approaches, showing that FVS specifications are better suited for validation tasks. In addition, we augment pattern specification by introducing the concept of violating behavior. Finally we characterize the type of properties that can be written in FVS and we formally introduce its syntax and semantics. © 2015 World Scientific Publishing Company.
author Braberman, Víctor Adrián
author_facet Braberman, Víctor Adrián
author_sort Braberman, Víctor Adrián
title Specification Patterns: Formal and Easy
title_short Specification Patterns: Formal and Easy
title_full Specification Patterns: Formal and Easy
title_fullStr Specification Patterns: Formal and Easy
title_full_unstemmed Specification Patterns: Formal and Easy
title_sort specification patterns: formal and easy
publishDate 2015
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_02181940_v25_n4_p669_Asteasuain
http://hdl.handle.net/20.500.12110/paper_02181940_v25_n4_p669_Asteasuain
work_keys_str_mv AT brabermanvictoradrian specificationpatternsformalandeasy
_version_ 1768541935479291904

Ejemplares similares