Formalización de OASIS en lógica dinámica incluyendo especificaciones de proceso

Abstract

OASIS en su versión 2.2 de OASIS utiliza como marco formal una variante de Lógica Dinámica. Sin embargo, la sección de especificación de procesos en la plantilla de una clase es formalmente tratada mediante un Algebra de Procesos para objetos. Este trabajo presenta una nueva visión para especificaciones de procesos en OASIS. Desde una perspectiva deóntica una especificación de clase en OASIS es un conjunto de axiomas de prohibición y obligación de ocurrencia de acciones, además de un conjunto de axiomas que establecen los mundos previos e inmediatamente posteriores a la ocurrencia de una acción. Consecuentemente, se distinguen dos tipos de especificaciones de procesos: aquellos que establecen prohibiciones (patterns) y aquellos que establecen obligaciones (operations). Se muestra cómo una especificación de procesos básica, incluyendo operadores de secuencia y alternativa, puede ser vista como un conjunto de axiomas en Lógica Dinámica. Esto permite formalizar toda la plantilla de clase OASIS en Lógica Dinámica. Utilizando un sublenguaje de CCS se presentan las correspondencias entre especificaciones de proceso en dicho lenguaje y axiomas en Lógica Dinámica. Se incluyen algunos ejemplos aplicados a OASIS.