基于HUML擴(kuò)展機(jī)制描述列控系統(tǒng)安全特性的研究

劉 磊

(中國(guó)鐵道科學(xué)研究院集團(tuán)有限公司通信信號(hào)研究所,北京 100081)

1 概述

CTCS-3級(jí)列控系統(tǒng)(Chinese Train Control System Level 3)是一個(gè)將先進(jìn)的計(jì)算機(jī)技術(shù)、通信技術(shù)以及控制技術(shù)融合為一體的復(fù)雜安全苛求系統(tǒng)。國(guó)際標(biāo)準(zhǔn)IEC61508-1和歐洲鐵道行業(yè)EN50129均強(qiáng)烈推薦利用形式化方法對(duì)列控系統(tǒng)進(jìn)行分析[1-2]， 因此針對(duì)CTCS-3級(jí)列控系統(tǒng)進(jìn)行建模和形式化分析對(duì)于完善系統(tǒng)功能和提高系統(tǒng)安全性顯得十分必要。

國(guó)內(nèi)針對(duì)CTCS-3級(jí)列控系統(tǒng)規(guī)范建模和形式化方法進(jìn)行了一系列的探索和研究，并取得大量成果[3-10]。文獻(xiàn)[8-10]采用能夠刻畫列控系統(tǒng)混成特性的Hybrid UML(HUML)對(duì)系統(tǒng)規(guī)范進(jìn)行半形式化建模，再利用模型轉(zhuǎn)化手段將其轉(zhuǎn)化為某一具體的形式化模型，最后利用模型檢驗(yàn)的形式化分析方法進(jìn)行驗(yàn)證，此方法便于使用計(jì)算機(jī)輔助工具，易于操作且自動(dòng)化程度較高，在列控系統(tǒng)建模和形式化分析領(lǐng)域中得到廣泛應(yīng)用。但是，此方法針對(duì)系統(tǒng)安全性分析均是在形式化建模階段進(jìn)行，如建立故障模型、使用故障注入手段等，需要運(yùn)用形式化復(fù)雜的數(shù)學(xué)理論，不利于在工業(yè)界推廣。

本文根據(jù)UML擴(kuò)展機(jī)制，對(duì)HUML進(jìn)行安全特性擴(kuò)展，對(duì)列控系統(tǒng)的安全需求和安全特性進(jìn)行描述，進(jìn)行半形式化模型安全設(shè)計(jì)，以半形式化模型為安全分析起點(diǎn)，從而達(dá)到降低形式化安全分析帶來(lái)的復(fù)雜度，便于在工業(yè)界推廣的效果。

2 HUML概述

2.1 UML擴(kuò)展機(jī)制

統(tǒng)一建模語(yǔ)言 (Unified Modeling Language，UML)是一種定義良好、易于表達(dá)，功能強(qiáng)大且普遍適用的圖形化、半形式化建模語(yǔ)言[11]。為了保持良好的應(yīng)用性，且能夠描述不同領(lǐng)域的特性和規(guī)則，UML底層設(shè)計(jì)了擴(kuò)展機(jī)制[12]，UML的擴(kuò)展機(jī)制允許使用者設(shè)計(jì)UML概要文件(Profile)，使用構(gòu)造型(Stereotype)、標(biāo)記值(Tagged Value)和約束(Constraint)三種擴(kuò)展機(jī)制自定義不同領(lǐng)域內(nèi)的元素[13]。

2.2 HUML概述

HUML是利用UML的概要文件擴(kuò)展機(jī)制，構(gòu)造出的能夠?qū)斐上到y(tǒng)建模的半形式化建模語(yǔ)言。該語(yǔ)言能夠?qū)α锌叵到y(tǒng)既包含離散時(shí)間變量又包含連續(xù)時(shí)間變量的混成性進(jìn)行建模。HUML按照功能結(jié)構(gòu)劃分為6個(gè)包，基礎(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)描述了模型的組成元素和之間的抽象語(yǔ)法。基礎(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)的動(dòng)態(tài)交互行為[15]。

2.3 建模軟件-RSA

IBM Rational Software Architect(RSA)是一種應(yīng)用廣泛的基于UML的圖形化建模工具，用戶可以用組件化和可視化的方式為復(fù)雜系統(tǒng)進(jìn)行建模，本文中將其作為HUML以及HUML安全特性擴(kuò)展的原型軟件工具。

3 安全特性需求和定義

3.1 安全特性需求

安全特性是指與系統(tǒng)安全性相關(guān)的一些元素，包括影響系統(tǒng)安全的相關(guān)元素和保障系統(tǒng)安全的相關(guān)元素。其中，前者是指系統(tǒng)在運(yùn)行過(guò)程中可能出現(xiàn)的故障，以及用以表述這些故障的成分，如類型、苛求程度等。后者是指系統(tǒng)在設(shè)計(jì)過(guò)程中應(yīng)當(dāng)采取的用以保障系統(tǒng)安全或達(dá)到一定安全完善度等級(jí)的措施、性能指標(biāo)等。對(duì)HUML進(jìn)行擴(kuò)展的主要目的就是期望HUML能夠?qū)@些元素進(jìn)行描述。

3.2 安全特性包定義

在進(jìn)行HUML擴(kuò)展時(shí)，可將安全特性相關(guān)元素放在一個(gè)獨(dú)立的安全特性包中。安全特性包定義了安全特性相關(guān)元素，以及各個(gè)元素之間的關(guān)系。這樣可以在現(xiàn)有的模型上疊加安全特性元素而無(wú)需改變?cè)械哪Ｐ驮亍０踩匦园械脑赜蒆UML模型元素?cái)U(kuò)展而來(lái)，將HUML的模型元素作為安全特性元素的擴(kuò)展基礎(chǔ)。可以在不改變HUML模型元素的基礎(chǔ)上增加安全特性元素，令新的HUML既可以進(jìn)行混成特性建模，又可以包含安全特性元素。

將安全特性包加入HUML元模型中，構(gòu)成新的HUML元模型。根據(jù)各個(gè)元素的類別不同，可以將所有的元素分成7個(gè)不同的包，如圖2所示。

圖2 安全特性擴(kuò)展后的HUML元模型

圖2描述了擴(kuò)展后的HUML元模型中各個(gè)元素包的關(guān)系，在新的元模型中，安全特性包僅與基礎(chǔ)包、類型包、表達(dá)式包以及擴(kuò)展類和擴(kuò)展?fàn)顟B(tài)機(jī)包有關(guān)。安全特性包中的元素及其之間的關(guān)系，如圖3所示。

圖3中各元素的含義如下。

(1)故障(Fault)：故障描述了系統(tǒng)在運(yùn)行過(guò)程中可能會(huì)出現(xiàn)的異常情況。根據(jù)CTCS-3級(jí)列控系統(tǒng)的不同組成部分，可細(xì)分為人機(jī)接口故障(MMI_Fault)、列車接口故障(TI_Fault)、車載計(jì)算機(jī)故障(KERNEL_Fault)、測(cè)速單元故障(ODO_Fault)、無(wú)線閉塞中心故障(RBC_Fault)以及與信息傳輸相關(guān)的設(shè)備功能故障(TRANS_Fault)等。

圖3 安全特性包中元素及關(guān)系

(2)故障類型(Fault Type)：故障類型描述了具體的故障所屬類型，根據(jù)故障所涉及到的不同功能，具體可分為信息重復(fù)(Repetition)，功能或信息不合時(shí)宜的出現(xiàn)(Insertion)，信息順序錯(cuò)誤(Resequence)，信息丟失(Del-etion)，延遲(Delay)，功能錯(cuò)誤或數(shù)據(jù)錯(cuò)誤(Corruption)，信息錯(cuò)誤(Masquerade)，功能缺失(Absent)，功能實(shí)時(shí)時(shí)機(jī)錯(cuò)誤(Timing)，實(shí)施錯(cuò)誤的功能(Incorrect)，測(cè)速或測(cè)距偏大(More)，測(cè)速或測(cè)距偏小(Less)等。

(3)苛求度(Criticality)：苛求度描述了故障所涉及的功能或數(shù)據(jù)對(duì)于列控系統(tǒng)安全的影響程度。根據(jù)安全分析的結(jié)果，將故障涉及的功能或數(shù)據(jù)分為三類：安全苛求的(Safety Critical)、安全相關(guān)的(Safety Related)和安全無(wú)關(guān)的(No Safety Related)。

(4)緩解措施(Fault Mitigation)：緩解措施是針對(duì)安全苛求或者安全相關(guān)的失效功能而提出的緩解辦法，主要目的是降低該功能失效的頻率或者失效帶來(lái)的影響。當(dāng)然，不是所有的功能都具有緩解措施，譬如有些系統(tǒng)的固有的核心功能一旦故障，是無(wú)法進(jìn)行緩解的(不包括冗余設(shè)計(jì)措施)。

(5)危險(xiǎn)容忍率(THR)：危險(xiǎn)容忍率(Tolerable Hazard Rate， THR)是指在滿足一定的安全完善度等級(jí)前提下，允許危險(xiǎn)發(fā)生的最大頻率。危險(xiǎn)容忍率屬于系統(tǒng)級(jí)指標(biāo)，根據(jù)系統(tǒng)的組成以及安全分析的結(jié)果，可對(duì)各子系統(tǒng)進(jìn)行THR的分配。

(6)安全性策略(Safety Policy)：上述危險(xiǎn)容忍率分配以及緩解措施的制定共同構(gòu)成用于保障系統(tǒng)安全的安全性策略。

4 安全特性在UML概要文件中的實(shí)現(xiàn)

面向列控系統(tǒng)安全特性對(duì)HUML進(jìn)行擴(kuò)展，本質(zhì)就是在HUML模型元素的基礎(chǔ)上進(jìn)行安全特性擴(kuò)展，通過(guò)建立概要文件，創(chuàng)建構(gòu)造型的方式，對(duì)需要擴(kuò)展的元素進(jìn)行定義。創(chuàng)建的概要文件及定義的元素如表1所示。

表1 概要文件及構(gòu)造型

下面對(duì)表1中概要文件各部分進(jìn)行詳細(xì)介紹。

4.1 數(shù)據(jù)類型

HUML元模型中數(shù)據(jù)類型包定義了所用數(shù)據(jù)類型，數(shù)據(jù)類型包中包括元類元素枚舉類型(Enumer-ation)，安全特性包中故障類型(Fault Type)，苛求度(Criticality)則是元類元素枚舉類型(Enumeration)的擴(kuò)展，在RSA工具中，可通過(guò)圖4所示的構(gòu)造型擴(kuò)展實(shí)現(xiàn)。

圖4 數(shù)據(jù)類型的構(gòu)造型實(shí)現(xiàn)

4.2 表達(dá)式和約束

HUML元模型中表達(dá)式包定義了表達(dá)式和約束，安全元素包中所用的危險(xiǎn)容忍率(THR)是對(duì)HUML元類元素表達(dá)式的擴(kuò)展，緩解措施(Fault Mitigation)是HUML元類元素約束的擴(kuò)展，在RSA工具中，可通過(guò)下述構(gòu)造型擴(kuò)展實(shí)現(xiàn)，如圖5所示。

圖5 表達(dá)式及約束的構(gòu)造型實(shí)現(xiàn)

4.3 故障元素Fault

故障(Fault)作為安全元素的核心，屬于元類元素(信號(hào))的擴(kuò)展，為了簡(jiǎn)化RSA實(shí)現(xiàn)過(guò)程，以信號(hào)事件的形式表示功能故障事件。因?yàn)楣收喜粫?huì)像信號(hào)一樣存在發(fā)出和接受的執(zhí)行動(dòng)作，因此采用布爾型的取值規(guī)則表示故障的發(fā)生與否，同時(shí)會(huì)觸發(fā)狀態(tài)圖的遷移。由于系統(tǒng)存在不同的功能單元，其故障表示方式也不同，因此可以根據(jù)系統(tǒng)特性，對(duì)Fault進(jìn)行細(xì)化，綜合兩方面，在RSA工具中，可通過(guò)圖6所示構(gòu)造型擴(kuò)展實(shí)現(xiàn)。

圖6 Fault構(gòu)造型實(shí)現(xiàn)

4.4 擴(kuò)展類Agent

擴(kuò)展類和擴(kuò)展?fàn)顟B(tài)機(jī)包中描述了前述的危險(xiǎn)容忍率(THR)、故障(Fault)等元素與類(Agent)的關(guān)系，即描述了如何在建模過(guò)程中體現(xiàn)這些安全特性元素。

圖7給出了Agent元素與安全特性元素的關(guān)系，即類具有相應(yīng)的故障事件，構(gòu)造安全參數(shù)(safepara)代表安全完善度等級(jí)，根據(jù)相應(yīng)的安全完善度等級(jí)會(huì)對(duì)該類進(jìn)行THR的分配。其中，THR分配過(guò)程會(huì)以參數(shù)表達(dá)式的形式存在。RSA工具中，可通過(guò)圖7所示的構(gòu)造型擴(kuò)展實(shí)現(xiàn)。

圖7 Agent構(gòu)造型實(shí)現(xiàn)

5 案例

圖8 車載設(shè)備建模示意

以CTCS-3級(jí)列控系統(tǒng)車載設(shè)備為例，建立包含安全特性的類圖，如圖8所示，圖中的車載設(shè)備類(OBE)，包含幾個(gè)故障事件，例如，車載設(shè)備無(wú)法施加制動(dòng) (F_NotBrake)具有類型以及苛求度的特征；車載設(shè)備位置錯(cuò)誤(F_IncorrectDistance)，屬于功能錯(cuò)誤(corruption)類型、安全相關(guān)(SafetyRelated)的故障。同時(shí)，通過(guò)參數(shù)表達(dá)式的形式給出了THR的分配信息。對(duì)于可緩解的故障事件，會(huì)存在《Fault Mitigation》的緩解措施，例如車載設(shè)備位置錯(cuò)誤(F_Incorrect Distance)存在應(yīng)答器鏈接反應(yīng)(linking reaction)的緩解措施。

6 結(jié)語(yǔ)

本文基于UML的擴(kuò)展機(jī)制，提出一種面向列控系統(tǒng)安全特性的HUML擴(kuò)展方法，擴(kuò)展后的HUML能夠在建模過(guò)程中對(duì)列控系統(tǒng)的安全特性進(jìn)行描述。此方法彌足了HUML模型無(wú)法直接刻畫列控系統(tǒng)安全特性的不足，為列控系統(tǒng)建模和形式化分析提供了一條新的思路。由于RSA軟件的一些限制，有些設(shè)計(jì)沒有完全實(shí)現(xiàn)，僅是通過(guò)現(xiàn)有元素進(jìn)行代替。為此，可進(jìn)一步研究UML的擴(kuò)展機(jī)制，在現(xiàn)有RSA有限表達(dá)能力的情況下實(shí)現(xiàn)表達(dá)能力更好的概要文件。