ParAlloy: Towards a Framework for Efficient Parallel Analysis of Alloy Models

ROSNER, NICOLÁS; GALEOTTI, JUAN PABLO; LOPEZ POMBO, CARLOS GUSTAVO; FRIAS, MARCELO FABIAN

LECTURE NOTES IN COMPUTER SCIENCE

Springer

Lugar: Berlín; Año: 2010 vol. 5977 p. 396 - 397

0302-9743

Alloy [3] is a widely adopted relational modeling language. Its appealing syntax (which incorporates many constructs ubiquitous in object orientation), and the tool support provided by the Alloy Analyzer [2], make model analysis accessible to a public of non-specialists. Models are translated to propositional formulas, and off-the-shelf SAT-solvers are used to look for counterexamples of user-provided assertions. The translation strongly depends on user-provided bounds for data domains called scopes. The larger the scopes, the more confident the user is about the correctness of the model. It is often the case that analysis does not scale well enough to analyze models under the provided scopes. It is clear that model analysis based on SAT-solving has limitations due to the intrinsic complexity of the SAT-solving step. Therefore, appropriately splitting the SAT formula becomes a way of mastering the complexity of the analysis. This gives origin to ParAlloy, our framework for parallel SAT-solving using Alloy model information in the SAT-formula splitting process. Three important characteristics of ParAlloy are: 1. It makes a novel use of Boolean Expression Diagrams (BEDs) [1] to represent propositional formulas, allowing to produce, during the problem decomposi- tion stage, fewer subproblems than state-of-the-art parallel SAT-solvers also based on problem decomposition. 2. It decomposes formulas using knowledge obtained from the Alloy model un- der analysis, improving the (parallel) analyzability even further. 3. It allows to analyze nontrivial Alloy properties (as for instance some asser- tions in [4]) that exceed the current capabilities of the Alloy Analyzer.