A UTP semantics for communicating processes with shared variables and its formal encoding in PVS

Ling Shi, Yongxin Zhao, Yang Liu, Jun Sun, Jin Song Dong, Shengchao Qin

Research output: Contribution to journalArticleResearchpeer-review

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.
Original languageEnglish
Pages (from-to)351-380
Number of pages30
JournalFormal Aspects of Computing
Volume30
Issue number3-4
Early online date25 Apr 2018
DOIs
Publication statusPublished - 1 Aug 2018

Fingerprint

Denotational Semantics
Encoding
Semantics
Trace
Concurrent Systems
Interleaving
Modeling Language
Concurrency
Merging
Updating
Refinement
Equivalence
Specification
Specifications
Communication
Operator
Theorem

Cite this

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. In: Formal Aspects of Computing. 2018 ; Vol. 30, No. 3-4. pp. 351-380.
@article{b0b2f8eb558441d7ba302a005158faa9,
title = "A UTP semantics for communicating processes with shared variables and its formal encoding in PVS",
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.",
author = "Ling Shi and Yongxin Zhao and Yang Liu and Jun Sun and Dong, {Jin Song} and Shengchao Qin",
year = "2018",
month = "8",
day = "1",
doi = "10.1007/s00165-018-0453-7",
language = "English",
volume = "30",
pages = "351--380",
journal = "Formal Aspects of Computing",
issn = "1433-299X",
publisher = "Springer Verlag",
number = "3-4",

}

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.

In: Formal Aspects of Computing, Vol. 30, No. 3-4, 01.08.2018, p. 351-380.

Research output: Contribution to journalArticleResearchpeer-review

TY - JOUR

T1 - A UTP semantics for communicating processes with shared variables and its formal encoding in PVS

AU - Shi, Ling

AU - Zhao, Yongxin

AU - Liu, Yang

AU - Sun, Jun

AU - Dong, Jin Song

AU - Qin, Shengchao

PY - 2018/8/1

Y1 - 2018/8/1

N2 - 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.

AB - 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.

UR - https://doi.org/10.1007/s00165-018-0453-7

U2 - 10.1007/s00165-018-0453-7

DO - 10.1007/s00165-018-0453-7

M3 - Article

VL - 30

SP - 351

EP - 380

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 1433-299X

IS - 3-4

ER -