Executability Analysis for Semantically Annotated Process Model

Semantically annotated process model (SPM) is a process model with semantic annotations, which include the precondition and effect, labeled for its activities based on the domain ontology. Such semantic annotations can increase the model´s understanding and reusability, and facilitate its implement as well as compliance analysis. However, SPM analysis is challenging, since its correctness is beyond the soundness of process model and its formal semantics needs to consider domain state change. To assuring the correctness of SPM, the executablity analysis, i.e., whether there exists activity whose precondition is falsatisfied when it is active, is essential and has also been identified as a coNP-hard problem. To tame the hardness of the executability, we define a dynamic semantics for SPM based on a model which is proposed for defining domain state transition, present an encoding method by which the formal semantics is encoded into formulae as well as the executability, and propose a procedure which can bounded model check and diagnose the executability by using SAT solver. Our method has been implemented as a tool called SPMT and its validity is also illustrated through examples.