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 |
| 会议日期 | November 12, 2012 - November 16, 2012 |
| 会议地点 | Kyoto, Japan |
| 关键词 | Logic programming Temporal logic |
| 页码 | 22-37 |
| 中文摘要 | 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. |
| 收录类别 | EI |
| 会议主办者 | Natl. Inst. Adv. Ind. Sci. Technol. (AIST); Res. Cent. Softw. Verif., Japan Adv. Inst. Sci. Technol. (JAIST) |
| 会议录 | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
 |
| 语种 | 英语 |
| ISSN号 | 0302-9743 |
| ISBN号 | 9783642342806 |
| 源URL | [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]. 见:14th International Conference on Formal Engineering Methods, ICFEM 2012. Kyoto, Japan. November 12, 2012 - November 16, 2012. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。