A UTP semantics for communicating processes with shared variables and its formal encoding in PVS

DOI10.1007/S00165-018-0453-7MaRDI QIDQ1798665zbMATH OpenOpenAlexWikidataFDO

Authors Ling Shi, Yongxin Zhao, Yang Liu, Jun Sun, Shengchao Qin, Jin-Song Dong

Publication date 23 October 2018

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10072/381740

zbMATH Keywords

denotational semanticsencodingshared variablesUTP

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• UTCP: Compositional Semantics for Shared-Variable Concurrency
• Communicating Sequential Processes. The First 25 Years
• Denotational semantics of communicating sequential programs
• Symbolic analysis tools for CSP
• scientific article; zbMATH DE number 3890713

Cites work

• A UTP semantics for \textsf{Circus}
• CSP theorems for communicating B machines
• CSP with Hierarchical State
• Deep semantic links of TCSP and Object-Z: TCOZ approach.
• Full abstraction for a shared-variable parallel language
• scientific article; zbMATH DE number 439891 (Why is no real title available?)
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 2080001 (Why is no real title available?)
• scientific article; zbMATH DE number 1852174 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3278860 (Why is no real title available?)
• Isabelle. A generic theorem prover
• Laws of programming
• Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
• Proof principles of CSP -- CSP-prover in practice
• The stable revivals model in CSP-Prover
• Tools and Algorithms for the Construction and Analysis of Systems
• Unifying theories in Isabelle/HOL
• Unifying Theories in ProofPower-Z
• Unifying theories of programming in Isabelle

Cited in

(7)

• A UTP approach for rTiMo
• Angelic processes for CSP via the UTP
• A process calculus BigrTiMo of mobile systems and its formal semantics
• Theoretical and practical approaches to the denotational semantics for MDESL based on UTP
• UTCP: Compositional Semantics for Shared-Variable Concurrency
• Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs
• An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency

Describes a project that uses

Uses Software

• Isabelle
• ProofPower
• PAT
• PTSC
• Circus
• TCOZ
• Coq
• CSP-prover
• ML
• PVS
• HOL

This page was built for publication: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1798665)