Abstract

OMG has provided a set of Common Object Services (COS), which help the users to build large-scale distributed CORBA applications. One of the most important CORBA services defined by OMG is the Object Transaction Service (OTS), which augments CORBA object model with the notion of distributed transactions. The implementation design of the OTS is critical for the service to be effective in applications. Temporal Petri nets enhance greatly the modeling and analyzing power of Petri nets. The dynamic behavior of a given system and causality in events are elegantly described by formulae containing temporal operators. A three-tier formal model with OTS is presented by temporal colored Petri nets in the present study, and the functional correctness of the transaction processing model is analyzed and verified using the reasoning rules of temporal logic and reachability graph.

Paper Details