2009/09/29

Verificación modular de código con SAT

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

Estado del arte

Para el desarrollo de una tesis la investigación del estado del arte (trabajos relacionados, antecedentes, o como se le quiera llamar) es una actividad de suma importancia cuyo objetivo es demostrar la relevancia de nuestra investigación propuesta y/o demostrar que nuestra propuesta es única.


Para dicha tarea, en mi tesis de maestría me encargaré de estudiar lo referente a la verificación y validación de sistemas orientados a objetos aplicando métodos formales, por lo que mediante este espacio, presentaré sinopsis de los artículos, tesis y demás trabajos de investigación que den soporte al estado del arte de mi tesis en desarrollo. De esta manera, en mi siguiente post les dejaré la sinopsis del artículo titulado "Modular verification of Code with SAT" de Dennis et al. [1].


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

2009/08/28

Enfoque humanitario para contrarrestar los efectos del cambio climático

Y continuando con mi búsqueda me vino a la mente algo que es muy bien sabido por todos y que concierne a la situación climatológica en nuestro planeta. No evité pasar por alto la idea de proponer una solución al fenómeno del cambio climático, atender quizás, uno de sus efectos secundarios y tal vez el de mayor impacto en nuestros días: la evidente escasez de agua. Después de todo, dicen los expertos que en el futuro las guerras no serán por petróleo, ni por territorios, se luchara por el agua.

Se preguntarán qué tiene que ver este tema en el blog, vaya, ¡no trata sobre ciencias naturales! El fenómeno del cambio climático es un tema que no sólo le concierne a los profesionales e involucrados de las ciencias naturales. Un muy buen tema de tesis para un posgrado, preferentemente un grupo de investigación multi-disciplinar. Por ello, en mi mente me planteo:

Es naturaleza del ser humano –racional; ¿es posible que existan seres humanos no racionales?- cuestionarse sobre el origen de las cosas, los fenómenos de la naturaleza. Desde principios de la humanidad, nuestros ancestros se planteaban interrogantes mismas que dieron origen al concepto de curiosidad, y siglos después, miles de años después, al método científico como lo conocemos hoy en día.

El invento de la rueda, el descubrimiento del fuego, la explicación de los fenómenos de la naturaleza (lluvia, relámpagos, arco iris, etc., etc.) son algunas de las cosas que la humanidad ha logrado demostrar de manera científica.

Para muchos de los retos y dificultades que la naturaleza nos ha presentado, hemos logrado, como humanidad proponer y aplicar soluciones que nos permitan convivir en armonía con ella. Para refugiarnos de la lluvia, se diseñan y construyen casas; para mantener nuestra temperatura corporal estable en los tiempos calurosos, se diseñan y se construyen dispositivos de ventilación y climatización…

Hoy en día, nos enfrentamos a un nuevo reto: los cambios climáticos, en particular, el fenómeno del calentamiento global, que entre otros efectos secundarios, y aunado a nuestro comportamiento irresponsable, ha puesto en evidencia una escasez de agua. Mientras usted está leyendo esto, la comunidad científica busca alternativas para contrarrestar los efectos del calentamiento global. A mí parecer, esta empresa debe ser una tarea conjunta, totalitaria de la humanidad. No sólo climatólogos, biólogos, químicos, y demás profesionales de las ciencias naturales. Es una tarea que también debe de involucrar a especialistas en ciencias y tecnologías computacionales, a la comunidad política, industrias, padres… Es algo que nos concierne a todos.

Porqué no, como seres racionales buscamos soluciones científicas-tecnológicas apoyadas de leyes globalizadas, pues después de todo, el concepto de globalización es ya una realidad desde hace un poco más de una década. Qué tal si la comunidad científica y/o tecnológica trabajamos juntos, proponiendo soluciones en las que quizás se regule el uso de agua a través de dispositivos electromecánicos, apoyados por una ley globalizada que penalice a todos quienes infrinjamos nuestro consumo de agua permitido.

Como he dicho, esto no sólo implica un esfuerzo de investigación y política, sino también de ética y responsabilidad social: la solución pudiese ser factible, viable e implementada. Sin embargo, muchos de nosotros tendemos a incumplir las leyes: robar luz, “colgarnos” de la señal de cable del vecino, discos o antros en los que se permite el acceso a menores de edad, y de seguro, no faltará quien robara agua.

Muchos opinarían que es una medida drástica: controlar (a nivel mundial) el consumo de agua, no sólo por medio de leyes cuyo incumplimiento impliquen la penalización (económica), si no también a través de dispositivos que midan el consumo del agua. Perfectamente sé que aplicar una ley globalizada implica quebrantar/debilitar la autonomía de los países y regímenes de gobierno, no obstante justifico esto bajo el contexto de globalización. El mundo, geográfica y socialmente tiende a unificarse: el inglés es prácticamente el idioma mundial por excelencia, la Internet nos permite la comunicación e intercambio de extremo a extremo en el planeta, el euro es la moneda que predomina en Europa, el dólar en América.

¿Porqué no una ley globalizada, porqué no? ¿Por qué no los países, al igual que firman tratados internacionales de economía, seguridad y otros, se firmase un tratado internacional donde los gobiernos se comprometan a vigilar el consumo de agua de sus habitantes? Y también entramos nosotros, la comunidad científica-tecnológica apoyando, como ya he dicho, en esta empresa, implementando dispositivos electromecánicos que regulen el consumo de la misma…