Abstract:
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.
Registro:
Documento: |
Artículo
|
Título: | ParAlloy: Towards a framework for efficient parallel analysis of alloy models |
Autor: | Rosner, N.; Galeotti, J.P.; Lopez Pombo, C.G.; Frias, M.F. |
Ciudad: | Orford, QC |
Filiación: | Department of Computer Science, FCEyN, Universidad de Buenos Aires, Argentina
|
Palabras clave: | Alloy analyzers; Data domains; Model analysis; Parallel analysis; Propositional formulas; Relational modeling; SAT solvers; SAT-solving; Abstracting; Alloys; Contour followers; Cerium alloys |
Año: | 2010
|
Volumen: | 5977 LNCS
|
Página de inicio: | 396
|
Página de fin: | 397
|
DOI: |
http://dx.doi.org/10.1007/978-3-642-11811-1_33 |
Título revista: | 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010
|
Título revista abreviado: | Lect. Notes Comput. Sci.
|
ISSN: | 03029743
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5977LNCS_n_p396_Rosner |
Referencias:
- Andersen, H.R., Hulgaard, H., Boolean expression diagrams (2002) Information and Computation, 179 (2), pp. 194-212
- Eén, N., Sörensson, N., An extensible sat solver (2004) LNCS, 2919, pp. 502-518. , Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. Springer, Heidelberg
- Jackson, D., Alloy: A lightweight object modelling notation (2002) ACM Transactions on Software Engineering and Methodology, 11 (2), pp. 256-290
- Jackson, D., (2002) A Micromodels of Software: Lightweight Modelling and Analysis with Alloy., , Computer Science and Artificial Intelligence Laboratory. MIT, Cambridge
- Snir, M., Otto, S., Huss-Lederman, S., Walker, D., Dongarra, J., (1998) MPI: The Complete Reference, , MIT Press, Cambridge
- Zave, P., Compositional binding in network domains (2006) LNCS, 4085, pp. 332-347. , Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. Springer, Heidelberg
Citas:
---------- APA ----------
Rosner, N., Galeotti, J.P., Lopez Pombo, C.G. & Frias, M.F.
(2010)
. ParAlloy: Towards a framework for efficient parallel analysis of alloy models. 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010, 5977 LNCS, 396-397.
http://dx.doi.org/10.1007/978-3-642-11811-1_33---------- CHICAGO ----------
Rosner, N., Galeotti, J.P., Lopez Pombo, C.G., Frias, M.F.
"ParAlloy: Towards a framework for efficient parallel analysis of alloy models"
. 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010 5977 LNCS
(2010) : 396-397.
http://dx.doi.org/10.1007/978-3-642-11811-1_33---------- MLA ----------
Rosner, N., Galeotti, J.P., Lopez Pombo, C.G., Frias, M.F.
"ParAlloy: Towards a framework for efficient parallel analysis of alloy models"
. 2nd International Conference on Abstract State Machines, Alloy, B and Z, ABZ 2010, vol. 5977 LNCS, 2010, pp. 396-397.
http://dx.doi.org/10.1007/978-3-642-11811-1_33---------- VANCOUVER ----------
Rosner, N., Galeotti, J.P., Lopez Pombo, C.G., Frias, M.F. ParAlloy: Towards a framework for efficient parallel analysis of alloy models. Lect. Notes Comput. Sci. 2010;5977 LNCS:396-397.
http://dx.doi.org/10.1007/978-3-642-11811-1_33