Membrane Calculus: a formal method for Grid transactions

The research of transaction processing in Web Services and Grid Services is active in academic and engineering areas. However, the formal method of transaction processing has not been fully investigated in the literature. This paper proposes a preliminary theoretical model called Membrane Calculus based on Membrane Computing and Petri nets to formalize Grid transactions. Five kinds of transition rules in Membrane Calculus (including object rules and membrane rules) are introduced and the operational semantics of transition rules are defined. Then, a typical long-running transaction example is presented to demonstrate the use of Membrane Calculus. Finally, the rewriting logic tool Maude is adopted to specify and execute the specification of this example. Copyright (c) 2006 John Wiley & Sons, Ltd.