劉 磊
(中國鐵道科學(xué)研究院集團(tuán)有限公司通信信號研究所,北京 100081)
CTCS-3級列控系統(tǒng)(Chinese Train Control System Level 3)是一個將先進(jìn)的計算機(jī)技術(shù)、通信技術(shù)以及控制技術(shù)融合為一體的復(fù)雜安全苛求系統(tǒng)。國際標(biāo)準(zhǔn)IEC61508-1和歐洲鐵道行業(yè)EN50129均強(qiáng)烈推薦利用形式化方法對列控系統(tǒng)進(jìn)行分析[1-2], 因此針對CTCS-3級列控系統(tǒng)進(jìn)行建模和形式化分析對于完善系統(tǒng)功能和提高系統(tǒng)安全性顯得十分必要。
國內(nèi)針對CTCS-3級列控系統(tǒng)規(guī)范建模和形式化方法進(jìn)行了一系列的探索和研究,并取得大量成果[3-10]。文獻(xiàn)[8-10]采用能夠刻畫列控系統(tǒng)混成特性的Hybrid UML(HUML)對系統(tǒng)規(guī)范進(jìn)行半形式化建模,再利用模型轉(zhuǎn)化手段將其轉(zhuǎn)化為某一具體的形式化模型,最后利用模型檢驗的形式化分析方法進(jìn)行驗證,此方法便于使用計算機(jī)輔助工具,易于操作且自動化程度較高,在列控系統(tǒng)建模和形式化分析領(lǐng)域中得到廣泛應(yīng)用。但是,此方法針對系統(tǒng)安全性分析均是在形式化建模階段進(jìn)行,如建立故障模型、使用故障注入手段等,需要運用形式化復(fù)雜的數(shù)學(xué)理論,不利于在工業(yè)界推廣。
本文根據(jù)UML擴(kuò)展機(jī)制,對HUML進(jìn)行安全特性擴(kuò)展,對列控系統(tǒng)的安全需求和安全特性進(jìn)行描述,進(jìn)行半形式化模型安全設(shè)計,以半形式化模型為安全分析起點,從而達(dá)到降低形式化安全分析帶來的復(fù)雜度,便于在工業(yè)界推廣的效果。
統(tǒng)一建模語言 (Unified Modeling Language,UML)是一種定義良好、易于表達(dá),功能強(qiáng)大且普遍適用的圖形化、半形式化建模語言[11]。為了保持良好的應(yīng)用性,且能夠描述不同領(lǐng)域的特性和規(guī)則,UML底層設(shè)計了擴(kuò)展機(jī)制[12],UML的擴(kuò)展機(jī)制允許使用者設(shè)計UML概要文件(Profile),使用構(gòu)造型(Stereotype)、標(biāo)記值(Tagged Value)和約束(Constraint)三種擴(kuò)展機(jī)制自定義不同領(lǐng)域內(nèi)的元素[13]。
HUML是利用UML的概要文件擴(kuò)展機(jī)制,構(gòu)造出的能夠?qū)斐上到y(tǒng)建模的半形式化建模語言。該語言能夠?qū)α锌叵到y(tǒng)既包含離散時間變量又包含連續(xù)時間變量的混成性進(jìn)行建模。HUML按照功能結(jié)構(gòu)劃分為6個包,基礎(chǔ)包(Basics),數(shù)據(jù)類型包(Types),數(shù)據(jù)包(Data),表達(dá)式包(Expressions),通信包(Communi-cations)以及擴(kuò)展類和擴(kuò)展?fàn)顟B(tài)機(jī)包(Modes and Agents)[14],如圖1所示。
圖1 HUML元素模型包的關(guān)系
HUML元模型的這種包結(jié)構(gòu)描述了模型的組成元素和之間的抽象語法?;A(chǔ)包定義了建模中以抽象類存在的基本建模概念。數(shù)據(jù)類型包定義了基本數(shù)據(jù)類型。表達(dá)式包擴(kuò)展定義了約束(Constraint)和表達(dá)式(Expression)的形式。擴(kuò)展類和擴(kuò)展?fàn)顟B(tài)機(jī)包是模型的核心,定義了與擴(kuò)展類(Agent)和擴(kuò)展?fàn)顟B(tài)機(jī)(Mode)相關(guān)的所有元素。擴(kuò)展類創(chuàng)建了系統(tǒng)的框架結(jié)構(gòu),擴(kuò)展?fàn)顟B(tài)機(jī)描述了系統(tǒng)的動態(tài)交互行為[15]。
IBM Rational Software Architect(RSA)是一種應(yīng)用廣泛的基于UML的圖形化建模工具,用戶可以用組件化和可視化的方式為復(fù)雜系統(tǒng)進(jìn)行建模,本文中將其作為HUML以及HUML安全特性擴(kuò)展的原型軟件工具。
安全特性是指與系統(tǒng)安全性相關(guān)的一些元素,包括影響系統(tǒng)安全的相關(guān)元素和保障系統(tǒng)安全的相關(guān)元素。其中,前者是指系統(tǒng)在運行過程中可能出現(xiàn)的故障,以及用以表述這些故障的成分,如類型、苛求程度等。后者是指系統(tǒng)在設(shè)計過程中應(yīng)當(dāng)采取的用以保障系統(tǒng)安全或達(dá)到一定安全完善度等級的措施、性能指標(biāo)等。對HUML進(jìn)行擴(kuò)展的主要目的就是期望HUML能夠?qū)@些元素進(jìn)行描述。
在進(jìn)行HUML擴(kuò)展時,可將安全特性相關(guān)元素放在一個獨立的安全特性包中。安全特性包定義了安全特性相關(guān)元素,以及各個元素之間的關(guān)系。這樣可以在現(xiàn)有的模型上疊加安全特性元素而無需改變原有的模型元素。安全特性包中的元素由HUML模型元素擴(kuò)展而來,將HUML的模型元素作為安全特性元素的擴(kuò)展基礎(chǔ)??梢栽诓桓淖僅UML模型元素的基礎(chǔ)上增加安全特性元素,令新的HUML既可以進(jìn)行混成特性建模,又可以包含安全特性元素。
將安全特性包加入HUML元模型中,構(gòu)成新的HUML元模型。根據(jù)各個元素的類別不同,可以將所有的元素分成7個不同的包,如圖2所示。
圖2 安全特性擴(kuò)展后的HUML元模型
圖2描述了擴(kuò)展后的HUML元模型中各個元素包的關(guān)系,在新的元模型中,安全特性包僅與基礎(chǔ)包、類型包、表達(dá)式包以及擴(kuò)展類和擴(kuò)展?fàn)顟B(tài)機(jī)包有關(guān)。安全特性包中的元素及其之間的關(guān)系,如圖3所示。
圖3中各元素的含義如下。
(1)故障(Fault):故障描述了系統(tǒng)在運行過程中可能會出現(xiàn)的異常情況。根據(jù)CTCS-3級列控系統(tǒng)的不同組成部分,可細(xì)分為人機(jī)接口故障(MMI_Fault)、列車接口故障(TI_Fault)、車載計算機(jī)故障(KERNEL_Fault)、測速單元故障(ODO_Fault)、無線閉塞中心故障(RBC_Fault)以及與信息傳輸相關(guān)的設(shè)備功能故障(TRANS_Fault)等。
圖3 安全特性包中元素及關(guān)系
(2)故障類型(Fault Type):故障類型描述了具體的故障所屬類型,根據(jù)故障所涉及到的不同功能,具體可分為信息重復(fù)(Repetition),功能或信息不合時宜的出現(xiàn)(Insertion),信息順序錯誤(Resequence),信息丟失(Del-etion),延遲(Delay),功能錯誤或數(shù)據(jù)錯誤(Corruption),信息錯誤(Masquerade),功能缺失(Absent),功能實時時機(jī)錯誤(Timing),實施錯誤的功能(Incorrect),測速或測距偏大(More),測速或測距偏小(Less)等。
(3)苛求度(Criticality):苛求度描述了故障所涉及的功能或數(shù)據(jù)對于列控系統(tǒng)安全的影響程度。根據(jù)安全分析的結(jié)果,將故障涉及的功能或數(shù)據(jù)分為三類:安全苛求的(Safety Critical)、安全相關(guān)的(Safety Related)和安全無關(guān)的(No Safety Related)。
(4)緩解措施(Fault Mitigation):緩解措施是針對安全苛求或者安全相關(guān)的失效功能而提出的緩解辦法,主要目的是降低該功能失效的頻率或者失效帶來的影響。當(dāng)然,不是所有的功能都具有緩解措施,譬如有些系統(tǒng)的固有的核心功能一旦故障,是無法進(jìn)行緩解的(不包括冗余設(shè)計措施)。
(5)危險容忍率(THR):危險容忍率(Tolerable Hazard Rate, THR)是指在滿足一定的安全完善度等級前提下,允許危險發(fā)生的最大頻率。危險容忍率屬于系統(tǒng)級指標(biāo),根據(jù)系統(tǒng)的組成以及安全分析的結(jié)果,可對各子系統(tǒng)進(jìn)行THR的分配。
(6)安全性策略(Safety Policy):上述危險容忍率分配以及緩解措施的制定共同構(gòu)成用于保障系統(tǒng)安全的安全性策略。
面向列控系統(tǒng)安全特性對HUML進(jìn)行擴(kuò)展,本質(zhì)就是在HUML模型元素的基礎(chǔ)上進(jìn)行安全特性擴(kuò)展,通過建立概要文件,創(chuàng)建構(gòu)造型的方式,對需要擴(kuò)展的元素進(jìn)行定義。創(chuàng)建的概要文件及定義的元素如表1所示。
表1 概要文件及構(gòu)造型
下面對表1中概要文件各部分進(jìn)行詳細(xì)介紹。
HUML元模型中數(shù)據(jù)類型包定義了所用數(shù)據(jù)類型,數(shù)據(jù)類型包中包括元類元素枚舉類型(Enumer-ation),安全特性包中故障類型(Fault Type),苛求度(Criticality)則是元類元素枚舉類型(Enumeration)的擴(kuò)展,在RSA工具中,可通過圖4所示的構(gòu)造型擴(kuò)展實現(xiàn)。
圖4 數(shù)據(jù)類型的構(gòu)造型實現(xiàn)
HUML元模型中表達(dá)式包定義了表達(dá)式和約束,安全元素包中所用的危險容忍率(THR)是對HUML元類元素表達(dá)式的擴(kuò)展,緩解措施(Fault Mitigation)是HUML元類元素約束的擴(kuò)展,在RSA工具中,可通過下述構(gòu)造型擴(kuò)展實現(xiàn),如圖5所示。
圖5 表達(dá)式及約束的構(gòu)造型實現(xiàn)
故障(Fault)作為安全元素的核心,屬于元類元素(信號)的擴(kuò)展,為了簡化RSA實現(xiàn)過程,以信號事件的形式表示功能故障事件。因為故障不會像信號一樣存在發(fā)出和接受的執(zhí)行動作,因此采用布爾型的取值規(guī)則表示故障的發(fā)生與否,同時會觸發(fā)狀態(tài)圖的遷移。由于系統(tǒng)存在不同的功能單元,其故障表示方式也不同,因此可以根據(jù)系統(tǒng)特性,對Fault進(jìn)行細(xì)化,綜合兩方面,在RSA工具中,可通過圖6所示構(gòu)造型擴(kuò)展實現(xiàn)。
圖6 Fault構(gòu)造型實現(xiàn)
擴(kuò)展類和擴(kuò)展?fàn)顟B(tài)機(jī)包中描述了前述的危險容忍率(THR)、故障(Fault)等元素與類(Agent)的關(guān)系,即描述了如何在建模過程中體現(xiàn)這些安全特性元素。
圖7給出了Agent元素與安全特性元素的關(guān)系,即類具有相應(yīng)的故障事件,構(gòu)造安全參數(shù)(safepara)代表安全完善度等級,根據(jù)相應(yīng)的安全完善度等級會對該類進(jìn)行THR的分配。其中,THR分配過程會以參數(shù)表達(dá)式的形式存在。RSA工具中,可通過圖7所示的構(gòu)造型擴(kuò)展實現(xiàn)。
圖7 Agent構(gòu)造型實現(xiàn)
圖8 車載設(shè)備建模示意
以CTCS-3級列控系統(tǒng)車載設(shè)備為例,建立包含安全特性的類圖,如圖8所示,圖中的車載設(shè)備類(OBE),包含幾個故障事件,例如,車載設(shè)備無法施加制動 (F_NotBrake)具有類型以及苛求度的特征;車載設(shè)備位置錯誤(F_IncorrectDistance),屬于功能錯誤(corruption)類型、安全相關(guān)(SafetyRelated)的故障。同時,通過參數(shù)表達(dá)式的形式給出了THR的分配信息。對于可緩解的故障事件,會存在《Fault Mitigation》的緩解措施,例如車載設(shè)備位置錯誤(F_Incorrect Distance)存在應(yīng)答器鏈接反應(yīng)(linking reaction)的緩解措施。
本文基于UML的擴(kuò)展機(jī)制,提出一種面向列控系統(tǒng)安全特性的HUML擴(kuò)展方法,擴(kuò)展后的HUML能夠在建模過程中對列控系統(tǒng)的安全特性進(jìn)行描述。此方法彌足了HUML模型無法直接刻畫列控系統(tǒng)安全特性的不足,為列控系統(tǒng)建模和形式化分析提供了一條新的思路。由于RSA軟件的一些限制,有些設(shè)計沒有完全實現(xiàn),僅是通過現(xiàn)有元素進(jìn)行代替。為此,可進(jìn)一步研究UML的擴(kuò)展機(jī)制,在現(xiàn)有RSA有限表達(dá)能力的情況下實現(xiàn)表達(dá)能力更好的概要文件。