ParAlloy: Towards a framework for efficient parallel analysis of alloy models
Alloy [Jac02a] is a widely adopted relational modeling language. Its appealing syntax and the support provided by the Alloy Analyzer [Jac02b] tool make model analysis accessible to a public of non-specialists. A model and property are translated to a propositional formula, which is fed to a SAT-solv...
Guardado en:
| Autores principales: | , , , |
|---|---|
| Publicado: |
2010
|
| Materias: | |
| Acceso en línea: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p396_Rosner http://hdl.handle.net/20.500.12110/paper_03029743_v5977LNCS_n_p396_Rosner |
| Aporte de: |
| Sumario: | Alloy [Jac02a] is a widely adopted relational modeling language. Its appealing syntax and the support provided by the Alloy Analyzer [Jac02b] tool make model analysis accessible to a public of non-specialists. A model and property are translated to a propositional formula, which is fed to a SAT-solver to search for counterexamples. 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. Due to the intrinsic complexity of the SAT-solving step, it is often the case that analyses do not scale well enough to remain feasible as scopes grow. © 2010 Springer. |
|---|