View article

Los lenguajes basados en máquinas de estados finitos (también llamadosautomátas finitos) son usados de manera ubicua para la especificación desistemas de software. La formalidad de estos modelos permite la aplicación de técnicasde validación tales como el model checking. De esta manera, pueden respondercon seguridad si un sistema cumple o no las propiedades de interés. Al mismo tiempo,estás máquinas pueden ser utilizadas de manera composicional, especificando comportamientosaislados mediante varias máquinas, y estableciendo el comportamientoglobal mediante su composición en paralelo. Este enfoque reduce el esfuerzo de validación,ya que la validez de las propiedades en el sistema deberían ser dependientesde la validez de las propiedades en cada componente. Sin embargo, este enfoque esamenazado por la complejidad del sistema especificado, dando lugar al problema dela explosión de estados, que puede impedir la aplicación de estas técnicas. En esta tesis presentamos un enfoque que intenta paliar este problema, proveyendoinformación cuantitativa respecto de la propiedad que se intentó validar sinéxito. Nuestro enfoque se sostiene sobre dos contribuciones distintas, donde cada unade ellas puede, además, ser aplicada en el contexto de problemas relacionados. Estatesis se inspira en el modelado y model checking probabilísticos, que pueden proveerinformación cuantitativa respecto de la validez de una propiedad. Esta cuantificaciónnos sirve de validación parcial en el contexto del problema que nos interesa. Sin embargo, un enfoque composicional tiene sus propios problemas en un …