Japan Advanced Institute of Science and Technology

Japan Advanced Institute of Science and Technology

JAIST Repository

https://dspace.jaist.ac.jp/

Title

Author(s)

Citation

Issue Date

Type

Text version

URL

Rights

Description

with Ambient Calculus

Satoshi Mineshita

Scho ol of Information Science,

Japan Advanced Institute of Science and Technology

February 15, 1999

Keywords: formal semantics, mobile agent, calculus.

Abstract

Introduction

Studiesonformalsemanticsofdistributedprogramminglanguagesanditsrelatedresearch

topics are getting important these days. Formal semantics is necessary in order to truly

understand the natureof aprogramming language and the behaviorof programs written

inthelanguage. Therefore,theexactdescriptionofsemanticsindistributedprogramming

languages is urgent, and it is connected to the development of distributed softwares by

this exact description.

The purpose of this study is to give it formal models, specications of the various

motions of realistic mobile agents. In this study, specially, it thinks about the various

motions of mobile agents when physically cutting of the communication happened, and

twoformalizationof the faulttolerance andthe disconnectedoperationare decidedtob e

done.

The disconnected operation handlesthe process of keepingthe work,while the result

is always returned in the middle p oint. The fault tolerance handles the result which the

emergency process operates, when the communication is not taken in point of time in

whichthe countdown ended.

Mobile Agent

Mobile agentsare programs thatmoveandexecute onthenetworkwithdata, andagents

that do es the agency of pro cessing of the addressee in remote process. There are many

Copyright c

1999bySatoshiMineshita

mobileagent,andwhentheyareincluded, itthinks howdisconnectedoperationand fault

tolerance are included. Actually, eachmobile agentlanguage is developeda various view

andhavethedierentstyle. But,thethingwhichhadtherecoveryfunctionwhenadevice

trouble and atrouble occurredis still dicult, and itis a future research subject.

Calculus that amobile agentis expressed musthave itsexpression whichhas charac-

teristicsb einglookedforintheabove. Asforcommunication,CCS(CalculusofCommuni-

catingSystems)whichare formalmodelsoftheparallelcomputingexists,andPI-calculus

that the movement of processes is represented as the movement of a channels that refer

toprocessesexists. AmbientCalculus whichwasunderlainconcepts and techniquesof -

calculusmakesamovemento ccur onambientand allwhichisthe bounded placedwhich

a calculation occurs in, and it thought that its technique was suitable for expressing a

mobile agent,and we did researchinthis cause.

Formal Semantics

Howtodescribethesemanticofprogramlanguagesstrictlybythemathematicalorformal

logical system is the formal semantics of programming languages, by this, the standard-

ization of program languages, the verication of correctness, the exact description of

specications, the automatic generation of processors can be done.

In this study, we was used operational semantics that express the semantic of pro-

gramming languages by giving it the abstract machine which has the structure that the

eect of program languages can be judged.

Ambient Calculus

AmbientCalculus tousebythis studyhasitsexpressionwhichcan mo delrewallaccess,

numerals, Turing machine by using the concept of ambient and the peculiar action that

is entering,exiting, opening upan ambient.

Furthermore,by adding the concept of the interpro cesscommunication, it makes en-

coding of -calculus possible, and it isshown thatan expression ishigh.

Representation of Mobile Agents

Inthis study,wedeneacountdown,working impossibilitycondition andbyusingthese,

the semanticof twocondition is decidedto be givento it.

One of those is disconnectedoperation of mobile agents. In this study, it is thinking

about the process that the work is continued with returning always a result on the way.

As anexample, The case that it is indicated how much work a mobile agent during the

work nishes atpresentin the transmittingcause is presumed.

Route conrmation between ambients, a base for the data transmission , a base for

the data deliveryone byone, transmittingdata are dened,byusing these, disconnected

sendingof dataisdone and whenitcannotcommunicate,beforesendingdata,itismade

work impossibility condition, and made the condition that it waits for the next sending

data is dened.

Another ofthoseisfaulttolerance inphysicallycuttinginmobileagents. Whenphys-

ically cutting happens, a countdown is done because the judgmentof p ermanent cutting

or temp orary cutting is dicult, and when a countdown was nished, if communication

cannot b etaken, the process for the emergency starts and faulttolerance isdone.

A base for the round agent, a round agent are dened, and it is dened that fault

tolerance is done when this round agent is made to work continuously and round agent

doesn't come back tothe base.

Conrmation of motions

Motionofthemotionimpossibilityconditionandtheabovetwodenitionsareconrmed,

and it ascertains that amotion as the specications is done.

Reductions are done,and vericationsare done by conrmingachangeinthat condi-

tion.

Conclusion

The motion of the actual mobile agent could be expressed by Ambient Calculus which

had only primitiveelement.

As that result,the base toexamine the behavior of the distributed calculation math-

ematicallycould be made, and moreoverthe AmbientCalculus' own expressioncould be

conrmed.