资源描述：
《creating implementations from promela models》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、CREATINGIMPLEMENTATIONSFROMPROMELAMODELS9SiegfriedLoffler,EcoleNationaleSuperieuredesTelecommunications,Departe-mentReseaux,46RueBarrault,75634ParisCedex13,FranceCurrentaddress:SiegfriedLoer,Hewlett{PackardLaboratories,FiltonRoad,StokeGif-ford,BristolBS126Q
2、Z,UKE-mailaddress:loeffler@res.enst.frAhmedSerhrouchni,EcoleNationaleSuperieuredesTelecommunications,Departe-mentReseaux,46RueBarrault,75634ParisCedex13,FranceE-mailaddress:ahmed@res.enst.fr8SIEGFRIEDLOFFLERANDAHMEDSERHROUCHNIIthastobementionedthatthecompile
3、ritselfisnotvalidatedandmostprob-ablystillcontainsquitealotofbugs.Thereforetheresultingimplementationsarenot100%validated.Anotherthingwhichislefttodoisavalidationoftheprotocolthatweusefortheconnectionofclientsandservers.Abasicdescriptionofthisprotocolcanbefo
4、undin[7].4.ConclusionsWithPROMELA/SPIN,Holzmannhasattackedtwoofthemainfactorsinhibitingmorewidespreaduseofspeci cationorvalidationtools,namelydicultyofuseandtheinherentlimitationsofthe nitestatereachabilitymethods.However,forthesteptothe nalimplementation,s
5、omedicultiesremain.ThemajordrawbackofPROMELAinitscurrentstateisthatthesemanticsarestillnotexactlyspeci ed,thereforeallowinginterpretationswhichmayleadtoproblemswhenimplementingthedesign.Anotherproblemisthemissingcapabilityofthelanguagetore nethespeci cation
6、inawaythatsucestodescribedetails(liketimeouts)ofanimplementation.OurextendedSPINtoolisusablefortherapidprototypingofvalidatedimple-mentationsofcommunicationprotocols.Becauseofourdi erentinterpretationoftheatomic"statement,itispossiblefortheimplementationto
7、behavenotexactlyasexpected.Thegeneratedimplementationisnot100%validatedbecausewehadtoaddcodeforaschedulerandforexternalcommunicationswhichhasnotbeenexhaustivelyveri ed.Themainapplication eldweseefortheimplementationsgeneratedwiththecurrentversionofourextende
8、dSPINtoolistherapidprototypingoftestingsce-narios.References[1]GerardJ.Holzmann,AT&T,DesignandValidationofComputerProtocols,PrenticeHall,1991[2]GerardJ.Holzmann,AT&T,What'sNewinSPINVersion2.0,in
