| Título: | Verificación de propiedades temporales en PPML |
| Autores: |
Regis, Germán Aguirre, Nazareno Matías |
| Fecha: |
2012-10-03 2008-10 2008 |
| Publicador: | Unversidad Nacional de La Plata |
| Fuente: |
 |
| Tipo: |
Objeto de conferencia Objeto de conferencia |
| Tema: |
métodos formales autómatas temporizados business processes procesos de negocios Formal methods Model checking Ciencias Informáticas |
| Descripción: |
Product Process Modeling Languaje(PPML) es un lenguaje formal para modelar Procesos de Negocios que posee una semántica basada en sistemas de transición de estados temporizados. El lenguaje posee elementos que lo hacen apropiado para la especificación formal de procesos de negocios con restricciones temporales, concurrencia, etc. Sin embargo, no existe actualmente ninguna herramienta de soporte al lenguaje; en particular, el lenguaje carece de herramientas de verificación de propiedades temporales asociadas a las especificaciones. En este trabajo proponemos, en primer lugar, una codificación de la semántica de PPML en autómatas temporizados, a través de una traducción de PPML al lenguaje UPPAAL. En segundo lugar, aprovechamos esta traducción, que ha sido automatizada en un prototipo, para realizar verificación de propiedades CTL (branching time) de especificaciones PPML, utilizando la herramienta asociada a UPPAAL. Product Process Modeling Languaje(PPML) is a formal language for the specification of Business Processes, it has a formal semantics based on timed transition systems. The language has artifacts that make it suitable for the formal specification of Business Processes with temporal restrictions, concurrency, etc. . Nevertheless, there is no support tool for the language. Particulary, the language lacks tools for the verification of temporal properties associated to specifications. In this paper we propose, first, a codification of the PPML semantics into timed automatas through a translation from PPML to the language UPPAAL. Second, we use this translation, that was automated in a prototype, in order to verify CTL (branching time) propierties of the PPML specifications, using the UPPAAL asociated tool. Workshop de Ingeniería de Software y Bases de Datos (WISBD) |
| Idioma: | Español |
1 Ajuste de las variables que gobiernan los modelos de comportamiento de HDM-4 para vías no pavimentadas de la región de Antofagasta (Chile) por Rojas Cazaluade, Oscar Orlando | 6 Alternativas para el fraccionamiento de un Parque Industrial por Borrego, Juan Antonio |
2 La Agrimensura como base de investigaciones arqueológicas por Alfageme, Marcelo O.,Papagni, Jorge H. | 7 La propiedad horizontal por López, María Inés |
3 Anteproyecto de saneamiento y loteo por Antolín, Ricardo Gabriel,Williams, Enrique Oliver | 8 Laguna "San Antonio" por Milone, Ricardo Raúl |
4 Balneario Municipal de la ciudad de Diamante por Battistessa, Gustavo J.,Palomeque, José F. | 9 Estudio catastral de tierras en el partido de San Fernando por Miquelarena, Carlos Alberto |
5 | 10 |