搜索
本科毕业设计外文文献及译文文献、资料题目：Specification,AnalysisandVerificationofanAutomatedParkingGarage文献、资料来源：谷歌学术文献、资料发表（出版）日期：2005院（部）：机电工程学院专业：机械工程及自动化班级：机械112姓名：江治国学号：2011071154指导教师：刘辉翻译日期：2015.3.10山东建筑大学毕业设计外文文献及译文-1-外文文献：Specification,AnalysisandVerificationofanAutomatedParkingGarageAadMathijssen,A.JohannesPretoriusAbstractInthisreportwediscussthespecification,analysisandverificationofanautomatedparkinggarageinmCRL2,aprocessalgebrawithdata.Weviewtheparkinggarageasasystemthatweconceptuallydivideintothreelayers:alogicallayer,asafetylayerandahardwareabstractionlayer.Thisallowsustoabstractfromimplementationdetails(hardwareabstractionlayer)andalgorithmdesign(logicallayer).Instead,weareabletofocusonthespecificationofacommunicationinterfacebetweenthesetwolayersthatonlyallowssafesystembehavior.Thisinterfaceconstitutesthesafetylayer.Forthesafetylayer,weidentifyandformulateanumberofrequirements.Theseareverifiedandreportedon.Wealsodiscusstheanalysisofthespecificationofthesafetylayerwithasimplecustomvisualizationtool.Thistoolwasimplementedasaplug-intothemCRL2toolsetandhelpedusgainimportantinsightsduringthespecificationandanalysisofthesafetylayer.1IntroductionDuringthepasttwodecadesprocessalgebrashavebecomeincreasinglypopulartoolsfordescribingcomplexsystemsthatinteractwiththeirenvironment[5].Suchsystemsdifferfromclassicbatchprocessesthatreceiveinput,processtheinput,produceoutputandthenterminate.Instead,theirbehavioriscontinuouslyinfluencedbyinformationthattheyreceivefromtheirenvironment.Anautomatedparkinggarageisaprimeexampleofsuchasystem.Itisinoperation24hoursaday,7daysaweek:itiscontinuouslyonstandby,readytostowawayandretrievecarsforusers.Furthermore,thestateofthegarageisconstantlychangingascarsareaddedandremoved.Atanypointintime,thisstateinfluenceswhichoperationsarepossibleandhowtheyareexecuted.Processalgebraallowsforhigh-leveldescriptionsofsystemsthatinteractwiththeirenvironment.Asystemisregardedasanumberofinteractingprocessesthattogetherdescribeitsbehaviour.Inthiswayamathematicalmodelisacquiredandthisisusedtoprovevarious山东建筑大学毕业设计外文文献及译文-2-propertiesofthesystemusingmathematicalprooftechniques.TheprocessalgebrausedinthisreportismCRL2[3].ItsucceedsandextendsµCRL[4,5].WithµCRLalargenumberofreal-worldsystemshavebeenanalysedandverified.SomeofthesuccessesthatµCRLhasbookedincludethedetectionofanunknowndeadlockinthemostcomplexvariantoftheslidingwindowprotocol[1,11],theidentificationofanumberoferrorsinadistributedliftingsystemfortrucks[2]andthediscoveryoftwoerrorsinaJavadistributedmemoryimplementation[9].Fromalltheseexperimentsweunfortunatelyhavehadtoformulatethe100%rule:in100%ofthecasesconsidered,systemsturnouttocontainmoreorlessseriouserrors,whicharenotveryhardtodetect.AnimportantcharacteristicofmCRL2anditspredecessorµCRListheinclusionofdata.Experiencehasshownthatinreal-worldsystemsdataisofparamountimportance[6].Inadditiontotheexecutionofactions,itisoftenthecasethatdataisstoredandcommunicated,thushavingasignificantinfluenceonsystembehaviour.IntheremainderofthisreportwediscussthespecificationofanautomatedparkinggarageinmCRL2.Wealsodiscusstheanalysisandverificationofthesystemandthetechniquesused.Insection2weprovidemoredetailsonthechallengespresentedbythissystem.Insection3weoutlinetheapproachwehavetakentoaddresstheseissuesandweexplainhowweconceptuallydividethesystemintothreelayers.Thisallowsustoconcentrateononelayer,thesafetylayer,whichwebelieveisessentialinverifyingthatthesystemissafe.WefollowthisbyadiscussionofmCRL2andthemCRL2toolsetinsection4.Insections5,6and7wespecifythehardwareabstractionlayer,thesafetylayerandthelogicallayerrespectively.Wetreatthehardwareabstractionlayerandthelogicallayerterselybutrevealmoredetailsofthesafetylayer:weprovideaspecification,formulateanumberofsafetyrequirementsandverifythese.Insection8wedescribeasimplevisualizationplug-inforthemCRL2toolsetaswellastheinsightswegainedfromusingit.Finally,wedrawconclusionsinsection9.2ProblemdescriptionTheparkinggaragethatweareconcernedwithwascommissionedbydevelopersinBremen,GermanyandwasdesignedbytheDutchcompanyCVSSAutomatedParkingSystems.Itwillberealisedbelowstreetlevelinthebasementofanexistingbuilding.Accesstothegaragewillbe山东建筑大学毕业设计外文文献及译文-3-providedwithaverticalliftshaftthathasadoorwayatstreetlevel.Tousethefacility,userswilldrivetheircarthroughthisdoorwayintothelift.Aftertheyhaveexitedfromtheircarandthelift,theircarwillautomaticallybeloweredtoanintermediatelevel,rotated180◦horizontally,loweredtothebasementandstowedawayusinganumberofconveyorbeltsandshuttles.Whenauserwishestoretrieveacar,thissamesystemofconveyorbeltsandshuttleswillbeusedtobringthecartotheliftfromwhichitwillbebroughttostreetlevel.Sincethecarhadbeenrotatedbefore,itwillnowfacethedirectionofthestreet.Theuserstepsintothecaranddrivesawaythroughthedoorway.Thesystemwillprovideanumberofsecurityandsafetychecksduringcheck-inandcheck-outofacar.Thisincludesreadingatranspondercardonthecarandcheckingadatabaseofregisteredusersbeforeopeningthedoorwaytothelift.Asthecarisdrivenintothelift,theuserwillbeprovidedwithanumbero