Dennis et al. [1] someten a verificación 6 distintas implementaciones en Java de la estructura de datos Lista Enlazada. Para ello, los autores aplican un análisis modular, en el cual cada método de la clase es analizado de manera independiente al resto de métodos de la misma clase. El análisis involucra una reducción automática de dos fases: primero, a una forma intermedia en lógica relacional, y posteriormente, una conversión a formula booleana (empleando técnicas existentes), la cual es entonces manipulada por un solucionador SAT.
Los resultados presentados en este trabajo demuestran violaciones dentro de las implementaciones de varias librerías de acuerdo a la especificación abstracta de LinkedList y revelan también errores en la especificación de JML (Java Modeling Language).
Como trabajo futuro los autores proponen evaluar el análisis modular vs. análisis completo de un sistema. Finalmente concluyen con la aseveración que la técnica que presentan parece ser viable, aunque todavía queda mucho trabajo por hacer. Consideran que el obstáculo mayor para extender el análisis a todos los métodos de la interfase List es el manejo de colecciones genéricas en métodos tales como addAll.
Referencias
[1] G. Dennis, F. ShengHo Chang and D. Jackson. Modular verification of Code with SAT. ISSTA’06, July 17–20, 2006.
http://sdg.csail.mit.edu/pubs/2006/dennis_modular.pdf
No hay comentarios.:
Publicar un comentario