Compensation by design

CORC > 软件研究所 > 软件所图书馆 > 期刊论文

	Compensation by design
	Liu, Xi (1) ; Yang, Shaofa (2) ; Sanders, J.W. (3)
刊名	Formal Aspects of Computing
	2014
卷号	26 期号:4 页码:623-676
关键词	Service computing Long-running transaction Compensation Temporal logic
ISSN号	9345043
通讯作者	Liu, X.(williamxliu@gmail.com)
中文摘要	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
语种	英语
WOS记录号	WOS:000339105100001
公开日期	2014-12-16
内容类型	期刊论文
源URL	[http://ir.iscas.ac.cn/handle/311060/16851]
专题	软件研究所_软件所图书馆_期刊论文
推荐引用方式 GB/T 7714	Liu, Xi ,Yang, Shaofa ,Sanders, J.W. . Compensation by design[J]. Formal Aspects of Computing,2014,26(4):623-676.
APA	Liu, Xi ,Yang, Shaofa ,&Sanders, J.W. .(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.