Compensation by design

ISCAS OpenIR

	Compensation by design
	Liu, Xi (1); Yang, Shaofa (2); Sanders, J.W. (3); Liu, X.(williamxliu@gmail.com)
	2014
发表期刊	Formal Aspects of Computing
ISSN	9345043
卷号	26 期号:4 页码:623-676
摘要	The current dominance of the service-based paradigm reflects the success of specific design and architectural principles embodied in terms like SOA and REST. This paper suggests further principles for the design of services exhibiting long-running transactions (that is, transactions whose characteristic feature is that in the case of failure not all system states can be automatically restored: system compensation is required). The principles are expressed at the level of scope-based compensation and fault handling, and ensure the consistency of data critical to the business logic. They do so by demanding (a) either the commitment of all of the transaction or none of it, and (b) that compensation is assured in case of failure in 'parent' transactions. The notion of scope is captured algebraically (rather than semantically) in order to express design guidelines which ensure that a given transaction satisfies those principles. Transactional processes are constructed by parallel composition of services, and transactions with scopes in a single service are dealt with as a special case. The system semantics is formalised as a transition system (in Z) and the principles are expressed as formulae in linear temporal logic over runs of the transition system. That facilitates the model checking (using SAL) of their bounded versions. Two simple examples are used throughout to illustrate definitions and finally to demonstrate the approach. © 2013 British Computer Society.; The current dominance of the service-based paradigm reflects the success of specific design and architectural principles embodied in terms like SOA and REST. This paper suggests further principles for the design of services exhibiting long-running transactions (that is, transactions whose characteristic feature is that in the case of failure not all system states can be automatically restored: system compensation is required). The principles are expressed at the level of scope-based compensation and fault handling, and ensure the consistency of data critical to the business logic. They do so by demanding (a) either the commitment of all of the transaction or none of it, and (b) that compensation is assured in case of failure in 'parent' transactions. The notion of scope is captured algebraically (rather than semantically) in order to express design guidelines which ensure that a given transaction satisfies those principles. Transactional processes are constructed by parallel composition of services, and transactions with scopes in a single service are dealt with as a special case. The system semantics is formalised as a transition system (in Z) and the principles are expressed as formulae in linear temporal logic over runs of the transition system. That facilitates the model checking (using SAL) of their bounded versions. Two simple examples are used throughout to illustrate definitions and finally to demonstrate the approach. © 2013 British Computer Society.
收录类别	SCI ; EI
关键词	Service Computing Long-running Transaction Compensation Temporal Logic
部门归属	(1) State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing, China; (2) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (3) African Institute for Mathematical Sciences, Muizenberg and Stellenbosch University, Stellenbosch, South Africa
语种	英语
WOS记录号	WOS:000339105100001
引用统计
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/16851
专题	中国科学院软件研究所
通讯作者	Liu, X.(williamxliu@gmail.com)
推荐引用方式 GB/T 7714	Liu, Xi ,Yang, Shaofa ,Sanders, J.W. ,et al. Compensation by design[J]. Formal Aspects of Computing,2014,26(4):623-676.
APA	Liu, Xi ,Yang, Shaofa ,Sanders, J.W. ,&Liu, X..(2014).Compensation by design.Formal Aspects of Computing,26(4),623-676.
MLA	Liu, Xi ,et al."Compensation by design".Formal Aspects of Computing 26.4(2014):623-676.