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.