Verificación y Validación Formal para SOA

A medida que el desarrollo de software fue creciendo en alcance y complejidad, el proceso de controlar el comportamiento de los sistemas para que sea exactamente igual al esperado fue tornándose cada vez más difícil. Encontrar errores lo antes posible es clave para cualquier desarrollo, ya que los costos para corregirlos aumentan de manera exponencial a medida que avanza el proyecto. La etapa de testing es indispensable en este sentido, aunque no asegura la ausencia de errores: aquellos que no estén cubiertos en los casos de tests pasarán desapercibidos.

Ante esta situación surgieron técnicas para verificar formalmente el comportamiento de los sistemas, dentro de las cuales se destaca una llamada model checking. Una herramienta de model checking (o un model checker) verifica que el comportamiento de un sistema determinado cumpla una cierta propiedad, chequeando todas las posibles ejecuciones del sistema. Ya que es una actividad costosa en recursos y tiempo, la validación a través de model checking se emplea en casos donde se requiere constatar el comportamiento de un sistema de manera rigurosa, completa y exhaustiva.

Model Checking y SOA

Tales situaciones pueden encontrarse cada vez más dentro de aplicaciones y sistemas basados en arquitectura SOA, aunque con un condimento extra. Deben verificarse múltiples servicios en entornos altamente distribuidos y con numerosos canales de comunicación.

Para llevar a cabo esta acción se emplean model checkers orientados a servicios. Dentro de los mismos podemos mencionar a WSAT (Web Service Analysis Tool), disponible en http://www.cs.ucsb.edu/~su/WSAT/. El principal impacto de esta herramienta está en intensos controles sobre el intercambio distribuido de mensajes. Otras aproximaciones se basan en cambio en verificar el flujo de control de los servicios involucrados: para esto se emplean model checkers como BLAST o BLADE.

Otra arista de la validación está relacionada con la performance de cada servicio en relación a la carga que pueden soportar. Para atacar este punto son críticos los test de stress, los cuales cuantifican la frecuencia de las respuestas de los servicios ante condiciones adversas. Estos parámetros son de gran utilidad para establecer un service-level agreement (SLA) adecuado, el cual establece un acuerdo y habilita una validación frente al cliente respecto al nivel de calidad de servicio esperado.

Como se mencionó anteriormente, el model checking es un proceso costoso, y más en entornos distribuidos. Teniendo esto en cuenta, los model checkers para SOA suelen asumir ciertas condiciones, dependiendo de la herramienta, para poder completar en un tiempo razonable su tarea. Por ejemplo, asumir que los mensajes no se pierden, que la ejecución de los servicios es atómica (o se realiza en su totalidad o no se realiza) o que no existen restricciones de tiempo real. Todas estas son limitaciones que deben considerarse al elegir el model checker más conveniente.

Es claro que la verificación formal no es aplicable en todas las situaciones y arquitecturas SOA. Su utilización tiene sentido en contextos muy específicos, donde existen fuertes requerimientos respecto al comportamiento esperado. Otra posibilidad cada vez más elegida es verificar formalmente sólo partes críticas de la integración de servicios, y no todo el sistema. Esta opción permite balancear adecuadamente los pros y contras de la verificación formal.