Jonathan Matthew Rodriguez
Formalization and Verification of Assurance Points by Means of Colored Petri Nets
As the use of web services continues to grow, the need for better recovery methods for software processes increases as well. A method that has been introduced to address recovery in service composition is the use of Assurance Points (APs). Using the idea of checkpoints and user-defined constraints, APs use integration rules as a way to check correctness conditions and to invoke backward and forward recovery actions, using APs as intermediate rollback points within a process. Although the concept of APs has been introduced, APs have not yet been formalized. This research focuses on using Colored Petri Nets (CPNs) to model the semantics of Assurance Points and its recovery functionality for rollback, retry, and cascaded contingency. The graphical notation and exact mathematical definition of CPNs make it a suitable tool to model information systems, verify whether the design operates correctly, and eliminate dead paths in a process flow. As part of this research, CPN models were first designed and tested for a service composition and recovery model. The models were then extended to define and verify Assurance Point semantics and to demonstrate AP recovery functionality by simulating errors and observing recovery response to errors. The CPN specification provides a formal definition of Assurance Points that clarifies the semantics of the recovery actions in the context of the service composition model.