Publication Type

Journal Article

Version

publishedVersion

Publication Date

4-2018

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 machineassisted verification of CSP# specifications

Keywords

UTP, Denotational semantics, Shared variables, Encoding

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Formal Aspects of Computing

Volume

30

First Page

351

Last Page

380

ISSN

0934-5043

Publisher

Springer (part of Springer Nature): Springer Open Choice Hybrid Journals

Embargo Period

4-25-2021

Copyright Owner and License

Authors

Additional URL

https://doi.org/10.1007%2Fs00165-018-0453-7

Download

Share

COinS