Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/138432
Title: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
Authors: Shi, Ling
Zhao, Yongxin
Liu, Yang
Sun, Jun
Dong, Jin Song
Qin, Shengchao
Keywords: Engineering::Computer science and engineering
Issue Date: 2018
Source: Shi, L., Zhao, Y., Liu, Y., Sun, J., Dong, J. S., & Qin, S. (2018). A UTP semantics for communicating processes with shared variables and its formal encoding in PVS. Formal Aspects of Computing, 30, 351-380. doi:10.1007/s00165-018-0453-7
Journal: Formal Aspects of Computing
Abstract: 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 machine-assisted verification of CSP# specifications.
URI: https://hdl.handle.net/10356/138432
ISSN: 0934-5043
DOI: 10.1007/s00165-018-0453-7
Rights: © 2018 British Computer Society. All rights reserved. This paper was published in Formal Aspects of Computing and is made available with permission of British Computer Society.
Fulltext Permission: none
Fulltext Availability: No Fulltext
Appears in Collections:SCSE Journal Articles

SCOPUSTM   
Citations 20

4
Updated on Mar 10, 2021

PublonsTM
Citations 20

3
Updated on Mar 4, 2021

Page view(s)

83
Updated on Jul 3, 2022

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.