UTP Semantics for rTiMo

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2017
• 出版时间：2017
• 年：2017
• 卷：10134
• 期：1
• 页码：176-196
• 丛书名：Unifying Theories of Programming
• ISBN：978-3-319-52228-9
• 卷排序：10134

文摘

rTiMo is a real-time version of TiMo (Timed Mobility), which is a process algebra for mobile distributed systems. In this paper, we investigate the denotational semantics for rTiMo. A trace variable tr is introduced to record the communications among processes as well as the location where the communication action takes place. Based on the formalized model, we study a set of algebraic laws, especially the laws about the migration and communication with real-time constraints. In order to facilitate the algebraic reasoning about the parallel expansion laws, we enrich rTiMo with a form of \(guarded \ choice\). This enables us to convert every parallel construct to a guarded choice.