Discrete Real Time Mobile Ambients

With the development of the technology of computer andnetwork, the mobile computation and the real time computationhave become the focus in computer science, and more and moreresearchers have focused on them. For the same problem, theresearchers in various fields have different research methods.The formal method is an important method for the distributedand parallel computation. In recent years, the formal methodis developed quickly. Many formal methods which can used toresearch the mobile computation and real time computation arepresented. Such as automata, Petri net, CCS, Pi-calculus andMobile Ambients. These formal method can be used to describeand research distributed system, translating value computationand space mobile computation. However, each of them has theirown character, for example, the Pi-calculus is suitable tomodel translating value computation; however the MobileAmbients does well in describing space mobile computation. Thereal time computation is another focus in computer science, andthe formal experts also have presented some formal frameworksfor real time computation. Most of these real time formalframeworks are got by extending formal framework without real time with time. The new formal systems can be used to researchthe computer systems' properties in time. The existing realtime formal systems include timed automata, timed CCS, realtime Pi-calculus and so on. But these real time formal systemscan't describe space structure, for the weakness of itsprototype. If we can extend Mobile Ambients with real time, thenthe space and the time will be researched in a unified formalframework.In this paper, we discussed the excellence and shortcomingof mobile ambients firstly. And then we presented a real timemobile computation model based on graphs. Following, weextended the mobile ambients with time, and presented a new realtime formal system——discrete real time mobile ambients. Whenwe check a system, not only the system should be model withformal language, but the properties that the system needsatisfy should be described with modal logic. In order to modeland check the real time computation system with discrete realtime mobile ambients, we extended the temper logic for mobileambients with time and presented the modal logic which candescribe the real time property. Finally, we presented themodel checking algorithm for sub-set of discrete real timemobile ambients, and model web services composite language BPEL4WS with discrete real time mobile ambients.Our paper consists of the following chapters:Firstly, we introduced mobile ambients, and presented thereal mobile computation model based on graphs.Secondly, we extended the mobile ambients with time andpresented a new real time formal method——the discrete timemobile ambients.Thirdly, we presented the temper logic for discrete timemobile ambients, and we presented the model checking algorithmfor discrete time mobile ambients. We proved that our algorithmis decidable.Fourthly, we used the discrete time mobile ambients tocheck a web service system.Finally, we summarized our work and introduced our futurework.