Model Checking Analysis of Semantically Annotated Business Processes = Modelo Comprobación de Análisis de Procesos de Negocio anotados semánticamente

Resumen

Semantic business processes require new analysis techniques able to deal with behavioral properties that also consider semantic aspects. In this paper, a model checking method is introduced including semantic aspects in both the model description and the formula to be verified. In addition, Unary resource description framework (RDF) annotated Petri net systems, a formalism that allows the semantic description of business processes using RDF annotations, is formally defined and used to represent the input model of the model checker. Finally, the prototype implementations of both the Unary RDF annotated Petri net formalism and a model checker framework based on the use of RDF and SPARQL tools are also presented---Los procesos de negocio semánticas requieren nuevas técnicas de análisis capaces de hacer frente a las propiedades de comportamiento que también se consideran aspectos semánticos. En este trabajo, un método de comprobación de modelo se introdujo incluyendo aspectos semánticos, tanto en la descripción del modelo y la fórmula para ser verificado. Además, Resource Description Framework Unario (RDF) anotado sistemas de redes de Petri, un formalismo que permite la descripción semántica de los procesos de negocio utilizando anotaciones RDF, se define formalmente y se utiliza para representar el modelo de entrada del comprobador de modelos. Finalmente, las implementaciones prototipo de tanto la Unario RDF anotados Petri formalismo red y un marco corrector modelo basado en el uso de RDF y SPARQL herramientas también se presentan.