DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour

"We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for t...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Regis, Germán, Cornejo, César, Gutiérrez Brida, Simón, Politano, Mariano, Raverta, Fernando, Ponzio, Pablo, Aguirre, Nazareno, Galeotti, Juan Pablo, Frías, Marcelo
Formato: Ponencias en Congresos acceptedVersion
Lenguaje:Inglés
Publicado: 2019
Materias:
ALLOY
VALIDACION DE SOFTWARE
RESPUESTA DINAMICA
LENGUAJES DE ESPECIFICACION
VERIFICACION DE SOFTWARE
Acceso en línea:http://ri.itba.edu.ar/handle/123456789/1764
Aporte de:
Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA) de Instituto Tecnológico de Buenos Aires (ITBA)
id I32-R138-123456789-1764
record_format dspace
spelling I32-R138-123456789-17642022-12-07T14:13:38Z DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour Regis, Germán Cornejo, César Gutiérrez Brida, Simón Politano, Mariano Raverta, Fernando Ponzio, Pablo Aguirre, Nazareno Galeotti, Juan Pablo Frías, Marcelo ALLOY VALIDACION DE SOFTWARE RESPUESTA DINAMICA LENGUAJES DE ESPECIFICACION VERIFICACION DE SOFTWARE "We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for the description of dynamic behaviours, understood as sequences of states over standard Alloy models, in terms of programs. The syntax is broad enough to accommodate abstract dynamic behaviours, e.g., using nondeterministic choice and finite unbounded iteration, as well as more concrete ones, using standard sequential programming constructions. The analysis of DynAlloy models resorts to the analysis of Alloy models, through an optimized translation that often makes the analysis more efficient than that of typical ad-hoc constructions to capture dynamism in Alloy." 2019-09-24T14:17:27Z 2019-09-24T14:17:27Z 2017-09 Ponencias en Congresos info:eu-repo/semantics/acceptedVersion 978-1450-351-05-8 http://ri.itba.edu.ar/handle/123456789/1764 en info:eu-repo/semantics/altIdentifier/doi/10.1145/3106237.3122826 application/pdf
institution Instituto Tecnológico de Buenos Aires (ITBA)
institution_str I-32
repository_str R-138
collection Repositorio Institucional Instituto Tecnológico de Buenos Aires (ITBA)
language Inglés
topic ALLOY
VALIDACION DE SOFTWARE
RESPUESTA DINAMICA
LENGUAJES DE ESPECIFICACION
VERIFICACION DE SOFTWARE
spellingShingle ALLOY
VALIDACION DE SOFTWARE
RESPUESTA DINAMICA
LENGUAJES DE ESPECIFICACION
VERIFICACION DE SOFTWARE
Regis, Germán
Cornejo, César
Gutiérrez Brida, Simón
Politano, Mariano
Raverta, Fernando
Ponzio, Pablo
Aguirre, Nazareno
Galeotti, Juan Pablo
Frías, Marcelo
DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
topic_facet ALLOY
VALIDACION DE SOFTWARE
RESPUESTA DINAMICA
LENGUAJES DE ESPECIFICACION
VERIFICACION DE SOFTWARE
description "We describe DynAlloy Analyzer, a tool that extends Alloy Analyzer with support for dynamic elements in Alloy models. The tool builds upon Alloy Analyzer in a way that makes it fully compatible with Alloy models, and extends their syntax with a particular idiom, inspired in dynamic logic, for the description of dynamic behaviours, understood as sequences of states over standard Alloy models, in terms of programs. The syntax is broad enough to accommodate abstract dynamic behaviours, e.g., using nondeterministic choice and finite unbounded iteration, as well as more concrete ones, using standard sequential programming constructions. The analysis of DynAlloy models resorts to the analysis of Alloy models, through an optimized translation that often makes the analysis more efficient than that of typical ad-hoc constructions to capture dynamism in Alloy."
format Ponencias en Congresos
acceptedVersion
author Regis, Germán
Cornejo, César
Gutiérrez Brida, Simón
Politano, Mariano
Raverta, Fernando
Ponzio, Pablo
Aguirre, Nazareno
Galeotti, Juan Pablo
Frías, Marcelo
author_facet Regis, Germán
Cornejo, César
Gutiérrez Brida, Simón
Politano, Mariano
Raverta, Fernando
Ponzio, Pablo
Aguirre, Nazareno
Galeotti, Juan Pablo
Frías, Marcelo
author_sort Regis, Germán
title DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
title_short DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
title_full DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
title_fullStr DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
title_full_unstemmed DynAlloy analyzer: a tool for the specification and analysis of Alloy models with dynamic behaviour
title_sort dynalloy analyzer: a tool for the specification and analysis of alloy models with dynamic behaviour
publishDate 2019
url http://ri.itba.edu.ar/handle/123456789/1764
work_keys_str_mv AT regisgerman dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
AT cornejocesar dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
AT gutierrezbridasimon dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
AT politanomariano dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
AT ravertafernando dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
AT ponziopablo dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
AT aguirrenazareno dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
AT galeottijuanpablo dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
AT friasmarcelo dynalloyanalyzeratoolforthespecificationandanalysisofalloymodelswithdynamicbehaviour
_version_ 1765660760660246528

Ejemplares similares