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

DOI10.1007/s00165-018-0453-7zbMath1398.68373OpenAlexW2799615765MaRDI QIDQ1798665

Jun Sun, Ling Shi, Yang Liu, Yongxin Zhao, 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 semanticsencodingUTPshared variables

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)

Related Items

A UTP approach for rTiMo, Theoretical and practical approaches to the denotational semantics for MDESL based on UTP, Angelic processes for CSP via the UTP, A process calculus BigrTiMo of mobile systems and its formal semantics

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
• A UTP semantics for \textsf{Circus}
• Isabelle. A generic theorem prover
• Deep semantic links of TCSP and Object-Z: TCOZ approach.
• Full abstraction for a shared-variable parallel language
• CSP theorems for communicating B machines
• Unifying Theories of Programming in Isabelle
• Unifying Theories in Isabelle/HOL
• CSP with Hierarchical State
• Laws of programming
• The Stable Revivals Model in CSP-Prover
• Proof Principles of CSP – CSP-Prover in Practice
• Unifying Theories in ProofPower-Z
• Tools and Algorithms for the Construction and Analysis of Systems