Evolución del softwareuna formalización basada en lógica temporal de predicados y Redes de Petri coloreadas

Resumo

Se utilizan dos formalismos: las Redes de Petri Coloreadas (RdPC) y la Lógica Temporal de Predicados (LTP) para especificar la evolución del software, La tesis se basa en los trabajos previos de José Parets, en la metodología MEDES y herramienta HEDES desarrollados por éste dentro de este campo. Se formalizan los cambios de estructura que un sistema puede sufrir a lo largo de toda su vida y que implican que pase qa comportarse de forma diferente. En este procesod e maduración se debe velar por la conservación de una serie de invariantes. Para verificrlos se asocian precondiciones a las acciones de cambio que se verifican consultando una historia funcional y una historia estructural que guardan la memoria sobre el funcionamiento y los cambios de estructura que un sistema puede sufrir respectivamente. Se describre la sémántica de dos lenguajes basados en LTP. Con uno se especifícan las acciones y condiciones de realización asociadas a éstas. Con el otro se especifican las acciones estructurales, los cambios, y las condiciones asociadas a éstas. Se han creado algoritmos para dotar a los lenguajes basados en LTP de una semántica operacional, aprovechándose por tanto de las ventajas de ambos formalismos. Las RdPC porporcionan mecanismos de análisis de propiedades de los sistemas que modelan y permiten una representación gráfica y opracional de éstos. Debido a la reflexividad inducida a ambos formalismos se ha probado que la gestión del funcionamiento de un sistema y la ggestión de su cambios de estructura se hacen de foram homogénea y en ellos intervienen los mismos componentes. Todos los conceptos estudiados para la evolución dentro de este trabajo se han implementado y probado en la herramienta HEDEs.