Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

1-2013

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

Keywords

Shared Variable, Open Semantic, Parallel Composition, Sequential Program, Communicate Sequential Process

Discipline

Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, October 29 - November 1

First Page

215

Last Page

230

ISBN

9783642412011

Identifier

10.1007/978-3-642-41202-8_15

Publisher

Springer Link

City or Country

Queenstown, New Zealand

Additional URL

https://doi.org/10.1007/978-3-642-41202-8_15

Download

Share

COinS