Artículo
Rosner, N.; Pombo, C.G.L.; Aguirre, N.; Jaoua, A.; Mili, A.; Frias, M.F.; Rybalchenko A.; Rybalchenko A.; Cohen E. "Parallel bounded verification of alloy models by tranScoping" (2014) 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013. 8164:88-107
Consulte la política de Acceso Abierto del editor
Abstract:
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.
Registro:
| Documento: | Artículo |
| Título: | Parallel bounded verification of alloy models by tranScoping |
| Autor: | Rosner, N.; Pombo, C.G.L.; Aguirre, N.; Jaoua, A.; Mili, A.; Frias, M.F.; Rybalchenko A.; Rybalchenko A.; Cohen E. |
| Filiación: | Department of Computer Science, FCEyN, Universidad de Buenos Aires, Argentina Consejo Nacional de Investigaciones Científicas y Técnicas (CONICET), Argentina Department of Computer Science, FCEFQyN, Universidad Nacional de Río Cuarto, Argentina Qatar University, Qatar New Jersey Institute of Technology, United States Department of Software Engineering, Instituto Tecnológico de Buenos Aires (ITBA), Argentina |
| Palabras clave: | 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 |
| Año: | 2014 |
| Volumen: | 8164 |
| Página de inicio: | 88 |
| Página de fin: | 107 |
| Título revista: | 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013 |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8164_n_p88_Rosner |
Referencias:
- Abrial, J.-R., (1996) The B-Book: Assigning Programs to Meanings, , Cambridge University Press
- Anastasakis, K., Bordbar, B., Georg, G., Ray, I., On challenges of model transformation from UML to Alloy (2010) Software and Systems Modeling, 9 (1), pp. 69-86
- Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E., Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 (2006) FMCO 2005. LNCS, 4111, pp. 342-363. , In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.), Springer, Heidelberg
- Chrabakh, W., Wolski, R., GrADSAT: A Parallel SAT Solver for the Grid UCSB Computer Science Technical Report Number 2003-05
- Eén, N., Sörensson, N., An Extensible SAT-solver (2004) SAT 2003. LNCS, 2919, pp. 502-518. , In: Giunchiglia, E., Tacchella, A. (eds.), Springer, Heidelberg
- A Message Passing Interface Standard. Message Passing Interface Forum (1998) High Performance Computing Applications, 12, pp. 1-299. , MPI2
- Dalcin, L., Paz, R., Storti, M., D’Elia, J., MPI for Python: Performance improvements and MPI-2 extensions J. Parallel Distrib. Comput., 68 (5), pp. 655-662
- http://www.msoos.org/cryptominisat2; Davies, J., Woodcock, J., Using, Z., Specification, Refinement and Proof (1996) International Series in Computer Science, , Prentice Hall
- Dennis, G., Chang, F., Jackson, D., Modular Verification of Code with SAT (2006) ISSTA 2006, pp. 109-120
- Galeotti, J.P., Rosner, N., Pombo, C.L., Frias, M.F., Analysis of invariants for efficient bounded verification (2010) ISSTA 2010, pp. 25-36
- Gil, L., Flores, P., Silveira, L.M., PMSat: A parallel version of MiniSAT. Journal on Satisfiability (2008) Boolean Modeling and Computation, 6, pp. 71-98
- Jackson, D., Schechter, I., Shlyakhter, I., Alcoa: The alloy constraint analyzer (2000) Proceedings of ICSE, p. 2000. , Limerick, Ireland
- Jackson, D., (2006) Software Abstractions, , MIT Press
- Maoz, S., Ringert, J.O., Rumpe, B., CD2Alloy: Class Diagrams Analysis Using Alloy Revisited (2011) MODELS 2011. LNCS, 6981, pp. 592-607. , Whittle, J., Clark, T., K¨uhne, T. (eds.), Springer, Heidelberg
- Malik, P., Groves, L., Lenihan, C., Translating Z to Alloy (2010) ABZ 2010. LNCS, 5977, pp. 377-390. , In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.), Springer, Heidelberg
- Matos, P.J., Marques-Silva, J., Model Checking Event-B by Encoding into Alloy (2008) ABZ 2008. LNCS, 5238, p. 346. , Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.), Springer, Heidelberg
- Ohmura, K., Ueda, K., C-sat: A Parallel SAT Solver for Clusters (2009) SAT 2009. LNCS, 5584, pp. 524-537. , In: Kullmann, O. (ed.), Springer, Heidelberg
- Ramananandro, T., Mondex, an electronic purse: Specification and refinement checks with the Alloy model-finding method (2008) Formal Aspects of Computing, 20 (1), pp. 21-39
- Shao, D., Gopinath, D., Khurshid, S., Perry, D., Optimizing Incremental Scope- Bounded Checking with Data-Flow Analysis (2010) ISSRE 2010, pp. 408-417
- Shao, D., Khurshid, S., Perry, D., An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method (2009) FM 2009. LNCS, 5850, pp. 757-772. , In: Cavalcanti, A., Dams, D.R. (eds.), Springer, Heidelberg
- Sperberg-McQueen, C.M., Alloy Version of Xpath 1.0 Data Model, , http://www.blackmesatech.com/2010/01/xpath10.als
- (1999) XML Path Language (Xpath) Version 1.0, , World Wide Web Consortium (W3C), W3C Recommendation (November 16
- Zave, P., Compositional binding in network domains (2006) FM 2006. LNCS, 4085, pp. 332-347. , In: Misra, J., Nipkow, T., Sekerinski, E. (eds.), Springer, Heidelberg
- Zhang, H., Bonacina, M.P., Hsiang, J., PSATO: A distributed propositional prover and its application to quasigroup problems (1996) J. Symb. Comput, 21, pp. 4-6
- http://cecar.fcen.uba.ar/A4 -
Citas:
---------- APA ----------
Rosner, N., Pombo, C.G.L., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F., Rybalchenko A.,..., Cohen E. (2014) . Parallel bounded verification of alloy models by tranScoping. 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013, 8164, 88-107.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8164_n_p88_Rosner [ ]
---------- CHICAGO ----------
Rosner, N., Pombo, C.G.L., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F., et al. "Parallel bounded verification of alloy models by tranScoping" . 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013 8164 (2014) : 88-107.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8164_n_p88_Rosner [ ]
---------- MLA ----------
Rosner, N., Pombo, C.G.L., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F., et al. "Parallel bounded verification of alloy models by tranScoping" . 5th International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2013, vol. 8164, 2014, pp. 88-107.Recuperado de https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8164_n_p88_Rosner [ ]
---------- VANCOUVER ----------
Rosner, N., Pombo, C.G.L., Aguirre, N., Jaoua, A., Mili, A., Frias, M.F., et al. Parallel bounded verification of alloy models by tranScoping. Lect. Notes Comput. Sci. 2014;8164:88-107.Available from: https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v8164_n_p88_Rosner [ ]
