A UTP semantics for communicating processes with shared variables
Shi, L. Zhao, Y. Liu, Y. Sun, J. Dong, J.S. Qin, S.
Shi, L.
Zhao, Y.
Liu, Y.
Sun, J.
Qin, S.
Citations
Altmetric:
Alternative Title
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. © 2013 Springer-Verlag.
Keywords
Source Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher
Series/Report No.
Collections
Rights
Date
2013
DOI
10.1007/978-3-642-41202-8_15
Type
Conference Paper