| Distributed computing, targeting at the study on distributed systems, has been a popular research topic in the field of computer science in recent years. Distributed systems have been widely applied in our daily life, including telecommunication networks, network applications such as peer-to-peer networks and real-time pro-cess control. Formal methods have been considered as an feasible and effective way to specify and verify distributed systems. Continuous attention is paid to the formal languages and process algebras or calculi on studying distributed systems.Parameterized Networks of Processes (pNets) is a machine-oriented semantic for-malism used for specifying and verifying the behaviour of distributed components or systems. In addition, it can be used to define the semantics of languages in the parallel and distributed computation area. Unlike other traditional process calculi, pNets only own one pNet node as an operator which composes all subnets running in parallel. Using this single synchronization artifact, it is capable of ex-pressing many operators or synchronization mechanisms. In this paper, we explore a denotational semantics for parameterized networks based on Unifying Theories of Programming. Also, we link our denotational semantics with the existing oper-ational semantics for pNets to discuss the consistency of the semantics. A set of algebraic laws is also explored based on the denotational semantics. Furthermore, we investigate the expressiveness of by encoding several operators in LOTOS and CSP, and some algebraic formulas as well. A number of algebraic laws extracted from those classical process algebras are proved by using our denotational seman-tics. |
PDF Full Text Request