Artículo
Aguirre, N.M.; Frias, M.F.; Ponzio, P.; Cardiff, B.J.; Galeotti, J.P.; Regis, G. "Towards abstraction for DynAlloy specifications" (2008) 10th International Conference on Formal Engineering Methods, ICFEM 2008. 5256 LNCS:207-225
Consulte la política de Acceso Abierto del editor
Abstract:
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.
Registro:
| Documento: | Artículo |
| Título: | Towards abstraction for DynAlloy specifications |
| Autor: | Aguirre, N.M.; Frias, M.F.; Ponzio, P.; Cardiff, B.J.; Galeotti, J.P.; Regis, G. |
| Ciudad: | Kitayushu-City |
| Filiación: | Department of Computer Science, FCEFQyN, Universidad Nacional de Río Cuarto, Argentina Department of Computer Science, FCEyN, Universidad de Buenos Aires, Argentina |
| Palabras clave: | Abstracting; Computer software; Formal methods; Java programming language; Model checking; Program translators; Software engineering; Specifications; Atomic actions; Case studies; Dynamic logics; Final states; Intermediate states; JAVA programs; Operational units; Partial correctnesses; Predicate abstractions; SAT solvers; Computer software reusability |
| Año: | 2008 |
| Volumen: | 5256 LNCS |
| Página de inicio: | 207 |
| Página de fin: | 225 |
| DOI: | http://dx.doi.org/10.1007/978-3-540-88194-0-14 |
| Título revista: | 10th International Conference on Formal Engineering Methods, ICFEM 2008 |
| Título revista abreviado: | Lect. Notes Comput. Sci. |
| ISSN: | 03029743 |
| Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v5256LNCS_n_p207_Aguirre |
Referencias:
- 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
- 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
- Clarke, E., Grumberg, O., Long, D., Model checking and abstraction (1994) ACM Transactions on Programming Languages and Systems (TOPLAS), 16 (5)
- 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)
- 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
- 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
- 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
- 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)
- 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
- 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
- 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
- Jackson, D., Alloy: A lightweight object modelling notation (2002) ACM Transactions on Software Engineering and Methodology (ACM TOSEM), 11 (2)
- Jackson, D., (2006) Software Abstractions: Logic, Language, and Analysis, , MIT Press, Cambridge
- 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)
- Taghdiri, M., Inferring Specifications to Detect Errors in Code (2004) Proceedings of the 19th International Conference on Automated Software Engineering ASE, , Austria September
- 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
- Woodcock, J., Davies, J., (1996) Using Z: Specification, Refinement and Proof, , Prentice-Hall, Englewood Cliffs
- 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
Citas:
---------- APA ----------
Aguirre, N.M., Frias, M.F., Ponzio, P., Cardiff, B.J., Galeotti, J.P. & Regis, G. (2008) . Towards abstraction for DynAlloy specifications. 10th International Conference on Formal Engineering Methods, ICFEM 2008, 5256 LNCS, 207-225.http://dx.doi.org/10.1007/978-3-540-88194-0-14
---------- CHICAGO ----------
Aguirre, N.M., Frias, M.F., Ponzio, P., Cardiff, B.J., Galeotti, J.P., Regis, G. "Towards abstraction for DynAlloy specifications" . 10th International Conference on Formal Engineering Methods, ICFEM 2008 5256 LNCS (2008) : 207-225.http://dx.doi.org/10.1007/978-3-540-88194-0-14
---------- MLA ----------
Aguirre, N.M., Frias, M.F., Ponzio, P., Cardiff, B.J., Galeotti, J.P., Regis, G. "Towards abstraction for DynAlloy specifications" . 10th International Conference on Formal Engineering Methods, ICFEM 2008, vol. 5256 LNCS, 2008, pp. 207-225.http://dx.doi.org/10.1007/978-3-540-88194-0-14
---------- VANCOUVER ----------
Aguirre, N.M., Frias, M.F., Ponzio, P., Cardiff, B.J., Galeotti, J.P., Regis, G. Towards abstraction for DynAlloy specifications. Lect. Notes Comput. Sci. 2008;5256 LNCS:207-225.http://dx.doi.org/10.1007/978-3-540-88194-0-14
