Marcos temporales y probabilística para testing formal

Abstract

Los métodos formales son técnicas con base matemática que se utilizan tanto para el diseño y análisis de sistemas como para la evaluación de su corrección. El uso de métodos formales es especialmente relevante en sistemas en los que es importante asegurar que durante el proceso de desarrollo no se han producido errores. La representación formal de estos sistemas permite un análisis riguroso de sus propiedades. En particular, permite establecer la corrección del sistema con respecto a su especificación y, por tanto, asegurar su calidad. El método analitíco de mayor aplicación en entornos industriales orientado a dicho objetivo es el testing. Inicialmente, los métodos de testing estaban orientados al chequeo de aspectos cualitativos del sistema. Sin embargo, una gran parte de los sistemas desarrollados requieren considerar no sólo las acciones que se pueden ejecutar sino también los aspectos cuantitativos asociados con dichas acciones. Entre estas cabe destacar tanto condiciones temporales como probabilísticas, que juegan un papel decisivo a la hora de establecer la corrección de los sistemas. Un primer paso para poder realizar testing formal de sistemas que presentan este tipo de restricciones es la extensión de los lenguajes de especificación con elementos que permitan expresar dichas propiedades. Así mismo, las nociones de corrección deben adecuarse para tener en cuenta la dimensión temporal y /o probabilística. De un modo similar, los algoritmos de generación de tests deben ser adaptados para tratar con dichos requerimientos. El principal objetivo de esta tesis es la extensión de los métodos formales utilizados en las metodologías para el testing de sistemas, de modo que estos puedan ser aplicados a sistemas con restricciones temporales referentes al tiempo consumido por las acciones, el tiempo de espera del sistema para recibir una reacción del entorno, la probabilidad de que una acción tenga lugar, o la probabilidad de que una acción consuma una determinada cantidad de tiempo en su ejecución. Junto a ello, la aplicación de tests para la comprobación de dichas propiedades y la obtención de diagnósticos respecto a la corrección de los sistemas, es un objetivo prioritario de nuestro trabajo.