资源描述：
《system description verification of distributed erlang programsnew》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、SystemDescription:Veri cationofDistributedErlangPrograms12ThomasArts,MadsDam,Lars-akeFredlund,andDilianGurov1ComputerScienceLaboratory,EricssonTelecomAB,12625Stockholm,Sweden,E-mail:thomas@cslab.ericsson.se2SwedishInstituteofComputerScience,Box1263,S-16428Kista,Sweden,E-mail:fmfd,fred,diliang@s
2、ics.se1IntroductionSoftwarewrittenfortelecommunicationapplicationshastomeethighqualitydemands.Correctnessisonemajorconcern;theactivityofprovingformallythatasystemiscorrectiscalledveri cation.Telecommunicationssoftwareishighlyconcurrent,andtestingisoftennotcapableofguaranteeingcorrectnesstoasatis
3、factorydegree.Thesoftwarewearefacedwithconsistsofmany,relativelysmallmodules,writteninthefunctionallanguageErlang[AVWW96].Thesemodulesde nethebehaviourofanumberofprocessesoperatinginparallelandcommunicatingthroughasynchronousmessage-passing.Newprocessescanbegeneratedduringexecution.Becauseofthec
4、omplexityofsuchsoftware,ourapproachtoveri cationistoprovethatthesoftwaresatis esasetofpropertiescalledspeci cationandformalizedinasuitablelogiclanguage.Thespeci cationlanguageweuseisbasedonPark's-calculus[Par76,Koz83],extendedwithErlang-speci cfeatures.Thisisaverypowerfullogic,duetothepresenceo
5、fleastandgreatest xedpointrecursion,allowingtheformalizationofawiderangeofbehaviouralproperties.Veri cationinthiscontextisnotdecidable,butcanbeautomatedtoalargeextent,requiringhumaninterventioninafew,butcrucialpoints.Tofacilitateveri cationofErlangprogramsofrealisticsizewearedevel-opingaveri cat
6、iontoolimplementingatableau-basedproofsystemdescribedin[DFG98].Ourmainobjectivesaretoachieveasatisfactorydegreeofau-tomation,proofreuse,easynavigationthroughprooftableaux,andmeaningfulfeedbackaboutthecurrentproofstate,soastorequireuserinterventiononlywhenthisisreallynecessary,andtoassistintaking
7、informedproofdecisions.2TheErlangProgrammingLanguageWeconsideracorefragmentoftheErlangprogramminglanguagewithdynamicnetworksofprocessesoperatingondatatypessuchasnumbers,lists,tuples,orprocessidenti ers(pid's),usingasynchrono
