7. K. Yamalidou, J. Moody, M.D. Lemmon and P.J. Antsaklis, Feedback Control of Petri nets based on Place Invariants, Automatica, Vol. 32, No. 1, pp. 15-28, 1996.
8. J.O. Moody, P.J. Antsaklis, and M.D. Lemmon, “Application of Automatic Petri Net Con-trol Design”, proceedings of INRIA/IEEE Conference sur les technologies emergentes et l’automatisation de systemes de fabrication, October 10-13, Paris, France.
9. K.X. He and M.D. Lemmon, ”On the transformation of liveness-enforcing marking based supervisors into monitor supervisors”, submitted to the IEEE Conference on Decision and Control, Sydney Australia, December 2000.
10. W.M.Wonham and P.J. Ramadge, “On the supremal controllable sublanguage of a given language”, SIAM Journal of Control and Optimization, 25(3), pp. 637-659, May 1987.
11. R.S. Sreenivas, “On supervisory policies that enforce liveness in complete controlled Petri nets with directed cut-places and cut-transitions”, IEEE Trans. on Automatic Control, Vol.
44(6), June 1999, pp. 1221-1225.
12. Y. Li and W.M. Wonham, “control of vector discrete-event systems: controller synthesis”, IEEE Transactions on Automatic Control, Vol. 39(3), pp. 512-530, 1994.
13. K.X. He and M.D. Lemmon, ”On the existence of liveness-enforcing supervisory policies of discrete-event systems modeled by n-safe Petri nets”, Proceedings of IFAC conference on Control System Design, Special issue on Petri nets, Slovakia, June 2000.
14. Vogler, W. (1992), Modular Construction and Partial Order Semantics of Petri Nets, Lecture Notes in Computer Science, Vol. 625, Springer-Verlag, 1992.
15. P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems – An Ap-proach to the State-Explosion Problem. PhD thesis, University of Liege, Computer Science Department, November 1994.
16. P. Godefroid and P. Wolper, ”Using Partial Orders for the Efficient Verification of Dead-lock Freedom and Safety Properties,” Formal Methods in System Design, Kluwer Academic Publishers, Vol. 2, No. 2, April 1993, pp. 149-164.
17. K. McMillan,”Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits”, Computer Aided Verification, 4th International Workshop (CAV’92), (Bochmann and Probst (eds.), LLNCS Vol 663, Springer Verlag, 164-177, 1992.
18. A. Kondratyev, M. Kishinevsky, A. Taubing, and S. Ten, “Structural approach for the analysis of Petri nets by reduced unfoldings”, Proceedings of the 17th International Conference on Application and Theory of Petri Nets, Osaka Japan, June 24-28, 1996.
19. K.X. He and M.D. Lemmon, “Liveness verification of discrete event systems modeled by n-safe Petri nets”, to appear in Proceedings of the 21st International Conference on Application and Theory of Petri Nets, Denmark, June 2000.
20. J. Esparza, S. Romer, and W. Vogler, “An improvement of McMillan’s unfolding algorithm”,
Proceedings of Tools and Algorithms for the Construction and Analysis of Systems, (T.
Ma-garia and B. Steffen, eds.), LNCS Vol. 1055, Springer-Verlag, 1996.
Based on Extended Petri Nets
?
KhaledEl-Fakih
1
,HirozumiYamaguchi
2
,
Gregorv.Bochmann
1
,andTeruoHigashino
2
1
SchoolofInformationTechnologyandEngineering,UniversityofOttawa,
150LouisPasteur,Ottawa,OntarioK1N6N5,Canada
fkelfakih,bochmanng@site.u ottaw a.ca
2
GraduateSchoolofEngineering Science,OsakaUniversity,
1-3Machikaneyamacho,Toyonaka,Osaka560-8531, Japan
fh-yamagu,higashinog@ics.es.o saka- u.ac .jp
Abstract. Protocolsynthesisisusedtoderivea specication ofa
dis-tributedsystemfromthespecicationoftheservicestobeprovidedby
thesystemtoitsusers.Maintainingsuchasysteminvolvesapplying
fre-quentminormodicationstotheservicespecication duetochangesin
theuserrequirements.Inordertoreducethemaintenancecostsofsucha
system,wepresentanoriginalmethodthatconsistsofasetofrulesthat
avoidcompleteprotocolsynthesisafterthesemodications.Theserules
aregivenforasystemmodeledasanextendedPetrinet.Anapplication
exampleisgivenalongwithsomeexperimentalresults.
1 Introduction
Synthesis methods havebeen used(for surveyssee [5,6]) to derivea
specica-tionofadistributedsystem(hereaftercalledprotocolspecication)automatically
fromagivenspecicationoftheservicetobeprovidedbythedistributedsystem
toitsusers(calledservicespecication).Theservicespecicationiswrittenlike
a program of a centralized system, and does not contain any specication of
themessageexchange betweendierentphysicallocations.However,the
proto-col specicationcontainsthespecicationofcommunicationsbetweenprotocol
entities(PE's)atthedierentlocations.
A number of existing protocol synthesis strategies have been described in
theliterature.Therststrategy,[9,3,4,8,10,12,14,17,18],aimsat
implement-ingcomplexcontrol-owsusingseveral computationalmodelssuchasLOTOS,
Petrinets,FSM/EFSMandtemporallogic.Thesecondstrategy,[20,23,19,24,
22], aimsatsatisfyingthetiming constraintsspeciedbyagivenservice
speci-cationin thederivedprotocol specication.Thisstrategydealswithreal-time
distributed systems.Thelaststrategy,[21,25,11,15,7,16], dealswiththe
man-changedbetweenPE'sforagivenxedresourceallocationondierentphysical
locations.
Somemethodsinthelaststrategy,especiallythesepresentedinourprevious
researchwork[26],havetriedtosynthesizeaservicespecicationbyderivingits
corresponding protocol specication with minimum communication costs and
optimalallocationof resources.
Asanexample,weconsideraComputerSupportedCooperativeWork(CSCW)
softwaredevelopmentprocess.Thisprocessisdistributed amongengineers
(de-velopers,designers,managersand others). Eachengineer hashis ownmachine
(PE) and participates in the development process using distributed resources
(drafts, sourcecodes, object codes, multimedia videoand audio les, and
oth-ers)placedondierentmachines.Consideringtheneedforusingtheseresources
between dierent computers, we derive, using our protocol synthesis method,
theengineer'ssub-processes(protocolspecication)knowingthewholesoftware
development cycle(service specication) and wedecideon anallocation of
re-sources that would minimize the communication costs. Both the service and
protocolspecicationsaredescribedusingextendedPetri nets.
Inrealisticapplications,maintainingasystemmodeledbyagivenextended
Petrinetspecication,involvesmodifyingitsspecicationasaresultofchanges
in the user requirements. Synthesizing the whole system after each
modica-tionis considered expensiveand time consuming.Therefore, itisimportant to
re-synthesizethe modiedparts of servicespecication in order to reduce the
maintenance cost,which wasreportedto accountfor asmuch astwo-thirdsof
thecostofsoftwareproduction[30].
In this paper, we present a new method for re-synthesizing the protocol
specication from a modied service specication. The method consists of a
set of rulesthat wouldbeapplied to dierent PE'safter amodicationto the
servicespecication,in ordertoproducenewsynthesized(henceforthcalled
re-synthesized) PE's. The parts of the protocol specication that correspond to
theunmodiedparts oftheservicespecicationarepreservedintact.As shown
later, thismethod reducesthecostof synthesizingthewhole systemaftereach
modication.
This paperis organized as follows. Section 2 givesexamplesof service and
protocolspecications,and Section 3describestheprotocol synthesismethod.
Basedonthismethod,wepresentinSection4protocolre-synthesismethodalong
withsomeapplicationexamplesinSection5.Section6concludesthispaperand
includes ourinsightsforfutureresearch.
2 Service Specication and Protocol Specication
i>R1
[ R1<-R2+i, R2<-R1+R2+i ] G1 ? i
R1 R2
G1
i>R1
[ R1<-R2+i, R2<-R1+R2+i ] G1 ? i
R1 R2
G1 3
1
fire
2 5 6
(a) (b)
transition t transition t
Fig.1.Register Valuesand TokenLocations beforeand afterFiringofTransitionin
PNR
system.Inthis model, anI/Oeventbetweenusersand thesystemfollowedby
the calculation of new valuesof variables inside the systemis associated with
theringofatransition.Sincedistributedsystemscontainsomevariables(e.g.
databasesandles)andtheirvaluesareupdatedaccordingtoinputsfromusers,
theycanbemodeledbyPNRnaturally.
Eachtransition t inPNR hasalabelhC(t);E(t);S(t)i, where C(t) isa
pre-conditionstatement(oneoftheringconditionsoft),E(t)isaneventexpression
(whichrepresentsI/O)andS(t)isasetofsubstitutionstatements(which
repre-sentsparallelupdatesofdatavalues).Consider,forexample,transitiontofFig.1
whereC(t)=\i>R
1
",E(t)=\G
1
?i"andS(t)=\R
1 R
2 + i;R
2 R
1 + R
2 + i".
i is aninput variable, which keepsan input value and its value is referredby
onlythetransition t.R
1
andR
2
are registers,whichkeepassigned valuesuntil
new values areassigned, and their valuesmay be referred and updatedby all
thetransitionsinPNR(thatis,globalvariables).G
1
isagate,aserviceaccess
point (interaction point) betweenusers and thesystem. Note that \?" in E(t)
meansthatE(t) isaninputevent.
Atransitionmayreif(a)eachofitsinputplacehasonetoken,(b)thevalue
ofC(t)istrueand(c)aninputvalueisgiventhroughthegateinE(t)(ifE(t)is
aninputevent).Assumethatanintegerofvalue3hasbeengiventhroughgate
G
1
,and thecurrentvaluesof registersR
1
and R
2
are 1and2,respectively.In
thiscasethevalueof\i>R
1
"istrueandthetransitionmayre.Ifitres,the
event\G
1
?i"is executed andthe inputvalue3is assigned to inputvariable i.
Then\R
1 R
2
+i"and\R
2 R
1
+R
2
+i"areexecutedinparallel.Therefore
afterthering,thetokensaremovedandthevaluesofregistersR
1
andR
2 are
G1?i1
[R2<-retrieve(R1,i1)]
keyword(i1)
keyword(i2) G2?i2
[R4<-retrieve(R3,R2,i2)]
G1!R4 [ ] true
R1 R2 R3 R4
G1 G2
T1
T2
T3
Fig.2.ServiceSpecication
aninputeventanditmeansthatthevaluegiventhroughG
s
isassignedtothe
input variable \iv". \" is an internal event, which is unobservable from the
users.S(t) isaset ofsubstitution statements,each ofthe form\R
w exp
w
",
whereR
w
isaregisterandexp
w
isanexpressionwhoseargumentsarefromthe
input variable in E(t)and registers.If t res, E(t) is executed followedby the
parallelexecutionofstatementsinS(t).
2.2 Service Specication
At ahighly abstracted level, adistributed systemis regarded asa centralized
system which works and provides services as a single \virtual" machine. The
numberofactualPE'sandcommunicationchannelsamongthemarehidden.The
specicationofthedistributedsystematthisleveliscalledaservicespecication
anddenoted bySspec.
Actualresources of a distributed system may be located on some physical
machines,calledprotocolentities.However,onlyonevirtualmachineisassumed
atthislevel.Fig.2showsSspecofasimpledatabasesystemwhichhasonlythree
transitions.Thesystemreceivesakeyword(inputvariablei
1
)throughgateG
1 ,
retrievesanentrycorrespondingtothe keywordfromadatabase(registerR
1 ),
and stores the result to registerR
2
. This is done on transition T
1
. Then the
systemreceivesanotherkeyword(input variable i
2
)throughgateG
2
, retrieves
R3 R4 R1 R2
G1 G2
keyword(i1)
keyword(i2) G1?i1
R tmp1 ID(Mb2, w)
[Rtmp1.R2<-w]
ID(Mb2, w) [Rtmp1.i1<-i1]
ID(Mb1, w) [Rtmp3.i1<-w]
g31?w
[R2<-retrieve (R1, Rtmp3.i1)]
τ
g13?w g13!Mb1[Rtmp1.i1]
g32!Mg1[ ]
g32?w
g31!Mb2[R2]
g23?w
[Rtmp1.i2<-w]
g12?w true
[R4<-retrieve (R3, Rtmp1.R2, Rtmp1.i2)]
τ true
G1!R4 true
true
true
ID(Ma2, w)
R tmp2 R tmp3
g12
g13 g21 g23 g32 g31
[Rtmp2.i2<-i2]
G2?i2
true true
g21!Mb2[Rtmp2.i2] g23!Ma2[ ]
τ true τ true
PE1 PE2 PE3
ID(Mg1, w)
true
t 1.1
t 1.2 t 1.6
t 2.1
t 2.3 t 2.2
t 1.3
t 1.4
t 1.5
t 2.4
t 2.5 t 2.7
t 2.6
t 2.8
t 3.1
Fig.3.ProtocolSpecication
2.3 ProtocolSpecication
A distributed system is acommunication system which consists of pprotocol
entitiesPE
1 ,PE
2
,...andPE
p
.Weassumeaduplexandreliablecommunication
channelwithinnitecapacitybuersatbothends,betweenanypairofPE
i and
PE
j
.ThePE
i (PE
j
)sideofthecommunicationchannelisrepresentedasgate
g
ij (g
ji
). Moreover, we assume that some resources (registers and gates) are
allocatedtocertainPE'softhedistributedsystem.
TwoPE'scommunicatewitheachotherbyexchangingmessages.IfPE
i
ex-ecutesanoutputevent\g
ij
!M[R
w
]",thevalueofregisterR
w
locatedonPE
i is
senttoPE
j
throughthecommunicationchannelbetweenthemandputintothe
buerat PE
j
'send. M is anidentiertodistinguishseveral valueswhich may
exist at thesametime onthesamechannel. PE
j
cantakethe valueidentied
byM fromthebuer,byexecutinganinputevent\g
ji
?w"withapre-condition
ID(M;w).ID(M;w)isapredicatewhosevalueistrueitheidentierininput
variablewisM.Notethatmorethanoneregister'sorinputvariable'svaluecan
besent at atime. If a received data contains multiple values, theyare
distin-guishedbysuÆxsuchasw:R
1
andw:i.Asetofanidentierandregister/input
k
specicationshPspec
1
,...,Pspec
p
iiscalledaprotocolspecicationanddenoted
by Pspec
h1;pi
. We need a protocol specication to implement the distributed
system.
Asanexample,letusassumethattherearethreePE'sPE
1 ,PE
2
andPE
3
inordertoimplementtheservicespecicationofFig.2.Wealsoassumethatan
allocationofresourcestothesePE'shasbeenxedasfollows.PE
1
hasthegate
G
1
andtheregistersR
3
hastheregisters
R
1
andR
2
. Note that inaddition to these registers,weassumethat eachPE
i
hasanotherregisterR tmp
i
to keepreceivedvaluesgiventhroughgates(inputs
and message contents). R tmp
i
can contain several values. The values can be
distinguishedbyaddingthenameofthevalueassuÆx,suchasR tmp
1 :R
3 1
.Fig.
3showsanexampleofPspec
h1;3i
,whichprovidestheserviceofFig.2,basedon
thisallocationofresources.
Accordingto thespecicationof Fig. 3,PE
1
rst receivesan input(input
variable i
(ontransition t
1:1
). Then it
sendsthevalueofR tmp
1 :i
1 toPE
3
asamessage(ontransitiont
1:2
),sincePE
3
needs the value of i
1
to change the value of R
2 . PE
3
receives and stores the
valueto R tmp
3 :i
1
ontransition t
1:3
.Then it changes thevalueof R
2
using its
own value and the value of R tmp
3 :i
1
on transition t
1:4
, and sends a message
to PE
2
on transition t
1:5
. When PE
2
receives the message on transition t
1:6 ,
PE
2
knows that it cannowcheck thevalue of C(T
2
) and executeE(T
2
). PE
2
receivesaninput(inputvariablei
2
)andstoresittoR tmp
2 :i
2
ontransitiont
2:1 ,
and sends twomessages. Oneis to send thevalue of i
2
receives these values and stores them to R tmp
1
on transitions t
2:6
and t
2:7
, respectively. Then it changes the value of R
4 on
transitiont
2:8
.Finally,PE
1
outputsthevalueofR
4
ontransitiont
3:1
returntotheirinitialstates.
As exemplied in the abovediscussion, PE's cooperate with each other by
exchangingmessages.ThecommunicationbetweendierentPE'smaybequite
complexanditisdiÆculttodesignprotocolsthatbehavecorrectly.Thereforewe
wouldliketoderiveaprotocolspecicationautomatically,suchthatitprovides
thesameserviceasagivenservicespecication.
3 Synthesis Overview
A method for derivingprotocol specicationwith an optimal allocationof
re-sourcesfromagivenservicespecicationispresentedinthissection.Thismethod
isbasedonasetofrules(calledhenceforthsynthesisrules)thatspecifyhowto
execute each transition T
x
)i of the service specication
amongstdierentderivedPE's.
3.1 SynthesisRules
ForexecutingatransitionT
x
)ioftheservicespecication
by the corresponding set of transitions t
x:1
;t
x:2
;::: of the PE'sin theprotocol
specication,weproceedasfollows.
{ ThePEthathasgateG
s
usedin E(T
x
)(sayPEstart(T
x
))checksthevalue
ofC(T
x
)(pre-conditionstatement)andexecutesE(T
x
)(eventexpression).
{ Afterthat,thePEsendsmessagescalled-messagestothePE'swhichhave
theregistersused intheargumentsofS(T
x
)(substitutionstatements).
{ Inresponse,thesePE'ssendtheregistervaluestothePE'swhich havethe
registerstobeupdatedinS(T
x
)(PEsubst(T
x
)denotesthesetofthosePE's)
asmessagescalled -messages.
{ Thesubstitution statements are executed and notication messagescalled
-messagesaresenttothosePE'swhichwillstarttheexecutionofthenext
transitions.
Forexample,fortransitionT
2
oftheservicespecicationinFig.2,PEstart(T
2
checksthevalueof pre-condition
state-ment "keyword(i
2
)" and executes"G
2
?i
2
"on transition t
2:1
ontransitiont
2:2
sincePE
3
hasregisterR
2 which
is used to substitute the value of R
4
. PE
2
also sends the input value to PE
1
as a -message \Mb
2
" on transition t
2:3
. PE
3
receives the -message \Ma
2
"
on transition t
2:4
and sends thevalue ofR
2
receives these two-messageson transitions t
2:6
and t
2:7 ,
and then executes\R
4
)" ontransition t
2:8
using its own
registerR
3
andthereceivedvaluesofR
2
andi
2
. ThePE'swhich willstartthe
executionofnexttransitionT
3 isPE
1
itself. Therefore,PE
1
doesnotsend any
-message.ThenPE
1
startstheexecutionofT
3
ontransitiont
3:1 .
InFig.4,wepresentthedetailsoftheaboverules[26],thatareclassiedinto
actionandmessagerules.ActionrulesspecifywhichPEchecksthepre-condition
andexecutestheeventandsubstitutionstatementsofT
x
.Messagerulesspecify
howthePE'sexchangemessages,andthecontentsandtypesofthesemessages.
ThreetypesofmessagesareexchangedfortheexecutionofT
x
.(1)-messages
aresentbythePEthat startstheexecutionofT
x
(i.e. PEstart(T
x
))toinform
thosePE'swhoneedtosendtheirregisters'valuestootherPE's,thattheycan
goahead andsendthesevalues.Thus,an-messagedoesnotcontainvaluesof
registers.(2) -messagesaresentin order to leteach PEwhichexecutes some
substitutionstatementsofT
x
(i.e.PE
k
2PEsubst(T
x
))knowthetimingandsome
[ActionRules]
(A1) ThePEwhichhasthegateappearinginE(Tx)(denotedbyGs)checksthat
(a) thevalueofC(T
x
)istrue,
(b) theexecutionoftheprevioustransitionsofT
x
hasbeennishedand
(c) aninputhasbeengiventhroughGs ifE(Tx)isaninputevent.
ThenthePEexecutes E(T
x
).ThisPEisdenotedbyPEstart(T
x ).
(A2) After(A1),thePE'swhichhaveatleastoneregisterwhosevalueischanged
inthesubstitutionstatementsS(T
x
)executethecorrespondingstatementsin
S(Tx).ThesetofthesePE'sisdenotedbyPEsubst(Tx).
[MessageRules]
(M
1
) Each PE
k
2PEsubst(T
x
) must receive at least one -message from some
PE's (each called PEj) inorder to knowthe timing and values of registers
it needs for executing itssubstitution statements(see (M
2
)),exceptwhere
PEk=PEstart(Tx),inthiscasePEkalreadyknowsthetimingtostart
execut-ingitssubstitutionstatementsofT
x .
(M2) If PEk2PEsubst(Tx) needs the value of some register (say Rz) in order
to executeits substitutionstatements,thenPE
k
mustreceiveR
z
througha
-messageifRz isnotinPEk.
(M
3
) EachPEjthatsendssomevaluesofregisterstoPE
k
2PEsubst(Tx)through
a-message,knowsthetimingtosendthesevaluesbyreceivingan-message
from PEstart(Tx). Note,if PEj=PEstart(Tx)then PEj knows the timingto
sendthesevalueswithoutreceivingan-message.
(M) After(A1),theonlyPEthat cansend-messages tothePE'swhichneed
themisPEstart(T
x ).
(M1) EachPEm2PEstart(Tx), where Txis the set of nexttransitionsof
Tx,mustreceivea-messagefromeachPE
k
2PEsubst(Tx)after(A2),except
wherem=k.ThisallowsPE
m
toknowthattheexecutionofthesubstitution
statementsofTxhadbeennished.
(M
2
) EachPE
m
2PEstart(T
x
)mustreceiveatleastone-messagefromsome
PEl(wherem6=l )inordertoknowthattheexecutionofTxhadbeennished
and/or to knowsome valuesof registersit needstoevaluateand executeits
conditionandeventexpression,respectively.
(M
3
) EachPE
l
thatsendsa-messagetoPE
m
2PEstart(T
x
):
(a) mustbeinPEsubst(Tx)(see(M1)),or
(b) mustreceivean-messagefromPEstart(Tx)toknowthetimingtosend
the-messagetoPE
m ,or
(c) itisitselfPEstart(Tx).Inthiscase, PElsends the-messagetoletPEm
knowthe timingand/or somevaluesof registerstostart evaluatingand
executingitsconditionandeventexpressions.
(M
4 ) IfPE
m
2PEstart(T
x
)needsthevalueofsomeregister(sayR
v
)inorderto
evaluateand/or executeits substitutionstatements,thenPEm mustreceive
Basedontheabovesynthesisrules,wedetermineabehaviorofthederivedPE's
that would minimizetheircommunicationcostwhileoptimallyallocatingtheir
resources,usinganIntegerLinearProgramming(ILP)model.Thiscostcouldbe
basedon thenumberofmessagesto beexchangedbetweendierent PE's[25].
Moreover,othercostcriteriacanalsobeconsideredsuchasthecostsofresource
allocation, size of messagesexchangedbetweendierent PE's,and frequencies
oftransitionexecution.
The ILP Model (for details see [26,25]) consists of an objective function
thatminimizesthecommunicationcostanddecidesonanoptimalallocationof
resources,basedonasetofconstraints.Theseconstraintsarebasedontheabove
synthesisrules,and theyconsistof 0-1integervariablesindicating(a) whether
aPEshould send amessageornot, (b)whether amessagecontains aregister
valueornot,or(c)whether aregister/gateisallocatedtoaPEornot.
4 Protocol Re-synthesis
In this section, we present our new method for re-synthesizing the protocol
specication from a modied service specication. The method consists of a
set of rulesthat wouldbeapplied to dierent PE'safter amodicationto the
servicespecication,inordertoproducenewsynthesized(re-synthesized)PE's.
Foreachsimplemodication(henceforthcalledatomicmodication)madeon
theservice specicationSspec,wedeneits correspondingatomic re-synthesis
rules.Asshownlater,theseatomicre-synthesisrulescanalsobesequentially
ap-pliedtodealwithmorethanonemodication.Notethattheatomicre-synthesis
rules arebasedonthesynthesisrulesdescribedin Section 3.Consequently, we
rules arebasedonthesynthesisrulesdescribedin Section 3.Consequently, we