Applications of formal methods to performance evaluation

Resum

En esta tesis se presenta un modelo teórico para validar características cualitativas y cuantitativas en sistemas concurrentes, multiprocesadores y de tiempo real: el Álgebra de procesos Markovianos ROSA. Se presenta una semántica operacional y otras denotacional para capturar las propiedades funcionales de un sistema, en particular pueden analizarse sistemas no deterministas, con probabilidades (generativas) y distribuciones Exponenciales y Poisson. Se proporcionan Relaciones de Equivalencia sobre estas semánticas que permiten comparar procesos funcionalmente. Asimismo se presenta un algoritmo de evaluación temporal que permite comparar la eficiencia de procesos. Se aplica ROSA al análisis de ABP (un caso de estudio clásico) y el MPEG-2 (una aplicación realcuyas características temporales son cruciales) obteniendo resultados interesantes. De esta forma se demuestra la utilidad de los modelos formales en la evaluación de prestaciones en sistemas reales. Finalmente, la imposibilidad de describir con exactitud la concurrencia real mediante ORSA conduce al uso de otro formalismo menos intuitivo pero con mejores aptitudes para el análisis de la concurrencia real: las Redes de Petri con Arcos Temporizados. Mediante su aplicación muy interesantes resultados en la mejora de la implementación del algoritmo de ciompresión de vido MPEG2, tales como un análisis de número de procesadores requeridos cuando se permita la maxima concurrencia, así como la mejora teórica obtenida en las prestaciones de este algoritmo.