Catálogo de publicaciones

Los lenguajes basados en máquinas de estados finitos (también llamados automátas finitos) son usados de manera ubicua para la especificación de sistemas de software. La formalidad de estos modelos permite la aplicación de técnicas de validación tales como el model checking. De esta manera, pueden responder con 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 comportamientos aislados mediante varias máquinas, y estableciendo el comportamiento global 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 dependientes de la validez de las propiedades en cada componente. Sin embargo, este enfoque es amenazado por la complejidad del sistema especificado, dando lugar al problema de la 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, proveyendo información cuantitativa respecto de la propiedad que se intentó validar sin éxito. Nuestro enfoque se sostiene sobre dos contribuciones distintas, donde cada una de ellas puede, además, ser aplicada en el contexto de problemas relacionados. Esta tesis se inspira en el modelado y model checking probabilísticos, que pueden proveer información cuantitativa respecto de la validez de una propiedad. Esta cuantificación nos sirve de validación parcial en el contexto del problema que nos interesa. Sin embargo, un enfoque composicional tiene sus propios problemas en un contexto probabilístico. Las anotaciones probabilísticas asociadas a eventos independientes precisan ser contrastadas con estimaciones obtenidas de la observación del comportamiento a modelar. Al agregar estas anotaciones, es preciso distinguir las fuentes de estas probabilidades; en otras palabras, las probabilidades de eventos independientes deberían estar asociadas al comportamiento de los componentes que generan este comportamiento. A su vez, es preciso mantener la relación entre la validez de los componentes de manera aislada, y la validez de los comportamientos en el sistema compuesto. Los formalismos disponibles al momento, sin embargo, no proveen la seguridad de que estos resultados de validez sean preservados durante la composición. La primera contribución de esta tesis es, entonces, una extensión probabilística al formalismo de Interface Automata. Esta extensión asegura la preservación de comportamiento tal como es observado por la lógica probabilística pCTL. La segunda parte de esta tesis apunta al análisis de estos modelos, en particular cuando un análisis exhaustivo no es factible, teniendo en cuenta que la complejidad del model checking probabilístico es aún mayor que en el caso clásico. Nuestra hipótesis en este trabajo es que una exploración parcial, pero sistemáticamente controlada, puede proveer cotas a los valores de interés con un costo computacional reducido. Los experimentos realizados sugieren que un análisis mediante este enfoque puede ser más efectivo que tanto el model checking exhaustivo como así también enfoques estadísticos relacionados.