Describing and analyzing behaviours over tabular specifications using (Dyn)alloy

Mostrar todas las versiones(3)

We propose complementing tabular notations used in requirements specifications, such as those used in the SCR method, with a formalism for describing specific, useful, subclasses of computations, i.e., particular combinations of the atomic transitions specified within tables. This provides the speci...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Aguirre, N.M., Frias, M.F., Moscato, M.M., Maibaum, T.S.E., Wassyng, A.
Formato: Artículo publishedVersion
Lenguaje:Inglés
Publicado: 2009
Materias:
Atomic transition
Autopilot systems
Dynamic logic
Example based
Operational languages
Requirements specifications
SAT-solving
Tabular expressions
Tabular notation
Tabular specifications
Test harness
Alloy languages
Computer software
Linguistics
Specifications
Cerium alloys
Software engineering
Acceso en línea:http://hdl.handle.net/20.500.12110/paper_03029743_v5503_n_p155_Aguirre
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paperaa:paper_03029743_v5503_n_p155_Aguirre
record_format dspace
spelling paperaa:paper_03029743_v5503_n_p155_Aguirre2023-06-12T16:47:19Z Describing and analyzing behaviours over tabular specifications using (Dyn)alloy Lect. Notes Comput. Sci. 2009;5503:155-170 Aguirre, N.M. Frias, M.F. Moscato, M.M. Maibaum, T.S.E. Wassyng, A. Atomic transition Autopilot systems Dynamic logic Example based Operational languages Requirements specifications SAT-solving Tabular expressions Tabular notation Tabular specifications Test harness Alloy languages Atomic transition Autopilot systems Operational languages Requirements specifications Tabular expressions Tabular notation Tabular specifications Computer software Linguistics Specifications Specifications Cerium alloys Software engineering We propose complementing tabular notations used in requirements specifications, such as those used in the SCR method, with a formalism for describing specific, useful, subclasses of computations, i.e., particular combinations of the atomic transitions specified within tables. This provides the specifier with the ability of driving the execution of transitions specified by tables, without the onerous burden of having to introduce modifications into the tabular expressions; thus, it avoids the problem of modifying the object of analysis, which would make the analysis indirect and potentially confusing. This is useful for a number of activities, such as defining test harnesses for tables, and concentrating the analyses on particular, interesting, subsets of computations. Unlike previous approaches, ours allows for the description of a wider class of combinations of the transitions defined by tables, by means of a rich operational language. This language is an extension of the Alloy language, called DynAlloy, whose notation is inspired by that of dynamic logic. The use of DynAlloy enables us to provide an extra mechanism for the analysis of tabular specifications, based on SAT solving. We will illustrate this and the features of our approach via an example based on a known tabular specification of a simple autopilot system. Fil:Frias, M.F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2009 info:eu-repo/semantics/article info:ar-repo/semantics/artículo info:eu-repo/semantics/publishedVersion application/pdf eng info:eu-repo/semantics/openAccess http://creativecommons.org/licenses/by/2.5/ar http://hdl.handle.net/20.500.12110/paper_03029743_v5503_n_p155_Aguirre
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Inglés
orig_language_str_mv eng
topic Atomic transition
Autopilot systems
Dynamic logic
Example based
Operational languages
Requirements specifications
SAT-solving
Tabular expressions
Tabular notation
Tabular specifications
Test harness
Alloy languages
Atomic transition
Autopilot systems
Operational languages
Requirements specifications
Tabular expressions
Tabular notation
Tabular specifications
Computer software
Linguistics
Specifications
Specifications
Cerium alloys
Software engineering
spellingShingle Atomic transition
Autopilot systems
Dynamic logic
Example based
Operational languages
Requirements specifications
SAT-solving
Tabular expressions
Tabular notation
Tabular specifications
Test harness
Alloy languages
Atomic transition
Autopilot systems
Operational languages
Requirements specifications
Tabular expressions
Tabular notation
Tabular specifications
Computer software
Linguistics
Specifications
Specifications
Cerium alloys
Software engineering
Aguirre, N.M.
Frias, M.F.
Moscato, M.M.
Maibaum, T.S.E.
Wassyng, A.
Describing and analyzing behaviours over tabular specifications using (Dyn)alloy
topic_facet Atomic transition
Autopilot systems
Dynamic logic
Example based
Operational languages
Requirements specifications
SAT-solving
Tabular expressions
Tabular notation
Tabular specifications
Test harness
Alloy languages
Atomic transition
Autopilot systems
Operational languages
Requirements specifications
Tabular expressions
Tabular notation
Tabular specifications
Computer software
Linguistics
Specifications
Specifications
Cerium alloys
Software engineering
description We propose complementing tabular notations used in requirements specifications, such as those used in the SCR method, with a formalism for describing specific, useful, subclasses of computations, i.e., particular combinations of the atomic transitions specified within tables. This provides the specifier with the ability of driving the execution of transitions specified by tables, without the onerous burden of having to introduce modifications into the tabular expressions; thus, it avoids the problem of modifying the object of analysis, which would make the analysis indirect and potentially confusing. This is useful for a number of activities, such as defining test harnesses for tables, and concentrating the analyses on particular, interesting, subsets of computations. Unlike previous approaches, ours allows for the description of a wider class of combinations of the transitions defined by tables, by means of a rich operational language. This language is an extension of the Alloy language, called DynAlloy, whose notation is inspired by that of dynamic logic. The use of DynAlloy enables us to provide an extra mechanism for the analysis of tabular specifications, based on SAT solving. We will illustrate this and the features of our approach via an example based on a known tabular specification of a simple autopilot system.
format Artículo
Artículo
publishedVersion
author Aguirre, N.M.
Frias, M.F.
Moscato, M.M.
Maibaum, T.S.E.
Wassyng, A.
author_facet Aguirre, N.M.
Frias, M.F.
Moscato, M.M.
Maibaum, T.S.E.
Wassyng, A.
author_sort Aguirre, N.M.
title Describing and analyzing behaviours over tabular specifications using (Dyn)alloy
title_short Describing and analyzing behaviours over tabular specifications using (Dyn)alloy
title_full Describing and analyzing behaviours over tabular specifications using (Dyn)alloy
title_fullStr Describing and analyzing behaviours over tabular specifications using (Dyn)alloy
title_full_unstemmed Describing and analyzing behaviours over tabular specifications using (Dyn)alloy
title_sort describing and analyzing behaviours over tabular specifications using (dyn)alloy
publishDate 2009
url http://hdl.handle.net/20.500.12110/paper_03029743_v5503_n_p155_Aguirre
work_keys_str_mv AT aguirrenm describingandanalyzingbehavioursovertabularspecificationsusingdynalloy
AT friasmf describingandanalyzingbehavioursovertabularspecificationsusingdynalloy
AT moscatomm describingandanalyzingbehavioursovertabularspecificationsusingdynalloy
AT maibaumtse describingandanalyzingbehavioursovertabularspecificationsusingdynalloy
AT wassynga describingandanalyzingbehavioursovertabularspecificationsusingdynalloy
_version_ 1769810232190435328

Ejemplares similares