铁道通信信号
鐵道通信信號
철도통신신호
RAILWAY SIGNALLING & COMMUNICATION
2013年
2期
80-84
,共5页
列车控制系统%需求规范%形式化方法%UML%属性规范语言
列車控製繫統%需求規範%形式化方法%UML%屬性規範語言
열차공제계통%수구규범%형식화방법%UML%속성규범어언
采用基于属性的分析方法,对CTCS-3级列控系统需求规范进行形式化验证.首先建立UML模型并转换为PSL模型.然后通过仿真运行,不断修正该模型,得到可实现的PSL模型.最后运用验证工具对PSL模型进行相关属性的验证,通过反例对错误进行定位和修改.以需求规范中的模式转换为例,采用该方法对其可达性、转移性及死锁性进行验证,验证过程表明基于属性的分析方法适用于CTCS-3级列控系统需求规范的验证.
採用基于屬性的分析方法,對CTCS-3級列控繫統需求規範進行形式化驗證.首先建立UML模型併轉換為PSL模型.然後通過倣真運行,不斷脩正該模型,得到可實現的PSL模型.最後運用驗證工具對PSL模型進行相關屬性的驗證,通過反例對錯誤進行定位和脩改.以需求規範中的模式轉換為例,採用該方法對其可達性、轉移性及死鎖性進行驗證,驗證過程錶明基于屬性的分析方法適用于CTCS-3級列控繫統需求規範的驗證.
채용기우속성적분석방법,대CTCS-3급렬공계통수구규범진행형식화험증.수선건립UML모형병전환위PSL모형.연후통과방진운행,불단수정해모형,득도가실현적PSL모형.최후운용험증공구대PSL모형진행상관속성적험증,통과반례대착오진행정위화수개.이수구규범중적모식전환위례,채용해방법대기가체성、전이성급사쇄성진행험증,험증과정표명기우속성적분석방법괄용우CTCS-3급렬공계통수구규범적험증.
