Model checking for BPEL4WS based on timed Ambient
Chunming Gao · Jisuanji gongcheng yu sheji · 2008
The Mobile Ambient calculus presented by Luca Cardelli is a formalism for describing the mobility of both process and mobile device, but the real-time property of the mobility has not been well described. Discrete time Mobile Ambient calculus (DTMA) is presented, which is extended by Mobile Ambient calculus with time. Based on a subset of the modal logic for DTMA, a model checking algorithm for DTMA is proposed. Finally an approach for modeling BPEL4WS is presented and by this method the model checking for reachability of the action in business process is implemented.