XJML 1.0 lanzado/XJML 1.0 released

Español

¡Hola a todos! Primero que nada, ¡les deseo un Feliz Año Nuevo 2012! Ahora bien, es un placer para mí, y estoy muy feliz de presentarles el primer lanzamiento de XJML, es decir XJML 1.0. XJML es la arquitectura de Verificación y Validación resultante de mi tesis de maestría titulada "Verificación y validación modular externa de Sistemas Orientados a Objetos empleando Diseño por Contrato".

La X en XJML es por XML (es decir, podemos escribir contratos para las clases Java que deseemos verificar) y la JML es el acrónimo para Java Modeling Language, el lenguaje subyacente y soportado por XJML.

¡Pero basta de hablar! Puede acceder todos los recursos de XJML (código fuente, librerías, documentación, tesis, etc.) a través de SourceForge: https://sourceforge.net/p/xjml/.

Los desarrolladores que deseen contribuir con el proyecto XJML pueden acceder a través de SVN: https://xjml.svn.sourceforge.net/svnroot/xjml/ or https://sourceforge.net/p/xjml/code/

Por último, pero no menos importante, puede encontrar en https://sourceforge.net/p/xjml/tickets/ algunas tareas con las que nos puede ayudar a mejorar XJML.

Esperamos sus opiniones sobre el proyecto, aportaciones, dudas, comentarios, críticas constructivas, todo aquello que persiga el objetivo de aportar conocimiento en esta área nos será valioso.

English

Hi everybody! First at all, I wish you a Happy New Year 2012! Now, is a pleasure for me, and I'm so glad to introduce you the first release of XJML, I mean XJML 1.0. XJML is the Verification and Validation architecture resulting from my master thesis called "Verification and validation modular external for Object Oriented Systems using Design By Contract".

The X in XJML is for XML (so, we can write contracts for the Java classes which want to verify) and the JML is the acronym for Java Modeling Language, the underlying language and supported by XJML.

Enough talk! You can access all the XJML resources (source code, libraries, documentation, thesis, etc.) through SourceForge: https://sourceforge.net/p/xjml/.

The developers who want contribute with the XJML project can access through SVN: https://xjml.svn.sourceforge.net/svnroot/xjml/ or https://sourceforge.net/p/xjml/code/

Last but not least, you can find in https://sourceforge.net/p/xjml/tickets/ tickets describing some tasks where you can help us to improve XJML.

We welcome your views on the project, contributions, questions, comments, constructive criticism, all that work towards the goal of providing knowledge in this area it will be valuable.

The way of the master...

Español

El título de este post es en honor a mi colega y amigo Genaro Alfonso, quien me imagino que usó tal título para su blogger haciendo alusión al camino del maestro, este camino que iniciamos de la Maestría en Sistemas Computacionales, en nuestra orgullosa y siempre amada División Académica de Informática y Sistemas, de la Universidad Juárez Autónoma de Tabasco. . .

Pero bueno, sin más, comparto un poco con ustedes (si es que hay alguien que me lee) sobre el área en la que estoy investigando. Mi tesis lleva por nombre "Verificación y validación modular externa de sistemas orientados a objetos empleando Diseño por Contrato. Caso: Comsión Estatal de Derechos Humanos" y claro, el área es Verificación y validación de sistemas, de la especialidad Ingeniería de Software.

En posteriores entradas les platicaré un poco más sobre lo que estoy proponiendo pues no me gustaría adelantar nada hasta no tener TODO lo más estable posible, de manera que no se "muevan" los componentes que estoy desarrollando y la propuesta y resultados están acordes con mis objetivos de investigación. Sólo compartiré un breve contexto de qué estoy usando y les platicaré un poco sobre la parte experimental y algunos conceptos del área de V&V.

Estoy trabajando con JML, acrónimo de Java Modeling Language el cual es un lenguaje para la especificación de interfaces de comportamiento que puede ser usado para especificar el comportamiento de módulos Java. Combina la técnica de Diseño por Contrato del lenguaje Eiffel y la especificación basada en modelos de la familia de lenguajes de especificación Larch, con algunos elementos del cálculo de refinamiento.

Hasta el momento llevo 80 experimentos realizados, de los cuales:

• 40 sirvieron para evaluar resultados de la técnica de verificación conocida como Runtime Assertion Checking (RAC).
  
  RAC es una técnica basada en compilación para traducir especificaciones a bytecode de verificación en tiempo de ejecución. A diferencia de los verificadores estáticos (descritos en el siguiente párrafo) los cuales verifican propiedades del programa en tiempo de compilación, JML RAC permite la verificación dinámica mediante la generación de bytecode que verifica que las especificaciones se cumplan durante la ejecución del programa. En el momento en el que una aserción falle, el código generado por JML RAC genera un error en tiempo de ejecución.
  
  En pocas palabras, RAC verifica código en tiempo de ejecución, requiriendo así un punto de ejecución del programa a verificar. Por ejemplo, en una clase Java, tradicionalmente el método public static void main(String[]).
  


• 40 fueron utilizados para estudiar el comportamiento y resultados de la técnica de verificación conocida como Extended Static Checking (ESC).
  
  ESC se encarga de la verificación estática en tiempo de compilación de las aserciones expresadas en XJML. Una diferencia significativa entre ESC/Java y RAC, es que el primero verifica la clase sin requerir un punto de ejecución como sucede con RAC.
  



• 40 se usarán en el estudio de Full Static Program Verification (FSPV).
  
  FSPV es una técnica de verificación que al igual que ESC emplea verificador de teoremas (theorem prover). ESC emplea, de manera predeterminada Simplify, mientras que FSPV a través de Proof General Kit usa Isabelle/HOL. FSPV es similar en comportamiento a ESC, en el sentido de no requerir un punto de ejecución, vaya, es también una verificación estática, que sin embargo detecta más errores en los módulos de un sistema (ver imagen).
  

Y bla, bla, bla. . . En próximas entradas, primeramente Dios (jajaja, el otro día estaba pensando: "se supone que soy Agnóstico y sin embargo, creo en Dios, pero bueno, religión X, política X") espero poder compartirles más sobre esto, si es que a alguien le interesa :)

Have a good day. 04:17:10 AM, Martes 15, noviembre 2011 CST.

¿En serio?/Really?

Español

El día de hoy encontré un blog interesante, el blog de Tecnología de Bertrand Meyer y me agrada mucho lo que he leído en sus dos primeros posts: "Nastiness in computer science" y en "All Bugs Great and Small".

Me recuerdan una entrevista que me hicieron hace como dos años y medio donde por supuesto escuché algo así como: "no escuché nada que me sorprenda" y la incompetencia y arrogancia de algunos quienes estamos en ésta disciplina.

Y finalmente, es agradable saber de las experiencias de otros, y en este contexto no me quedó nada más que reírme de sorpresa al leer las razones por las cuales se rechazó un artículo, por allá en 1987 cuando el comité revisor se basó en dos puntos fuertes para su rechazo:

• Pienso que el tiempo le demostrará que la herencia (sección 1.5.3) es una terrible idea.


• Los sistemas que hacen recolección automática de basura (garbage collection) y le evitan así al diseñador de realizar esto, no son buenos sistemas que refuercen industrialmente la ingeniería de software.

Esto me da un poco más de tranquilidad, el saber que no nada más yo he pasado por fuertes críticas. Críticas que muchas veces son duras y más si vienen de una figura muy respetada e imagen exterior de alguna organización, que cuando nos da su punto de vista sobre nuestras ideas parece ser que nos dejan en la lona, después de todo es agradable imaginar que el paso del tiempo les dejará ver que él/ella estaba equivocado y que aquella persona de la que dudaron, después de todo tenía razón.

¿Hacía dónde vamos en nuestra disciplina de estudio?

PD = Pendiente traducción al inglés/English translation pending