A UTP semantics for communicating processes with shared variables

CSP# (Communicating Sequential Programs) is a modelling language designed for specifying concurrent systems by integrating CSP-like compositional operators with sequential programs updating shared variables. In this paper, we define an observation-oriented denotational semantics in an open environme...

Full description

Saved in:
Bibliographic Details
Main Authors: SHI, Ling, ZHAO, Yongxin, LIU, Yang, SUN, Jun, DONG, Jin Song, QIN, Shengchao
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2013
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4999
https://ink.library.smu.edu.sg/context/sis_research/article/6002/viewcontent/a_utp.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-6002
record_format dspace
spelling sg-smu-ink.sis_research-60022020-03-12T09:38:10Z A UTP semantics for communicating processes with shared variables SHI, Ling ZHAO, Yongxin LIU, Yang SUN, Jun DONG, Jin Song QIN, Shengchao CSP# (Communicating Sequential Programs) is a modelling language designed for specifying concurrent systems by integrating CSP-like compositional operators with sequential programs updating shared variables. In this paper, we define an observation-oriented denotational semantics in an open environment for the CSP# language based on the UTP framework. To deal with shared variables, we lift traditional event-based traces into hybrid traces which consist of event-state pairs for recording process behaviours. We also define refinement to check process equivalence and present a set of algebraic laws which are established based on our denotational semantics. Our approach thus provides a rigorous means for reasoning about the correctness of CSP# process behaviours. We further derive a closed semantics by focusing on special types of hybrid traces; this closed semantics can be linked with existing CSP# operational semantics. 2013-01-11T08:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/4999 info:doi/10.1007/978-3-642-41202-8_15 https://ink.library.smu.edu.sg/context/sis_research/article/6002/viewcontent/a_utp.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Shared Variable Open Semantic Parallel Composition Sequential Program Communicate Sequential Process Software Engineering
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Shared Variable
Open Semantic
Parallel Composition
Sequential Program
Communicate Sequential Process
Software Engineering
spellingShingle Shared Variable
Open Semantic
Parallel Composition
Sequential Program
Communicate Sequential Process
Software Engineering
SHI, Ling
ZHAO, Yongxin
LIU, Yang
SUN, Jun
DONG, Jin Song
QIN, Shengchao
A UTP semantics for communicating processes with shared variables
description CSP# (Communicating Sequential Programs) is a modelling language designed for specifying concurrent systems by integrating CSP-like compositional operators with sequential programs updating shared variables. In this paper, we define an observation-oriented denotational semantics in an open environment for the CSP# language based on the UTP framework. To deal with shared variables, we lift traditional event-based traces into hybrid traces which consist of event-state pairs for recording process behaviours. We also define refinement to check process equivalence and present a set of algebraic laws which are established based on our denotational semantics. Our approach thus provides a rigorous means for reasoning about the correctness of CSP# process behaviours. We further derive a closed semantics by focusing on special types of hybrid traces; this closed semantics can be linked with existing CSP# operational semantics.
format text
author SHI, Ling
ZHAO, Yongxin
LIU, Yang
SUN, Jun
DONG, Jin Song
QIN, Shengchao
author_facet SHI, Ling
ZHAO, Yongxin
LIU, Yang
SUN, Jun
DONG, Jin Song
QIN, Shengchao
author_sort SHI, Ling
title A UTP semantics for communicating processes with shared variables
title_short A UTP semantics for communicating processes with shared variables
title_full A UTP semantics for communicating processes with shared variables
title_fullStr A UTP semantics for communicating processes with shared variables
title_full_unstemmed A UTP semantics for communicating processes with shared variables
title_sort utp semantics for communicating processes with shared variables
publisher Institutional Knowledge at Singapore Management University
publishDate 2013
url https://ink.library.smu.edu.sg/sis_research/4999
https://ink.library.smu.edu.sg/context/sis_research/article/6002/viewcontent/a_utp.pdf
_version_ 1770575187207520256