Please use this identifier to cite or link to this item: https://hdl.handle.net/10356/138432
Full metadata record
DC FieldValueLanguage
dc.contributor.authorShi, Lingen_US
dc.contributor.authorZhao, Yongxinen_US
dc.contributor.authorLiu, Yangen_US
dc.contributor.authorSun, Junen_US
dc.contributor.authorDong, Jin Songen_US
dc.contributor.authorQin, Shengchaoen_US
dc.date.accessioned2020-05-06T02:56:18Z-
dc.date.available2020-05-06T02:56:18Z-
dc.date.issued2018-
dc.identifier.citationShi, L., Zhao, Y., Liu, Y., Sun, J., Dong, J. S., & Qin, S. (2018). A UTP semantics for communicating processes with shared variables and its formal encoding in PVS. Formal Aspects of Computing, 30, 351-380. doi:10.1007/s00165-018-0453-7en_US
dc.identifier.issn0934-5043en_US
dc.identifier.urihttps://hdl.handle.net/10356/138432-
dc.description.abstractCSP# (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 machine-assisted verification of CSP# specifications.en_US
dc.description.sponsorshipNRF (Natl Research Foundation, S’pore)en_US
dc.language.isoenen_US
dc.relation.ispartofFormal Aspects of Computingen_US
dc.rights© 2018 British Computer Society. All rights reserved. This paper was published in Formal Aspects of Computing and is made available with permission of British Computer Society.en_US
dc.subjectEngineering::Computer science and engineeringen_US
dc.titleA UTP semantics for communicating processes with shared variables and its formal encoding in PVSen_US
dc.typeJournal Articleen
dc.contributor.schoolSchool of Computer Science and Engineeringen_US
dc.identifier.doi10.1007/s00165-018-0453-7-
dc.identifier.scopus2-s2.0-85046010121-
dc.identifier.volume30en_US
dc.identifier.spage351en_US
dc.identifier.epage380en_US
dc.subject.keywordsUTPen_US
dc.subject.keywordsDenotational Semanticsen_US
item.grantfulltextnone-
item.fulltextNo Fulltext-
Appears in Collections:SCSE Journal Articles

SCOPUSTM   
Citations 20

5
Updated on Jul 11, 2022

PublonsTM
Citations 20

4
Updated on Jul 8, 2022

Page view(s)

91
Updated on Aug 16, 2022

Google ScholarTM

Check

Altmetric


Plumx

Items in DR-NTU are protected by copyright, with all rights reserved, unless otherwise indicated.