Towards scaling up DynAlloy analysis using predicate abstraction

DynAlloy is an extension to the Alloy specifi cation language suitable for modeling properties of executions of software systems. DynAlloy provides fully automated support for verifying properties of programs, in the style of the Alloy Analyzer, i.e., by exhaustively searching for counterexamples of...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Ariño, Rodrigo, Degiovanni, Renzo, Fervari, Raul, Ponzio, Pablo Daniel, Aguirre, Nazareno Matías
Formato: Objeto de conferencia
Lenguaje:Español
Publicado: 2009
Materias:
Ciencias Informáticas
Software
Automation
Program analysis
Acceso en línea:http://sedici.unlp.edu.ar/handle/10915/21045
Aporte de:
SEDICI (UNLP) de Universidad Nacional de La Plata
id I19-R120-10915-21045
record_format dspace
institution Universidad Nacional de La Plata
institution_str I-19
repository_str R-120
collection SEDICI (UNLP)
language Español
topic Ciencias Informáticas
Software
Automation
Program analysis
spellingShingle Ciencias Informáticas
Software
Automation
Program analysis
Ariño, Rodrigo
Degiovanni, Renzo
Fervari, Raul
Ponzio, Pablo Daniel
Aguirre, Nazareno Matías
Towards scaling up DynAlloy analysis using predicate abstraction
topic_facet Ciencias Informáticas
Software
Automation
Program analysis
description DynAlloy is an extension to the Alloy specifi cation language suitable for modeling properties of executions of software systems. DynAlloy provides fully automated support for verifying properties of programs, in the style of the Alloy Analyzer, i.e., by exhaustively searching for counterexamples of properties in bounded scenarios (bounded domains and iterations of programs). But, as for other automated analysis techniques, the so called state explotion problem makes the analysis feasible only for small bounds. In this paper, we take advantage of an abstraction technique known as predicate abstraction, for scaling up the analysis of DynAlloy specifi cations. The implementation of predicate abstraction we present enables us to substantially increase the domain and iteration bounds in some case studies, and its use is fully automated. Our implementation is relatively e cient, exploiting the reuse of already calculated abstractions when these are available, and an "on the fly" check of traces when looking for counterexamples. We introduce the implementation of the technique, and some preliminary experimental results with case studies, to illustrate the benefi ts of the technique.
format Objeto de conferencia
Objeto de conferencia
author Ariño, Rodrigo
Degiovanni, Renzo
Fervari, Raul
Ponzio, Pablo Daniel
Aguirre, Nazareno Matías
author_facet Ariño, Rodrigo
Degiovanni, Renzo
Fervari, Raul
Ponzio, Pablo Daniel
Aguirre, Nazareno Matías
author_sort Ariño, Rodrigo
title Towards scaling up DynAlloy analysis using predicate abstraction
title_short Towards scaling up DynAlloy analysis using predicate abstraction
title_full Towards scaling up DynAlloy analysis using predicate abstraction
title_fullStr Towards scaling up DynAlloy analysis using predicate abstraction
title_full_unstemmed Towards scaling up DynAlloy analysis using predicate abstraction
title_sort towards scaling up dynalloy analysis using predicate abstraction
publishDate 2009
url http://sedici.unlp.edu.ar/handle/10915/21045
work_keys_str_mv AT arinorodrigo towardsscalingupdynalloyanalysisusingpredicateabstraction
AT degiovannirenzo towardsscalingupdynalloyanalysisusingpredicateabstraction
AT fervariraul towardsscalingupdynalloyanalysisusingpredicateabstraction
AT ponziopablodaniel towardsscalingupdynalloyanalysisusingpredicateabstraction
AT aguirrenazarenomatias towardsscalingupdynalloyanalysisusingpredicateabstraction
bdutipo_str Repositorios
_version_ 1764820465366335488

Ejemplares similares