a concurrent temporal programming model with atomic blocks

ISCAS OpenIR

	a concurrent temporal programming model with atomic blocks
	Yang Xiaoxiao; Zhang Yu; Fu Ming; Feng Xinyu
	2012
会议名称	14th International Conference on Formal Engineering Methods, ICFEM 2012
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	22-37
会议日期	November 12, 2012 - November 16, 2012
会议地点	Kyoto, Japan
收录类别	EI
ISSN	0302-9743
ISBN	9783642342806
部门归属	(1) State Key Laboratory of Computer Science Institute of Software Chinese Academy of Sciences Beijing China; (2) University of Science and Technology of China Hefei China
摘要	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 interval 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 practical concurrent programs. © 2012 Springer-Verlag.; 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 interval 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 practical concurrent programs. © 2012 Springer-Verlag.
关键词	Logic Programming Temporal Logic
主办者	Natl. Inst. Adv. Ind. Sci. Technol. (AIST); Res. Cent. Softw. Verif., Japan Adv. Inst. Sci. Technol. (JAIST)
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15859
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Yang Xiaoxiao,Zhang Yu,Fu Ming,et al. a concurrent temporal programming model with atomic blocks[C],2012:22-37.