预览加载中，请您耐心等待几秒...

安全关键系统需求形式化建模分析实例研究.docx

预览
1/3
2/3
3/3

在线预览结束，喜欢就下载吧，查找使用更方便

下载提示 文本预览

如果您无法下载资料，请参考说明：

1、部分资料下载需要金币，请确保您的账户上有足够的金币

2、已购买过的文档，再次下载不重复扣费

3、资料包下载后请先用软件解压，在使用对应软件打开

安全关键系统需求形式化建模分析实例研究 Introduction Thesafetycriticalsystemisintendedforsuchasystemwherefailurecanresultinlossoflife,seriousinjuriesorsignificantenvironmentaldamage.Toavoidsuchadverseconsequences,safety-criticalsystemsneedtobedesigned,constructed,testedandmaintainedtothehighestlevelofsafetyandquality.Formalmodelingisoneofthetechniqueswidelyusedinthedevelopmentofsafety-criticalsystems.ThispaperprovidesanexampleofformalmodelingusingtheKIVsystemforthesafety-criticalsystemrequirementanalysis. KIVSystem TheKIVsystemisatoolforformalmodelcheckingandpropertyverification.Itisusedtomodelandanalyzecomplexsystemswithrigorousmathematicalmethods.TheKIVsystemsupportsthedevelopmentofformalmodelsusingavarietyofmodelinglanguages,includingprocessalgebras,temporallogics,andfirst-orderlogic.TheKIVsystemalsoprovidesautomatedsupportforanalysis,includingsymbolicexecution,modelchecking,andtheoremproving. Safety-CriticalSystem Thesafety-criticalsystemweareconsideringisarailwaysignallingsystem.Therailwaysignallingsystemisresponsibleforensuringthesafeandefficientmovementoftrains.Thesignallingsystemhastoprovidesignalstotraindriversthroughdisplaypanelsandincabindicators.Thesignallingsystemmustalsocontrolthepointswhichallowtrainstomovefromonetracktoanother. Requirementsanalysis Thefirststageoftheformalmodelingprocessisrequirementsanalysis.Inthisstage,weidentifythehigh-levelrequirementsofthesafety-criticalsystem.Therequirementsaredefinedthroughthefollowingsteps. Step1:Identifystakeholders Stakeholdersareindividualsororganizationsthathaveadirectorindirectinterestinthesafety-criticalsystem.Thestakeholdersfortherailwaysignallingsystemincludepassengers,trainoperators,maintenancepersonnel,andregulatoryauthorities. Step2:Determinetherequirements Therequirementsaredefinedbasedonthestakeholders'needsandexpectations.Therequirementsfortherailwaysignallingsystemincludethefollowing. 1.Thesignallingsystemmustensurethattrainsoperatesafely. 2.Thesignallingsystemshouldallowtrainstooperateefficiently. 3.Thesignalling