Information Technology Reference
In-Depth Information
Compensable Programs
He Jifeng
Software Engineering Institute
East China Normal University, Shanghai
Abstract. Transaction-based services are increasingly being applied in
solving many universal interoperability problems. Compensation is one
typical feature for long-running transactions. This paper presents a de-
sign matrix model for specifying the behaviour of compensable programs
and provides new healthiness conditions to capture these new program-
ming features. The new model for handling exception and compensation
is built as conservative extension of the standard relational model in the
sense that the algebraic laws presented in [14] remain valid. The paper
also shows that the design matrix model is a retract of the design model.
1
Introduction
With the development of Internet technology, web services and web-based appli-
cations play an important role to information systems. The aim of web services
is to achieve the universal interoperability between different web-based appli-
cations. Due to the provided interface, web services can be invoked across the
Internet. In recent years, in order to develop web-based information systems
and describe the infrastructure for carrying out business transactions, various
business modelling languages have been introduced, such as XLANG, WSFL,
BPEL4WS (BPEL) and StAC [24,15,9,7].
Compensation is one typical feature for long-running transactions. Butler
et al. have investigated the compensation feature in the style of process al-
gebra CSP [6,7,8], namely compensating CSP. The operational semantics and
trace semantics have been studied [8]. The compensation is expressed as P
Q ,
where P is the forward process and Q is its associated compensation behaviour.
StAC (Structured Activity Compensation) [6] is a business process modelling
language, where compensation acts as one of its main features. Its operational
semantics has also been studied in [7]. Meanwhile, the combination of StAC and
B method has been explored, which can provide the precise description of busi-
ness transactions. Further, Bruni et al. have studied the transaction calculi for
StAC programs. The long-running transactions were discussed, and a process
calculi was provided in the form of Java API, namely Java Transactional Web
Services [4]. Qiu et al. have provided a deep formal analysis of the fault be-
haviour for BPEL-like processes [22]. Pu et al. have formalized the operational
semantics for BPEL [21], where bisimulation has been considered.
รท
This work was supported by the National Basic Research Program of China (Grant
No. 2005CB321904).
 
Search WWH ::




Custom Search