Parallel bounded verification of alloy models by tranScoping

Bounded verification is a technique associated with the Alloy specification language that allows one to analyze Alloy software models by looking for counterexamples of intended properties, under the assumption that data type domains are restricted in size by a provided bound (called the scope of the...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autores principales: Rosner, Nicolás, Frias, Marcelo
Publicado: 2014
Materias:
Alloy Analyzer
Bounded verification
Parallel analysis
Parallel SAT-solving
Alloys
Decision making
Specification languages
Alloy analyzers
Analysis problems
Boolean satisfiability problems
Bounded verifications
Novel techniques
Parallelizations
SAT-solving
Verification
Acceso en línea:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8164_n_p88_Rosner
http://hdl.handle.net/20.500.12110/paper_03029743_v8164_n_p88_Rosner
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id paper:paper_03029743_v8164_n_p88_Rosner
record_format dspace
spelling paper:paper_03029743_v8164_n_p88_Rosner2023-06-08T15:28:50Z Parallel bounded verification of alloy models by tranScoping Rosner, Nicolás Frias, Marcelo Alloy Analyzer Bounded verification Parallel analysis Parallel SAT-solving Alloys Decision making Specification languages Alloy analyzers Analysis problems Boolean satisfiability problems Bounded verifications Novel techniques Parallel analysis Parallelizations SAT-solving Verification Bounded verification is a technique associated with the Alloy specification language that allows one to analyze Alloy software models by looking for counterexamples of intended properties, under the assumption that data type domains are restricted in size by a provided bound (called the scope of the analysis). The absence of errors in the analyzed models is relative to the provided scope, so achieving verifiability in larger scopes is necessary in order to provide higher confidence in model correctness. Unfortunately, analysis time usually grows exponentially as the scope is increased. A technique that helps in scaling up bounded verification is parallelization. However, the performance of parallel bounded verification greatly depends on the particular strategy used for partitioning the original analysis problem, which in the context of Alloy is a boolean satisfiability problem. In this article we present a novel technique called tranScoping, which aims at improving the scalability of bounded exhaustive analysis by using information mined at smaller scopes to guide decision making at larger ones. In its application to parallel analysis, tranScoping compares different ways to split an Alloy-borne SAT problem at small scopes, and extrapolates this information to select an adequate partitioning criterion for larger scopes. As our experiments show, tranScoping allows us to find suitable criteria that extend the tractability barrier, and in particular leads to successful analysis of models on scopes that have been elusive for years. © Springer-Verlag Berlin Heidelberg 2014. Fil:Rosner, N. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Fil:Frias, M.F. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2014 https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8164_n_p88_Rosner http://hdl.handle.net/20.500.12110/paper_03029743_v8164_n_p88_Rosner
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
topic Alloy Analyzer
Bounded verification
Parallel analysis
Parallel SAT-solving
Alloys
Decision making
Specification languages
Alloy analyzers
Analysis problems
Boolean satisfiability problems
Bounded verifications
Novel techniques
Parallel analysis
Parallelizations
SAT-solving
Verification
spellingShingle Alloy Analyzer
Bounded verification
Parallel analysis
Parallel SAT-solving
Alloys
Decision making
Specification languages
Alloy analyzers
Analysis problems
Boolean satisfiability problems
Bounded verifications
Novel techniques
Parallel analysis
Parallelizations
SAT-solving
Verification
Rosner, Nicolás
Frias, Marcelo
Parallel bounded verification of alloy models by tranScoping
topic_facet Alloy Analyzer
Bounded verification
Parallel analysis
Parallel SAT-solving
Alloys
Decision making
Specification languages
Alloy analyzers
Analysis problems
Boolean satisfiability problems
Bounded verifications
Novel techniques
Parallel analysis
Parallelizations
SAT-solving
Verification
description Bounded verification is a technique associated with the Alloy specification language that allows one to analyze Alloy software models by looking for counterexamples of intended properties, under the assumption that data type domains are restricted in size by a provided bound (called the scope of the analysis). The absence of errors in the analyzed models is relative to the provided scope, so achieving verifiability in larger scopes is necessary in order to provide higher confidence in model correctness. Unfortunately, analysis time usually grows exponentially as the scope is increased. A technique that helps in scaling up bounded verification is parallelization. However, the performance of parallel bounded verification greatly depends on the particular strategy used for partitioning the original analysis problem, which in the context of Alloy is a boolean satisfiability problem. In this article we present a novel technique called tranScoping, which aims at improving the scalability of bounded exhaustive analysis by using information mined at smaller scopes to guide decision making at larger ones. In its application to parallel analysis, tranScoping compares different ways to split an Alloy-borne SAT problem at small scopes, and extrapolates this information to select an adequate partitioning criterion for larger scopes. As our experiments show, tranScoping allows us to find suitable criteria that extend the tractability barrier, and in particular leads to successful analysis of models on scopes that have been elusive for years. © Springer-Verlag Berlin Heidelberg 2014.
author Rosner, Nicolás
Frias, Marcelo
author_facet Rosner, Nicolás
Frias, Marcelo
author_sort Rosner, Nicolás
title Parallel bounded verification of alloy models by tranScoping
title_short Parallel bounded verification of alloy models by tranScoping
title_full Parallel bounded verification of alloy models by tranScoping
title_fullStr Parallel bounded verification of alloy models by tranScoping
title_full_unstemmed Parallel bounded verification of alloy models by tranScoping
title_sort parallel bounded verification of alloy models by transcoping
publishDate 2014
url https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8164_n_p88_Rosner
http://hdl.handle.net/20.500.12110/paper_03029743_v8164_n_p88_Rosner
work_keys_str_mv AT rosnernicolas parallelboundedverificationofalloymodelsbytranscoping
AT friasmarcelo parallelboundedverificationofalloymodelsbytranscoping
_version_ 1768542363089633280

Ejemplares similares