Process Calculus BigrTiMo Of Mobile Distributed Systems And Its Formal Semantics

The computing in mobile distributed systems provides high-quality information services to mobile users located at different locations,and it has been widely used in a variety of domains,ranging from education and research,to national defense and military,to transportation and aerospace.The mobility and the environment of mobile computing may significantly influence the quality of communication,which may lead to communication interruption.Motivated by this,how to describe the mobility and the environment and how to increase the quality of services become an important issue.In this thesis,we use formal methods to study mobile distributed systems,and propose the process calculus Bigr Ti Mo for mobile distributed systems.Compared with the exsiting calculus for mobile distributed systems,our calculus not only can capture the mobility,but also can describe the spatial structure and time constraint.This thesis investigates the operational semantics of the Bigr Ti Mo calculus and develops an executable formal specification of Bigr Ti Mo calculus using Maude.Based on the Unifying Theories Programming proposed by Professors C.A.R.Hoare(Turing Award Winner)and Jifeng He,this thesis explores the denotational semantics,algebraic semantics and semantic linking theory for the Bigr Ti Mo calculus.We mainly explore how the algebraic semantics relates with the operational semantics and denotational semantics.Based on Hoare Logic,this thesis investigates the proof system of Bigr Ti Mo calculus allowing us to prove program correctness.The main contributions of this thesis inculude:· We present a process calculus for mobile distributed systems called Bigr Ti Mo,which combines r Ti Mo calculus and Bigraph model proposed by Professor Robin Milner(Turing Award Winner).r Ti Mo calculus only can model the local communication,in order to model the remote communication,we extend the r Ti Mo model into Bigr Ti Mo by introducing the Bigraph model.Bigr Ti Mo calculus not only can model the mobility,but also can model the spatial structure and time constraint.· We investigate the formal semantic models for Bigr Ti Mo calculus,including the operational semantics,denotational semantics,algebraic semantics and proof system.The operational semantics suggests a complete set of possible individual steps which may be taken in its execution.Based on the rewrting engine Maude,we implement our calculus and verify mobile distributed systems.The approach of denotational semantics is under a purely mathematical basis.Compared with operational semantics,denotational semantics is more abstract and expresses what a program does.Algebraic semantics consists of a set of algebraic laws,in order to support our algebraic expansion laws,we introduce a new concept called guarded choice.Based on denotational semantics,we prove the soundness of the algebraic laws.A proof system provides a set of proof rules,which can be used to specify and verify program correctness.We prove the soundness of the proof system and illustrate the applications of our approach.· We explore the semantic linking theory.We mainly work on how to derive the operational semantics and denotational semantics from algebraic semantics.In order to define the derivation strategy,we introduce the concept of head normal form.We prove the equivelence between the derived transition system(i.e.,the operational semantics)and the derivation strategy,which indicates that the operational semantics is sound and complete.