Marcos temporales y probabilísticos para testing formal

Resumen

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 ase gurar 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 especifi cación y, por tanto, asegurar su calidad. El método analítico 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 sist ema. 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 tempor ales 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 deb en 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 res tricciones 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 c antidad 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.