A temporal programming model with atomic blocks based on projection temporal logic

ISCAS OpenIR

	A temporal programming model with atomic blocks based on projection temporal logic
	Yang, Xiaoxiao (1); Zhang, Y. (1); Fu, Ming (2); Feng, Xinyu (2); Yang, Xiaoxiao
	2014
发表期刊	Frontiers of Computer Science
ISSN	20952228
摘要	Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model (αPTL) which extends the projection temporal logic (PTL) to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.; Atomic blocks, a high-level language construct that allows programmers to explicitly specify the atomicity of operations without worrying about the implementations, are a promising approach that simplifies concurrent programming. On the other hand, temporal logic is a successful model in logic programming and concurrency verification, but none of existing temporal programming models supports concurrent programming with atomic blocks yet. In this paper, we propose a temporal programming model (αPTL) which extends the projection temporal logic (PTL) to support concurrent programming with atomic blocks. The novel construct that formulates atomic execution of code blocks, which we call atomic interval formulas, is always interpreted over two consecutive states, with the internal states of the block being abstracted away. We show that the framing mechanism in projection temporal logic also works in the new model, which consequently supports our development of an executive language. The language supports concurrency by introducing a loose interleaving semantics which tracks only the mutual exclusion between atomic blocks. We demonstrate the usage of αPTL by modeling and verifying both the fine-grained and coarse-grained concurrency.
收录类别	EI
部门归属	(1) State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China; (2) Suzhou Institute for Advanced Study University of Science & Technology of China, SuZhou, China
语种	英语
WOS记录号	WOS:000345385900005
引用统计	被引频次：1[WOS] [WOS记录] [WOS相关记录]
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/17012
专题	中国科学院软件研究所
通讯作者	Yang, Xiaoxiao
推荐引用方式 GB/T 7714	Yang, Xiaoxiao ,Zhang, Y. ,Fu, Ming ,et al. A temporal programming model with atomic blocks based on projection temporal logic[J]. Frontiers of Computer Science,2014.
APA	Yang, Xiaoxiao ,Zhang, Y. ,Fu, Ming ,Feng, Xinyu ,&Yang, Xiaoxiao.(2014).A temporal programming model with atomic blocks based on projection temporal logic.Frontiers of Computer Science.
MLA	Yang, Xiaoxiao ,et al."A temporal programming model with atomic blocks based on projection temporal logic".Frontiers of Computer Science (2014).