Model Checking Analysis of Semantically Annotated Business Processes

Author

Ibáñez, María José ; Fabra, Javier ; Álvarez, Pedro ; Ezpeleta, Joaquín

Author_Institution

Dept. of Comput. Sci. & Syst. Eng., Univ. de Zaragoza, Zaragoza, Spain

Volume

42

Issue

4

fYear

2012

fDate

7/1/2012 12:00:00 AM

Firstpage

854

Lastpage

867

Abstract

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.

Keywords

Petri nets; SQL; business data processing; formal verification; RDF annotations; SPARQL tools; annotated Petri net systems; model checking analysis; model checking method; resource description framework; semantically annotated business processes; unary RDF annotated Petri net formalism; Analytical models; Business; Data models; Process control; Resource description framework; Semantics; Business process analysis (BPA); Petri nets; SPARQL; model checking; resource description framework (RDF); semantic business processes (SBPs);

fLanguage

English

Journal_Title

Systems, Man and Cybernetics, Part A: Systems and Humans, IEEE Transactions on

Publisher

ieee

ISSN

1083-4427

Type

jour

DOI

10.1109/TSMCA.2012.2183357

Filename

6153390