A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
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 work, we define an observation-oriented denotational semantics in an open environmen...
Saved in:
Main Authors: | , , , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2018
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/5902 https://ink.library.smu.edu.sg/context/sis_research/article/6908/viewcontent/Shi2018_Article_AUTPSemanticsForCommunicatingP.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-6908 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-69082021-04-26T03:09:46Z A UTP semantics for communicating processes with shared variables and its formal encoding in PVS 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 work, 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 mixed traces which consist of state-event pairs for recording process behaviours. To capture all possible concurrency behaviours between action/channel-based communications and global shared variables, we construct a comprehensive set of rules on merging traces from processes which run in parallel/interleaving. We also define refinement to check process equivalence and present a set of algebraic laws which are established based on our denotational semantics. We further encode our proposed denotational semantics into the PVS theorem prover. The encoding not only ensures the semantic consistency, but also builds up a theoretic foundation for machineassisted verification of CSP# specifications 2018-04-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/5902 https://ink.library.smu.edu.sg/context/sis_research/article/6908/viewcontent/Shi2018_Article_AUTPSemanticsForCommunicatingP.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 UTP Denotational semantics Shared variables Encoding Programming Languages and Compilers Software Engineering |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
UTP Denotational semantics Shared variables Encoding Programming Languages and Compilers Software Engineering |
spellingShingle |
UTP Denotational semantics Shared variables Encoding Programming Languages and Compilers Software Engineering SHI, Ling ZHAO, Yongxin LIU, Yang SUN, Jun DONG, Jin Song QIN, Shengchao A UTP semantics for communicating processes with shared variables and its formal encoding in PVS |
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 work, 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 mixed traces which consist of state-event pairs for recording process behaviours. To capture all possible concurrency behaviours between action/channel-based communications and global shared variables, we construct a comprehensive set of rules on merging traces from processes which run in parallel/interleaving. We also define refinement to check process equivalence and present a set of algebraic laws which are established based on our denotational semantics. We further encode our proposed denotational semantics into the PVS theorem prover. The encoding not only ensures the semantic consistency, but also builds up a theoretic foundation for machineassisted verification of CSP# specifications |
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 and its formal encoding in PVS |
title_short |
A UTP semantics for communicating processes with shared variables and its formal encoding in PVS |
title_full |
A UTP semantics for communicating processes with shared variables and its formal encoding in PVS |
title_fullStr |
A UTP semantics for communicating processes with shared variables and its formal encoding in PVS |
title_full_unstemmed |
A UTP semantics for communicating processes with shared variables and its formal encoding in PVS |
title_sort |
utp semantics for communicating processes with shared variables and its formal encoding in pvs |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2018 |
url |
https://ink.library.smu.edu.sg/sis_research/5902 https://ink.library.smu.edu.sg/context/sis_research/article/6908/viewcontent/Shi2018_Article_AUTPSemanticsForCommunicatingP.pdf |
_version_ |
1770575659134877696 |