TY - GEN
T1 - Parallel bounded verification of alloy models by tranScoping
AU - Rosner, Nicolás
AU - Pombo, Carlos Gustavo López
AU - Aguirre, Nazareno
AU - Jaoua, Ali
AU - Mili, Ali
AU - Frias, Marcelo F.
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2014.
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
KW - Alloy Analyzer
KW - Bounded verification
KW - Parallel SAT-solving
KW - Parallel analysis
UR - http://www.scopus.com/inward/record.url?scp=84927632787&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84927632787&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-54108-7_5
DO - 10.1007/978-3-642-54108-7_5
M3 - Conference contribution
AN - SCOPUS:84927632787
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 88
EP - 107
BT - Verified Software
A2 - Cohen, Ernie
A2 - Rybalchenko, Andrey
A2 - Rybalchenko, Andrey
PB - Springer Verlag
T2 - 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013
Y2 - 17 May 2013 through 19 May 2013
ER -