Verificación de propiedades temporales en PPML

Abstract

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.