Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-41202-8_15
Title: A UTP semantics for communicating processes with shared variables
Authors: Shi, L.
Zhao, Y.
Liu, Y.
Sun, J.
Dong, J.S. 
Qin, S.
Issue Date: 2013
Source: Shi, L.,Zhao, Y.,Liu, Y.,Sun, J.,Dong, J.S.,Qin, S. (2013). A UTP semantics for communicating processes with shared variables. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8144 LNCS : 215-230. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-41202-8_15
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.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/77992
ISBN: 9783642412011
ISSN: 03029743
DOI: 10.1007/978-3-642-41202-8_15
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.

SCOPUSTM   
Citations

4
checked on Feb 21, 2018

Page view(s)

20
checked on Feb 17, 2018

Google ScholarTM

Check

Altmetric


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.