@inproceedings{f151bb2b5a9a411db11880a8bcd00dd5,
title = "A UTP semantics for communicating processes with shared variables",
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.",
author = "Ling Shi and Yongxin Zhao and Yang Liu and Jun Sun and Dong, \{Jin Song\} and Shengchao Qin",
year = "2013",
doi = "10.1007/978-3-642-41202-8\_15",
language = "英语",
isbn = "9783642412011",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "215--230",
booktitle = "Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods, ICFEM 2013, Proceedings",
note = "15th International Conference on Formal Engineering Methods, ICFEM 2013 ; Conference date: 29-10-2013 Through 01-11-2013",
}