%0 Journal Article 
%A Letelier Torres, Patricio
%A Sánchez Palma, Pedro
%A Ramos Salavert, Isidro
%A Pastor López, Óscar
%T Formalización de OASIS en lógica dinámica incluyendo especificaciones de proceso
%D 1998
%U http://hdl.handle.net/10317/731
%X 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.
%K Lenguajes y Sistemas Informáticos
%K OASIS
%K Lógica dinámica
%K Álgebra de procesos para Objetos (APO)
%~ GOEDOC, SUB GOETTINGEN