Analyzing Behavioral Properties of Semantic Business Processes with Parametric Data

Resumen

One of the basic problems in (semantic) business process management concerns the behavioral analysis at design time so that only correct processes are exposed. Although this analysis requires the semantic propagation of data and system preconditions through processes and between processes to be considered, some concrete data are usually obtained at runtime and cannot be used in early process development phases. This paper proposes Parametric Unary RDF Annotated Petri Net Systems (P-U-RDF-PN Systems) as a formalism to alleviate this problem. The formalism allows analyzing behavioral properties of semantic business processes at design time. Parametric values are used to represent the data that will be obtained at runtime, allowing to also consider them in the analysis phase. The paper formally defines the semantics of the formalism in terms of enabling and firing of transitions as well as the concept of reachability graph. It also presents how to compute and analyze this parametric reachability graph. The analysis is based on an adaption of model checking techniques, being temporal logic the formalism used to specify the system properties to be analyzed. Finally, an implementation prototype using RDF and SPARQL tools and a Satisfiability Modulo Theories solver is presented, with some experiments evaluating how scalable the prototype is