Towards abstraction for DynAlloy specifications
DynAlloy is an extension of the Alloy language to better describe state change via actions and programs, in the style of dynamic logic. In this paper, we report on our experience in trying to provide abstraction based mechanisms for improving DynAlloy specifications with respect to SAT based analysi...
Guardado en:
| Autor principal: | |
|---|---|
| Otros Autores: | , , , , |
| Formato: | Acta de conferencia Capítulo de libro |
| Lenguaje: | Inglés |
| Publicado: |
2008
|
| Acceso en línea: | Registro en Scopus DOI Handle Registro en la Biblioteca Digital |
| Aporte de: | Registro referencial: Solicitar el recurso aquí |
| LEADER | 08320caa a22008177a 4500 | ||
|---|---|---|---|
| 001 | PAPER-5503 | ||
| 003 | AR-BaUEN | ||
| 005 | 20230518203508.0 | ||
| 008 | 190411s2008 xx ||||fo|||| 00| 0 eng|d | ||
| 024 | 7 | |2 scopus |a 2-s2.0-57049127201 | |
| 040 | |a Scopus |b spa |c AR-BaUEN |d AR-BaUEN | ||
| 100 | 1 | |a Aguirre, N.M. | |
| 245 | 1 | 0 | |a Towards abstraction for DynAlloy specifications |
| 260 | |c 2008 | ||
| 270 | 1 | 0 | |m Aguirre, N. M.; Department of Computer Science, FCEFQyN, Universidad Nacional de Río CuartoArgentina; email: naguirre@dc.exa.unrc.edu.ar |
| 506 | |2 openaire |e Política editorial | ||
| 504 | |a Ball, T., Cook, B., Das, S., Rajamani, S., Refining Approximations in Software Predicate Abstraction (2004) LNCS, 2988. , Jensen, K, Podelski, A, eds, TACAS 2004, Springer, Heidelberg | ||
| 504 | |a Bjorner, N., Browne, A., Colon, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T., Verifying Temporal Properties of Reactive Systems: A STeP Tutorial (2000) Formal Methods in System Design, 16 | ||
| 504 | |a Clarke, E., Grumberg, O., Long, D., Model checking and abstraction (1994) ACM Transactions on Programming Languages and Systems (TOPLAS), 16 (5) | ||
| 504 | |a Clarke, E., Kroening, D., Sharygina, N., Yorav, K., Predicate Abstraction of ANSI-C Programs using SAT (2003), Technical Report CMU-CS-03-186. Carnegie Mellon University; Cousot, P., Abstract interpretation (1996) ACM Computing Surveys, 28 (2) | ||
| 504 | |a Das, S., Dill, D., Successive Approximation of Abstract Transition Relations (2001) Proceedings of the IEEE Symposium on Logic in Computer Science LICS, , IEEE Computer Society Press, Los Alamitos | ||
| 504 | |a Das, S., Dill, D., Counterexample Based Predicate Discovery in Predicate Abstraction (2002) LNCS, 2517. , Aagaard, M.D, O'Leary, J.W, eds, FMCAD 2002, Springer, Heidelberg | ||
| 504 | |a Dennis, G., Chang, F., Jackson, D., Modular Verification of Code with SAT (2006) Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA, pp. 109-120. , Portland, Maine, USA, pp | ||
| 504 | |a Frias, M., López Pombo, C., Baum, G., Aguirre, N., Maibaum, T., Reasoning about static and dynamic properties in alloy: A purely relational approach (2005) ACM Transactions on Software Engineering and Methodology (TOSEM), 14 (4) | ||
| 504 | |a Frias, M., Galeotti, J.P., López Pombo, C., Aguirre, N., DynAlloy: Upgrading alloy with actions (2005) Proceedings of the 27th International Conference on Software Engineering ICSE, , ACM Press, New York | ||
| 504 | |a Frias, M, Galeotti, J.P, López Pombo, C, Aguirre, N, Efficient Analysis of DynAlloy Specifications. In: ACM Transactions on Software Engineering and Methodology TOSEM, ACM Press, New York; Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, 1254. Springer, Heidelberg (1997); Galeotti, J.P., Frias, M.F., DynAlloy as a, Formal Method for the Analysis of Java Programs (2006) Proceedings of IFIP Working Conference on Software Engineering Techniques (SET, , Warsaw. Springer, Heidelberg | ||
| 504 | |a Jackson, D., Vaziri, M., Finding Bugs with a Constraint Solver (2000) Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), pp. 14-25. , Portland, OR, USA, August 21-24, pp, ACM Press, New York | ||
| 504 | |a Jackson, D., Alloy: A lightweight object modelling notation (2002) ACM Transactions on Software Engineering and Methodology (ACM TOSEM), 11 (2) | ||
| 504 | |a Jackson, D., (2006) Software Abstractions: Logic, Language, and Analysis, , MIT Press, Cambridge | ||
| 504 | |a Kim, S.-K., Carrington, D.: Formalizing the UML Class Diagram Using Object-Z. In: France, R.B., Rumpe, B. (eds.) UML 1999. LNCS, 1723. Springer, Heidelberg (1999); Snook, C., Butler, M., UML-B: Formal modeling and design aided by UML (2006) ACM Transactions on Software Engineering and Methodology (TOSEM), 15 (1) | ||
| 504 | |a Taghdiri, M., Inferring Specifications to Detect Errors in Code (2004) Proceedings of the 19th International Conference on Automated Software Engineering ASE, , Austria September | ||
| 504 | |a Uchitel, S., Chatley, R., Kramer, J., Magee, J., LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios (2003) LNCS, 2619. , Garavel, H, Hatcliff, J, eds, TACAS 2003, Springer, Heidelberg | ||
| 504 | |a Woodcock, J., Davies, J., (1996) Using Z: Specification, Refinement and Proof, , Prentice-Hall, Englewood Cliffs | ||
| 504 | |a Xie, Y., Aiken, A., Saturn: A Scalable Framework for Error Detection Using Boolean Satisfiability ACM-Transactions on Programming Languages and Systems (TOPLAS), , to appearA4 - ICFEM Organizing Committee | ||
| 520 | 3 | |a DynAlloy is an extension of the Alloy language to better describe state change via actions and programs, in the style of dynamic logic. In this paper, we report on our experience in trying to provide abstraction based mechanisms for improving DynAlloy specifications with respect to SAT based analysis. The technique we employ is based on predicate abstraction, but due to the context in which we make use of it, is subject to the following more specific improvements: (i) since DynAlloy's analysis consists of checking partial correctness assertions against programs, we are only interested in the initial and final states of a computation, and therefore we can safely abstract away some intermediate states in the computation (generally, this kind of abstraction cannot be safely applied in model checking), (ii) since DynAlloy's analysis is inherently bounded, we can safely rely on the sole use of a SAT solver for producing the abstractions, and (iii) since DynAlloy's basic operational unit is the atomic action, which can be used in different parts within a program, we can reuse the abstraction of an action in different parts of a program, which can accelerate the convergence in checking valid properties. We present the technique via a case study based on a translation of a JML annotated Java program into DynAlloy, accompanied by some preliminary experimental results showing some of the benefits of the technique. © 2008 Springer Berlin Heidelberg. |l eng | |
| 593 | |a Department of Computer Science, FCEFQyN, Universidad Nacional de Río Cuarto, Argentina | ||
| 593 | |a Department of Computer Science, FCEyN, Universidad de Buenos Aires, Argentina | ||
| 690 | 1 | 0 | |a ABSTRACTING |
| 690 | 1 | 0 | |a COMPUTER SOFTWARE |
| 690 | 1 | 0 | |a FORMAL METHODS |
| 690 | 1 | 0 | |a JAVA PROGRAMMING LANGUAGE |
| 690 | 1 | 0 | |a MODEL CHECKING |
| 690 | 1 | 0 | |a PROGRAM TRANSLATORS |
| 690 | 1 | 0 | |a SOFTWARE ENGINEERING |
| 690 | 1 | 0 | |a SPECIFICATIONS |
| 690 | 1 | 0 | |a ATOMIC ACTIONS |
| 690 | 1 | 0 | |a CASE STUDIES |
| 690 | 1 | 0 | |a DYNAMIC LOGICS |
| 690 | 1 | 0 | |a FINAL STATES |
| 690 | 1 | 0 | |a INTERMEDIATE STATES |
| 690 | 1 | 0 | |a JAVA PROGRAMS |
| 690 | 1 | 0 | |a OPERATIONAL UNITS |
| 690 | 1 | 0 | |a PARTIAL CORRECTNESSES |
| 690 | 1 | 0 | |a PREDICATE ABSTRACTIONS |
| 690 | 1 | 0 | |a SAT SOLVERS |
| 690 | 1 | 0 | |a COMPUTER SOFTWARE REUSABILITY |
| 700 | 1 | |a Frias, M.F. | |
| 700 | 1 | |a Ponzio, P. | |
| 700 | 1 | |a Cardiff, B.J. | |
| 700 | 1 | |a Galeotti, J.P. | |
| 700 | 1 | |a Regis, G. | |
| 711 | 2 | |c Kitayushu-City |d 27 October 2008 through 31 October 2008 |g Código de la conferencia: 74360 | |
| 773 | 0 | |d 2008 |g v. 5256 LNCS |h pp. 207-225 |p Lect. Notes Comput. Sci. |n Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |x 03029743 |w (AR-BaUEN)CENRE-983 |z 354088193X |z 9783540881933 |t 10th International Conference on Formal Engineering Methods, ICFEM 2008 | |
| 856 | 4 | 1 | |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-57049127201&doi=10.1007%2f978-3-540-88194-0-14&partnerID=40&md5=4fd533e9a52221a932eccc279df08ff5 |y Registro en Scopus |
| 856 | 4 | 0 | |u https://doi.org/10.1007/978-3-540-88194-0-14 |y DOI |
| 856 | 4 | 0 | |u https://hdl.handle.net/20.500.12110/paper_03029743_v5256LNCS_n_p207_Aguirre |y Handle |
| 856 | 4 | 0 | |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5256LNCS_n_p207_Aguirre |y Registro en la Biblioteca Digital |
| 961 | |a paper_03029743_v5256LNCS_n_p207_Aguirre |b paper |c PE | ||
| 962 | |a info:eu-repo/semantics/article |a info:ar-repo/semantics/artículo |b info:eu-repo/semantics/publishedVersion | ||
| 963 | |a VARI | ||
| 999 | |c 66456 | ||