属性驱动的列车控制系统需求建模与验证.pdf

《属性驱动的列车控制系统需求建模与验证.pdf》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、第23卷第2期Vol23No2团计算机应用RESEARCHANDD研EV究EL与OP开ME发NT史举编：1005-8451(2014)02，0001—06属性驱动的列车控制系统需求建模与验证何丽芸，赵林，程瑞军(北京交通大学轨道交通控制与安全国家重点实验室，北京100044)摘：形式化语言越来越多地用来描述列车控制系统需求规范，其精确的语法和语义一方面有助于创建精确的需求模型、消除理解差异，另一方面也为进一步分析验证提供了基础。通过提出一种基于属性的需求分析方法，利用具体的形式化技术来分析需求首先将由自然语言

2、描述的需求规范转换为属性描述语言(PSL)形式化规范，并通过仿真和博弈分别进行语义检查和可实现性验证，最后通过断言来检验形式化语言所刻画的系统的精确性和完整性。该方法从自然语言形式的需求约束中直接提取相关需求规范，构造形式化模型并进行验证，为需求的早期确认提供了一种新的实用途径。并以CTCS一3级列控系统RBC切换场景为例，说明该方法的有效性。炎键：需求规范；验证；列车控制系统；仿真；可实现性Ill分类：U284．4：TP39文献标识码：AProperty—drivenmodelingandverificat

3、ionforrequirementsofTrainControlSystemHELiyun．ZHA0Lin．CHENGRuijun(StateKeyLaboratoryofRailTramCControlandSafety,BeijingJiaotongUniversi~4Beijing100044，China)Abstract：FormallanguageswereincreasinglyusedtodescribetherequirementsspecificationofTrainControlSyst

4、em，theprecisesyntaxandsemanticsontheonehand，helpedtocreateaccuratedemandmodel，eliminatedunderstandingdifferences，ontheotherhandalsoprovidedabasisforfurtheranalysisofthevalidation．Thispaperpresentedapropertybasedrequirementsanalysisapproachwhichanalyzedrequi

5、rementbytheapplicationofspecializedformalanalysistechniques．Firstly,requirementsdescribedbynaturallanguageweretransformedintoformalrequirementsdescribedbyPSL(Prope~ySpecificationLanguage)．Secondly,thesemanticswerecheckedbysimulationandtherealizabilityoftheS

6、ystemwasverifiedbythegame．Finally,thecorrectnessandcompletenessoftheSystemwerevalidatedbyassurance．Thismethoddirectlyextractedtherelativerequirementsspecificationfromrequirementconstraintsdescribedbynatuxallanguageandformalizedthestructuresmodeltoverify,als

7、oprovidedanewpracticalwayfortheearlyvalidationoftherequirements．ByusingsomerequirementfragmentsfromRBCHandoverscenariosofCTCS一：；TrainControlSystemasarealisticexample，itwasdemonstratedtheefectivenessofthisapproach．Keywords：requirementsspecification；verificat

8、ion；TrainControlSystem；simulation；realizability需求规范是系统开发重要的依据性规范标准。统”)而言，其需求规范的缺陷往往造成不可估高质量的需求规范可以切断需求阶段的bug来源，量的财产损失和人员伤亡。具体来说，列控系统如果需求规范的质量控制不到位，极有可能会产需求规范大多都是依靠领域专家们的经验而制定生最原始的bug，并将会贯穿到整个系统开发的的，不可避