A UTP approach for rTiMo

Wanling Xie; Shuangqing Xiang; Huibiao Zhu

doi:10.1007/s00165-018-0467-1

A UTP approach for rTiMo

Wanling Xie, Shuangqing Xiang, Huibiao Zhu^*

^*Corresponding author for this work

Software Engineering Institute

Research output: Contribution to journal › Article › peer-review

8 Scopus citations

Abstract

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 guardedchoice. This can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.

Original language	English
Pages (from-to)	713-738
Number of pages	26
Journal	Formal Aspects of Computing
Volume	30
Issue number	6
DOIs	https://doi.org/10.1007/s00165-018-0467-1
State	Published - 1 Nov 2018

Keywords

Hoare logic
Mobile systems
UTP semantics
rTiMo

Access to Document

10.1007/s00165-018-0467-1

Cite this

@article{9458b76d593e4574aaa1a2b6caad7b94,

title = "A UTP approach for rTiMo",

abstract = "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 guardedchoice. This can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.",

keywords = "Hoare logic, Mobile systems, UTP semantics, rTiMo",

author = "Wanling Xie and Shuangqing Xiang and Huibiao Zhu",

note = "Publisher Copyright: {\textcopyright} 2018, British Computer Society.",

year = "2018",

month = nov,

day = "1",

doi = "10.1007/s00165-018-0467-1",

language = "英语",

volume = "30",

pages = "713--738",

journal = "Formal Aspects of Computing",

issn = "0934-5043",

publisher = "Association for Computing Machinery (ACM)",

number = "6",

}

TY - JOUR

T1 - A UTP approach for rTiMo

AU - Xie, Wanling

AU - Xiang, Shuangqing

AU - Zhu, Huibiao

PY - 2018/11/1

Y1 - 2018/11/1

N2 - 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 guardedchoice. This can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.

AB - 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 guardedchoice. This can enable us to convert every parallel program to the guarded choice form. Moreover, we also provide a set of proof rules, which can be used to verify the correctness and real-time properties of programs.

KW - Hoare logic

KW - Mobile systems

KW - UTP semantics

KW - rTiMo

UR - https://www.scopus.com/pages/publications/85051710163

U2 - 10.1007/s00165-018-0467-1

DO - 10.1007/s00165-018-0467-1

M3 - 文章

AN - SCOPUS:85051710163

SN - 0934-5043

VL - 30

SP - 713

EP - 738

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

IS - 6

ER -

A UTP approach for rTiMo

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this