91 Pages
English

Abstract Interpretation of Mobile Systems

-

Gain access to the library to view online
Learn more

Description

Abstract Interpretation of Mobile Systems 1 Jerome Feret Departement d'Informatique de l'Ecole Normale Superieure, 75230 PARIS Cedex 5, FRANCE Abstract We propose an Abstract Interpretation-based context-free analysis for mobile sys- tems written in the pi-calculus. Our analysis automatically captures a sound – but not complete – description of the potential behavior of a mobile system interacting with an unknown context. It focuses on both the control flow and the occurrence number of agents during computation sequences. Control flow analysis detects all the possible interactions between the agents of a system, but also the potential interactions with the context. In order to deal with dynamic creation of both names and agents which is an inherent feature of mobility, our analysis distinguishes between recursive instances of the same agent. This way, we are able to prove the integrity of an ftp-server used by an unbounded number of clients. Occurrence counting analysis just consists in abstracting the occurrence number of instances of agents. Our abstraction is relational; this makes us able to detect both quickly and precisely mutual exclusion and non-exhaustion of resources. Key words: mobility, pi-calculus, static analysis, abstract interpretation, control flow analysis, occurrence counting analysis, worst case analysis. 1 Introduction The development of large scale communicating distributed systems demands the design of methods for analyzing mobile systems.

  • agent can

  • abstract interpretation

  • comparisons between

  • agent

  • abstract interpretation-based analysis

  • analysis just

  • analysis detects

  • dependent counts


Subjects

Informations

Published by
Reads 6
Language English

AbstractInterpretationofMobileSystems
1

Je´roˆmeFeret
De´partementd’Informatiquedel’E´coleNormaleSupe´rieure,
75230PARISCedex5,FRANCE

Abstract
WeproposeanAbstractInterpretation-basedcontext-freeanalysisformobilesys-
temswritteninthe
π
-calculus.Ouranalysisautomaticallycapturesasound–but
notcomplete–descriptionofthepotentialbehaviorofamobilesysteminteracting
withanunknowncontext.Itfocusesonboththecontrolflowandtheoccurrence
numberofagentsduringcomputationsequences.
Controlflowanalysisdetectsallthepossibleinteractionsbetweentheagentsofa
system,butalsothepotentialinteractionswiththecontext.Inordertodealwith
dynamiccreationofbothnamesandagentswhichisaninherentfeatureofmobility,
ouranalysisdistinguishesbetweenrecursiveinstancesofthesameagent.Thisway,
weareabletoprovetheintegrityofan
ftp
-serverusedbyanunboundednumber
ofclients.Occurrencecountinganalysisjustconsistsinabstractingtheoccurrence
numberofinstancesofagents.Ourabstractionisrelational;thismakesusableto
detectbothquicklyandpreciselymutualexclusionandnon-exhaustionofresources.

Keywords:
mobility,
π
-calculus,staticanalysis,abstractinterpretation,control
flowanalysis,occurrencecountinganalysis,worstcaseanalysis.

1Introduction

Thedevelopmentoflargescalecommunicatingdistributedsystemsdemands
thedesignofmethodsforanalyzingmobilesystems.Insuchsystems,agent
distributiondynamicallychangesduringcomputation,makingtheiranalysisa
verydifficulttask.Furthermore,thesizeofthesesystems,suchastheInternet
forinstance,islargeenoughtopreventasinglepersonfromknowingthe
wholesystem.Thisiswhyweareinterestedinvalidatingpropertiesona
1
ThisworkwassupportedbytheRTDprojectIST-1999-20527“DAEDALUS”of
theEuropeanFP5programme.

PreprintsubmittedtoElsevierScience

11March2004

mobilesystemwhichbelongstoabiggerone,calleditscontext,withouthaving
preciseknowledgeofthiscontext.WeproposeafullyautomaticAbstract
Interpretation-basedanalysisfordetectingandprovingsomepropertiesof
suchmobilesystems.

Inthisstudy,wefocusonmobilesystemsdescribedinthe
π
-calculus[22,23]
whichisaformalismwellsuitedforunderstandingtheproblemsrelatedtomo-
bility.The
π
-calculusdescribessystemsofagentswhichmayinteractviathe
communicationofchannelnamesthroughchannels.Whenreceivingachannel
name,anagentgetssomecontroloverthisname:itcancommunicatewith
otheragentssharingthisnameorevencommunicatethisnametootheragents.
Theexpressivepowerofthe
π
-calculusalsofollowsfromareplicationmecha-
nism,whichallowsthespawningofnumberofinstancesofasameagent.Thus,
eachinstanceofeachagentopensitsownchannelsandcanthencommuni-
catetheirnamestootheragents.Thesemanticsofthe
π
-calculusisusually
describeduptoacongruencerelation.Thisrelationallowsagentstointeract
bysolvingconflictbetweenchannelnamesandmakingtheagentsmoveinthe
syntacticdescriptionofthesystem.Nevertheless,becauseofthiscongruence
relation,itwouldbeverydifficulttoderiveanabstractionoftheusualse-
manticsofthe
π
-calculus.Tosolvethisproblem,weintroduceanon-standard
semantics.Thisnon-standardsemanticsisfullyoperational(i.e.itrequires
nocongruencerelation).Itusesafreshnameallocationscheme,inorderto
providefreshnamestoopenedchannels,anddescribesconfigurationsassets
ofagents,sothatthecongruencerelationisnolongerrequired.Moreover,this
freshnameallocationschemeallowsustoencodesomeinterestingproperties
inthesemantics,suchasthefactthattwochannelshavebeenopenedbythe
sameinstanceofanagent,orbytwosuccessiveinstancesofanagent.

Havingchosentheappropriatesemantics,weusetheAbstractInterpretation
frameworktodesigndecidableanalysesofthe
π
-calculus.Thisframeworkis
highlygeneric:itcanbeappliedtovariousanalyses,providedsomeabstract
primitivesaregiven.Moreover,itisextensible:itallowsustobuildthe(ap-
proximatedreduced)productofseveralanalysesexpressedinthisframework.
Wethenuseourframeworktoaddresstwoorthogonalissues:thecontrolflow
andtheoccurrencecounting.Controlflowanalysisconsistsindetectingthe
setofagentinstancesthatcanreceivethenamesofthechannelsopenedbya
giveninstanceofanagent.Thisanalysisiscontext-free:itwilldetectwhich
channelnamescanbecommunicatedtothecontext.Itisalsonon-uniform
inthesensethatitdistinguishesbetweenrecursiveinstancesofagents.Itcan
prove,forinstance,thatanamecanbecommunicatedtoonlyoneotherin-
stanceofanagent,andnottotheotherones.Inthecaseofthe
ftp
-server,
itdetectsthattheservercanreturnaqueryonlytothecorrectclienteven
inthecasewhereanunboundednumberofclientsarecreated.Occurrence
countinganalysisconsistsinabstractingtheoccurrencenumberofinstances
ofagentsduringcomputationsequences.Itisespeciallyusefultodetectmu-

2

tualexclusion.Italsohelpsindiscoveringaboundtothenumberofagents
duringcomputationsequences,sothatwecanverifythatsomepartofthe
systemswillnotexceedphysicallimitsimposedbytheimplementationofthe
system.Inthecaseofthe
ftp
-server,wecanautomaticallyinferthemaximum
numberofsimultaneousclientsessions.Ourapproachreliesontheuseofa
reducedproductbetweenanon-relationalandarelationaldomain.Complex-
ityproblemsaresolvedbyusingapproximatedalgorithmsforcalculatinga
reductionbetweenthesetwodomains.
Asaresultwegetapolynomialanalysiswhichhasbeenimplementedin
Ocaml
.Thecorrespondingprototypecanbeusedonthewebat:

http://www.di.ens.fr/~feret/prototypes/prototypes.html.en
Someexamplesandashorttutorialarealsoprovided.
RelatedworksarediscussedinSect.2.Thestandardsemanticsofthe
π
-
calculusisgiveninSect.3.ItisfirstrefinedinSect.4andextendedtoopen
systemsinSect.5.AgenericabstractanalysisisdesignedinSect.6.Itis
instantiatedinbothSect.7andSect.8toget,respectively,acontrolflowand
anoccurrencecountinganalysis.Complexityresultsandanalysistimesare
giveninSect.9.

2Relatedwork

Flowanalysis.
Controlflowanalysesfocusontheexplicitflowofinformation.
Nielson
etal.
useabstractinterpretationin[1–3]toinferauniformdescrip-
tionoftheinteractionsbetweenagentsandapplySeidl’ssolvertogetacubic
implementationoftheiranalysisin[25].HennessyandRielyhavedesigneda
type-basedanalysiswiththesameexpressivepowerin[19].Theseanalysesuse
explicitinformationflowtodetectwhethersomesecurityconstraintsspecified
usingasecuritylevelcannotbeviolated.Nevertheless,theseanalyzesareuni-
form(or
mono-variant
).Theycannotdistinguishbetweendistinctinstances
ofthesameagent.Forexample,itisimpossibletogivedistinctsecuritylevels
todistinctinstancesofthesameagent.Systemspecificationcouldberewrit-
tensothatseveralinstancesofagivenagentaresyntacticlydistinguished
fromtheothers.Therefore,thisrequiresahumaninterventiontoguesswhich
replicationhavetobesyntacticallyunfoldedandhowmanyinstanceshave
tobedistinguished.Ouranalysisrequiresnohumananalysis,andcanfind
interestingpropertiesevenifanarbitrarynumberofinstanceshavetobe
distinguished.Moreover,itisnotobviousinmanycasesthatthereexistsa
syntacticrewritingofthesystemsothatseveraldifferentrecursiveinstances
canbedistinguishedonpurelysyntacticgroundandwherethesecuritypolicy

3

ischeckableusingpurelyuniformanalyses.

Cardelli
etal.
usegroupcreationin[4]toassigndependentsecuritylevels
tochannelnames.Agroupcanbeassociatedwitheachrecursiveinstanceof
anagent,andcanthenbeusedtopreventnamesofchannelsfromexiting
thescopeoftheinstancewhichhasopenedthesechannels.Nevertheless,our
analysisismuchmoreexpressive:wecaninferalgebraiccomparisonsbetween
agentinstances,whichallowsustoexpressthefactthataninstanceofan
agentcanonlycommunicatewiththenextinstanceofitorwiththeprevious
one.Asaconsequence,wecanprovethatthenameofachannelissentback
totheinstancewhichhaspreviouslyopenedthischannel,evenifthisnameis
notconfinedintothescopeofthisrecursiveinstance.

Venethasalreadyproposedanon-uniformanalysisin[30,31].Thisanalysis
infersasoundnon-uniformdescriptionofthetopologyofcommunications
betweentheagentsof
friendlysystems
[22],inwhichreplicationguardscannot
benestedandsystemsareclosed.Themaincontributionswithrespectto
Venet’sworkare:

(1)theextensionofthenon-uniformanalysistoagentswithnestedreplica-
tionguards;
(2)theextensiontoopensystemsactinginapossiblyunknowncontext;
(3)theoccurrencecountinganalysis.

Occurrencecountinganalysis.
Onlyveryfewanalysesforcountingoccur-
rencesofagentshavebeenpublished.Nevertheless,thisproblemisveryclose
totheproblemofapproximatingthebehaviorofaPetrinet,andofoccur-
rencecountinginmobileambients.In[18],Nielson
etal.
proposeanexponen-
tialanalysisforcountingoccurrencesofagentsinsideambients.In[26],they
usecontext-dependentcountsforinferringamoreaccuratedescriptionofthe
internalstructureofagents,attheexpenseofahighertimecomplexity(an
exponentialnumberofagentsaredistinguished).Theseanalysesrelyonthe
useofanon-relationaldomaintoabstractthecontentofanambient.Then,
theyusedisjunctivecompletion,andabstractthesetofallthepotentialcon-
tentsofasyntacticambientasthepowersetofthisabstractdomain.These
twoanalysesencounterthesameproblem:inthecasethatseveralinstances
ofthesameagentmaycoexist,whenoneinstanceofthisagentperformsa
computationstep,theseanalysescannotdecidewhetheronlyoneorseveral
instancesremainafterthiscomputationstep,sotheyhavetoconsiderthetwo
possiblecases,whichleadstobothalossofprecisionandanexponentialex-
plosionincomplexity.Theuseofanapproximatedreducedproductbetween
arelationaldomainandanon-relationaldomaintogloballyabstractsetsof
multi-setsofagentsallowsustosolvethisproblemefficiently.Thusweobtain
averyaccurateanalysiswhichispolynomialinthenumberofsyntacticagents
(i.e.polynomialinthesizeoftheinitialsystemconfiguration).

4

Behavioraltypes.
In[20],KobayashiandIgarashiuse
CCS
processesastypes
formobilesystemsandchecksomebehavioralinvariantsexpressedinmodal
logic.Nevertheless,describingcausalitybetweenactionsleadstoanexplosion
ofthesizeofthetypes.Anotherproblemisthattheirtypesystemcannot
expresspropertiesthatdealwiththedynamiccreationofchannelnames.
RajamaniandRehofhaveextendedthistypesystemin[28],sothatithandles
dynamicnamecreation.Buttypecheckingisundecidableingeneral.So,they
willhavetoproposeanapproximationinfuturework.
Modularanalysis.
Context-freesemanticsisanimportantissueinstaticanal-
ysis.Itallowstheanalysisofonlyapartofasystem,withoutmuchknowledge
ofitscontext.Itcanbeusedtoabstractthebehaviorofaninstanceofan
agent,anddetectwhichnamesmayescapethescopeofthispart.Thiscanbe
usedtodetectdeadcode,forinstance.RajamaniandRehofproposeamodular
analysisin[28].Havingabstractedthebehavioroftwomodules,theycancal-
culateanapproximationoftheparallelcompositionofthem.Butthisanalysis
isveryrestrictivebecausemoduletypesmustsatisfysome
assume-guarantee
properties.
Securityanalysis.
IntheDolev-Yao’smodel[13],asystemisusuallyprovednot
tobevulnerabletoagivenclassofattackers.Suchclassesarethendescribed
byasetofruleswhichexplainhowanattackercaninteractwithasystem.
Inourapproach,theclassoftheattackerisactuallyanysystemexpressedin
the
π
-calculus.Thebenefitisthatourcontext-freeanalysisiscompletewith
respecttothemodel,sothatwecanuseourresultstoanalyzeamodule.
Themaindrawbackofourapproachisthatwecannotexpressotherattacks.
Forinstance,wecouldimaginethatanattackercouldguesssomesensitive
information,byobservingthetimeofexecutionofsomeagents.

3
π
-calculus

Weintroduceinthissectionthe
π
-calculusandastandardsemanticsforit.
The
π
-calculusisaformalismusedtodescribemobilesystems.Itdescribes
asystemasasetofagentswhichexchangeinformationoverchannels.These
communicationsenableagentsynchronization,butalsodynamicmodification
ofthesystemtopology:agentscanopennewchannels,theycanalsopasscon-
troloversomechannelstootheragents,andtheycanevendynamicallycreate
otheragents.Here,weconsideralazyversionofthesynchronouspolyadic
π
-
calculus[22]withinternalchoiceoperator.Inthepolyadic
π
-calculus,agents
cancommunicatetuplesofchannelnames.Weusethelazyversionofreplica-
tionintroducedin[29,Chap.7]:agentcreationsareperformedonlywhenthey
arerequiredbyacommunication.Thisisnotalimitationasfullreplication
canbeencodedwithlazyreplication(Cf.[29,page:102]).

5

3.1Syntax

Let
N
beacountablesetofchannelnamesand
L
acountablesetoflabels.The
syntaxofagentsisdescribedinFig.1(a).Syntacticcomponentsareidentified
bydistinctlabelsin
L
.Inputguard,replicationguardandnamerestrictionact
asnamebinders,i.eintheagents
c
?
j
[
x
1
,...,x
n
]
P
,

d
?
j
[
y
1
,...,y
p
]
Q
and(
νx
)
R
,
theoccurrencesof
x
1
,...,
x
n
in
P
,
y
1
,...,
y
p
in
Q
and
x
in
R
arebound.We
alsoassumethatnonameoccurstwiceinawholesystem,asanargumentof
aninputguard,areplicationguardoranamerestriction.Usualrulesabout
scope,substitutionand
α
-conversionapply.Wedenoteby
fn
(
P
)thesetoffree
namesin
P
,i.enamesthatarenotunderthescopeofabinder,andby
bn
(
P
)
thesetofboundnamesin
P
.

3.2Semantics

Wenowinformallyintroducethesemanticsofthe
π
-calculus.Theagent
aP
firstcomputestheaction
a
beforelaunchingthecontinuation
P
.Theagent
(
νx
)
P
opensanewchannel,named
x
,theagent
P
canusethischannelfor
communicating,itcanalsosendthename
x
totheotheragents.In(
P
|
Q
),
P
and
Q
aretwoconcurrentagentswhichmaybehaveindependently,orinteract
bycommunicating.Theformula(
P

Q
)denotesaninternalchoicebetween
twoagents.Either
P
or
Q
isrun,whiletheotherfadesaway;thechoicebe-
tween
P
and
Q
doesnotdependontheotheragents.Theagent
0
doesnothing.
Theagent
c
!
i
[
x
1
,...,x
n
]
P
sendsamessageviathechannelnamed
c
,thismes-
isageisthetupleofchannelnames(
x
1
,...,x
n
).Theagent
c
?[
y
1
,...,y
n
]
P
waits
foramessageonthechannelnamed
c
,andbindsthechannelnames
y
1
,...,
y
n
to
thereceivedchannelnames.Theagent

c
?
i
[
y
1
,...,y
n
]
P
isa
resource
:itrepli-
catesitselfjustbeforereceivingamessage:anewinstanceof
P
islaunched
with
y
1
,...,
y
n
boundtothereceivedchannelnameswhile

c
?
i
[
y
1
,...,y
n
]
P
waits
forthenextmessage.
TheoperationalsemanticsisgivenbybothacongruencerelationinFig.1(b)
andareductionrelationinFig.1(c).Thecongruencerelationallowsagents
tointeract,whilethereductionrelationdescribesagentcomputations.Some
rulesinthecongruencerelationmakeagentsmoveinsidethesyntactictree:
theyasserttheassociativityandcommutativityoftheparallelcomposition.
Someothersextendthescopeofnamestotheagentstheyarecommunicated
to:
α
-conversionsolvesconflictsbetweennames,swappingselectsthenamethe
scopeofwhichwewishtoextend,andextrusionextendsitsscopetoanother
agent.Thereductionrelationdescribesagents’communications.Acommuni-
cationisallowedwhentherearetwoconcurrentagents,suchthatthefirstone
sendsamessageonachannel,whilethesecondonewaitsforamessageon

6

P
::=
aP
(action)
|
(
νx
)
P
(namerestriction)
|
(
P
|
P
)(parallelcomposition)
|
(
P

P
)(internalchoice)
|
0
(nil)
a
::=
c
!
j
[
x
1
,...,x
n
](outputguard)
|
c
?
i
[
x
1
,...,x
n
](inputguard)
|∗
c
?
i
[
x
1
,...,x
n
](replicationguard)
where
c,x
1
,...,x
n
,x
∈N
,i,j
∈L
and
n
>
0.
(a)Syntax
(
νx
)
P

(
νy
)
P
[
x

y
]if
y
6∈
fn
(
P
)(
α
-conversion)
P
|
Q

Q
|
P
(commutativity)
P
|
(
Q
|
R
)

(
P
|
Q
)
|
R
(associativity)
P
|
0

P
(endofanagent)
(
νx
)
0

0
(garbagecollecting)
(
νx
)(
νy
)
P

(
νy
)(
νx
)
P
(swapping)
((
νx
)
P
)
|
Q

(
νx
)(
P
|
Q
)if
x
6∈
fn
(
Q
)(extrusion)
where
x
,
y
∈N
.
(b)Congruencerelation
(
i,j
)

c
!
j
[
x
1
,...,x
n
]
P
|
c
?
i
[
y
1
,...,y
n
]
Q
−→
P
|
Q
(comm.)
(
i,j
)

c
!
j
[
x
1
,...,x
n
]
P
|∗
c
?
i
[
y
1
,...,y
n
]
Q
−→
P
|
Q
|∗
c
?
i
[
y
1
,...,y
n
]
Q
(replication)
P

Q



P
(leftchoice)
P

Q



Q
(rightchoice)
P

λ

QP


PP

λ

QQ

Q

P

λ

P

λλλ(
νx
)
P
−→
(
νx
)
QP

−→
Q

P
|
Q
−→
P

|
Q
where
c
,
x
,
x
1
,...,
x
n
,
y
1
,...,
y
n
∈N
,
i,j
∈L
,
λ
∈{⊕}∪
(
L×L
),
∼and
Q
=
Q
[
y
1

x
1
,...,y
n

x
n
].
(c)Reductionrelation
Fig.1.Standardoperationalsemantics
7

thesamechannel(wealsorequestthatbothmessageshavethesamearity).
Theresultsofsuchacommunicationareobtainedbyapplyingthesubstitu-
tionofthe
λ
-calculusinthecontinuationofthemessagereceiver.Whenthe
receiverisaresource,itisjustsyntacticallyreplicatedbeforeperformingthe
communication;thiswaytheresourceisstillavailableafterthecommunica-
tion.Wehavelabelledeachchoicereductionstepwiththesymbol

andeach
communicationreductionstepwiththelabelsofbothagentsinvolvedinthe
communication:thiswillallowustorelatethestateofasystemtothehistory
ofthecomputationstepsthathaveledtothisstate.

3.3Examples

Wenowproposesomeexamplestoillustrateboththissemanticsandthekind
ofpropertiesweareinterestedin.Wewillfindthatthesemanticswehave
consideredisnotpreciseenoughtohandlethepropertiesweareinterestedin.
Example1
An
ftp
-servercanbedescribedbythesystemgiveninFig.2.
Thefirstresourcerepeatedlycreatesanewclientwhichsendsaquerytoa
server.Thisqueryiscomposedofaquery
request
,andanaddress
address
.
Theclientsendsitsqueryagaininthecasethatitreceivesafailurereportde-
notedbytheagent
address![]
.Thesecondresourcedescribestheserver.When
thisonereceivesaquery,itreplicatesitself.Then,eitheritusesanavailable
portandcomputesthequeryoritreportsafailuretotheclientbyspawn-
ingtheagent
address![]
.Availableportsaredenotedbyagents
port![]
.Data
processingjustconsistsinacommunicationbetweentwoagentsoftheserver,
throughthechannelthenameofwhichis
deal
:mostcomputationalfeatures
areabstractedaway.Afterthiscommunication,theportisreleased,whilethe
answerissentbacktotheclient.Aninstanceoftheagent
email
![
rep
]
isleft
asatraceofthesession.
Ouranalysiswillproveboththeintegrityandthenon-exhaustionofthissys-
tem:itwilldiscoverthateachtimeanagent
email![rep]
isspawned,the
names
email
and
rep
arerespectivelyboundtothenamesoftwochannels
openedbytherestrictions
(
ν
address
)
and
(
ν
request
)
ofthesameinstance
ofaresource,andsotheserverreturnsitscomputedanswertothecorrect
client;italsocapturesthefactthatnomorethanthreeinstancesofthesyn-
tacticagent
deal
![
data
]
canoccursimultaneously,whichmeansthatnomore
thanthreesimultaneoussessionscanbeactiveinthesametime.
Example2
WeproposeinFig.3amobilesystemwhichcreatesaringof
processes,withatokenpassedaroundthisring.Thenamesofthechannels
openedbynamerestrictions
(
ν
left0
)
and
(
ν
right
)
denotetheprocessesof
thering.Thefirstpartofthesystemdescribestheringcreation.Thefirstpro-

8

((
ν
make)(
ν
server)(
ν
port)
((

make?
1
[](
ν
address
)(
ν
request
)
((

address
?
2
[]server!
3
[
address
,
request
])
|address
!
4
[]
|make!
5
[]
))|(

server?
6
[
email
,
data
](
ν
deal
)
(port?
7
[](
deal
!
8
[
data
]
|
deal
?
9
[
rep
](
email
!
10
[
rep
]
|
port!
11
[]))
⊕email
!
12
[]
))

|
port!
13
[]
|
port!
14
[]
|
port!
15
[]
|
make!
16
[])
)

Fig.2.An
ftp
-server

((
ν
make)(
ν
mon)(
ν
left0)
(((

make?
1
[
left
](
ν
right
)(mon!
2
[
left
,
right
]
|
make!
3
[
right
]))
|
(

make?
4
[
left
](mon!
5
[
left
,
left0]))
|
make!
6
[left0])
|((

mon?
7
[
prev
,
next
]
(

prev
?
8
[](
ν
crit
)(
crit
?[]
9
next
!
10
[]
|
crit
!
11
[])))
|
left0!
12
[]))
)

Fig.3.Aringofprocesses

9

cessiscreatedbytherestriction
(
ν
left0
)
.Anagent
mon
![
v1
;
v2
]
denotesa
connectionbetweentwoprocesses.Then,eachtimethefirstresourceisrepli-
cated,anewprocessiscreatedandlinkedtothepreviousprocess,whichhas
beenpassedasanargumentofthereplication.Thesecondresourcereplication
closestheringbylinkingthelastcreatedprocesstothefirstcreatedprocess.
Thesecondpartofthesystemdescribestheexecutionoftheprocesses:anad-
ditionalresourcespawnsaresourceforeachprocessofthering.Thenatoken
isputintotheringofprocesses:thetokenisdenotedbysyntacticcopiesof
theagents
next
![]
and
left0
![]
.Thenameofthisagentdescribesthetoken
location.Whenthetokenisavailable,thecorrespondingprocesscanreplicate
itsresource,andasaresulttheprocessentersitscriticalsection.Thecritical
sectionisexitedwhenthetwoagents
crit
![]
and
crit
?[]
haveinteracted;the
tokenisthenpassedtothenextprocess.
Ouranalysiscanproveboththeintegrityandthenon-exhaustionofthissys-
tem:itdiscoversthateachtimeanagent
mon![left;right]
isspawned,either
thename
left
islinkedtothechannelopenedbytherestriction
(
ν
left0
)
,or
bothnames
left
and
right
arelinkedtotwochannelsopenedbyinstancesof
therestriction
(
ν
right
)
,butthechannellinkedtothename
left
hasbeen
openedbythepreviousinstanceofit,whichmeansthataprocessofthering
canonlybeconnectedtoeitherthefirstoneortothenextone;itcaptures
thefactthatonlyonesimultaneousinstanceofthesyntacticagent
crit
![]
can
exist.Thatistosay,thatonlyoneprocessoftheringcanenteritscritical
sectionatagiventime.
Remark3
Thestandardsemanticsisnotwellsuitedtoexpressandcapture
integrityproperties,becausethelinkbetweenagentinstancesandthenames
ofthechanneltheyhaveopenedisnotencodedexplicitly.Forinstance,ifwe
thinkabouttheexampleofthe
ftp
-serverandifwecleverlychoosethenames
ofopenedchannelsbyindexingthemwiththeinstancenumberoftheclient
resource,weobtainaftertwosessionsoftheserverasystemofthefollowing
form
2
:
(
νc
)(
ν
address
1
)(
ν
request
1
)(
ν
address
2
)(
ν
request
2
)
(
S

|
address
1
!
10
[
request
1
]
|
address
2
!
10
[
request
2
])
.
Itappearsexplicitlythatrequestanswersarereturnedatgoodaddresses.How-
ever,wecouldhavechosenthenamesdifferentlyandobtainedthefollowing
α
-equivalentconfiguration:
(
νc
)(
ν
address
2
)(
ν
request
1
)(
ν
address
1
)(
ν
request
2
)
(
S

|
address
2
!
10
[
request
1
]
|
address
1
!
10
[
request
2
])
2
Thistermonlyshowsexplicitlytheinformationweareinterestedin.Thevariable
S

denotestherestofthesystemandthenotation(
νc
)denotesasequenceof
restrictionsforallimplicitnames.

01