資源描述：
《system description verification of distributed erlang programsnew》由會(huì)員上傳分享，免費(fèi)在線(xiàn)閱讀，更多相關(guān)內(nèi)容在教育資源-天天文庫(kù)。
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
