基于UML的列控系統(tǒng)建模策略及驗(yàn)證工具集成

1、基于UML的列控系統(tǒng)建模策略及驗(yàn)證工具集成2基于UML機(jī)制的列控系統(tǒng)需求規(guī)范建模方法介紹規(guī)范是系統(tǒng)開(kāi)發(fā)的起點(diǎn)和基礎(chǔ)，系統(tǒng)規(guī)范的缺陷將給項(xiàng)目成功帶來(lái)極大的風(fēng)險(xiǎn)。對(duì)于列控系統(tǒng)這樣安全荀求系統(tǒng)而言，系統(tǒng)需求規(guī)范中的任何缺陷都有可能由潛在的風(fēng)險(xiǎn)演變成系統(tǒng)失效從而導(dǎo)致安全事故的發(fā)生。因此，以列控系統(tǒng)需求規(guī)范為研究對(duì)象，本章將對(duì)其所體現(xiàn)的混成特性建模需求進(jìn)行分析，研究UML擴(kuò)展機(jī)制，充分挖掘UML的圖形功能，設(shè)計(jì)面向列控系統(tǒng)需求規(guī)范的混成UML概要文件，使之能夠包含更多的內(nèi)容與信息去準(zhǔn)確地刻畫(huà)列控系統(tǒng)的混成特性，最后介紹建模所選擇的工具。2.1列控系統(tǒng)需求規(guī)范建模的需求分析針對(duì)列控領(lǐng)域的建模需求擴(kuò)展UML

2、，首先要為其提供刻畫(huà)連續(xù)動(dòng)態(tài)行為的能力，擴(kuò)展后的UML類(lèi)似于一種特定領(lǐng)域語(yǔ)言(Domain-Specific Language)。這種做法在其他領(lǐng)域有成功的先例，例如，對(duì)于實(shí)時(shí)和嵌入式系統(tǒng)，OMG發(fā)布了一個(gè)標(biāo)準(zhǔn)的 UML 擴(kuò)展規(guī)范 MARTE41(UML Profile for Modeling and Analysis of Real-Timeand Embedded Systems)。其次，這種擴(kuò)展應(yīng)具有層次化和可組合的特性，基于混成自動(dòng)機(jī)的底層語(yǔ)義，使得在其上進(jìn)行形式推理和驗(yàn)證成為可能。針對(duì)列控系統(tǒng)混成特性的建模需通過(guò)帶有連續(xù)變量的微分表達(dá)式刻畫(huà)系統(tǒng)中連續(xù)的物理過(guò)程以及保持這些過(guò)程的微分

3、動(dòng)態(tài)約束條件；以及以不變集或信號(hào)事件等為條件的狀態(tài)遷移刻畫(huà)離散變化過(guò)程。面向列控領(lǐng)域UML建模的難點(diǎn)在于創(chuàng)建能夠刻畫(huà)列控領(lǐng)域混成特性的UML概要文件。具體對(duì)刻畫(huà)列控領(lǐng)域混成特性的所有元素(已存在的元類(lèi)元素和擴(kuò)展元素)進(jìn)行分析，可根據(jù)元素間的擴(kuò)展與被擴(kuò)展關(guān)系、擴(kuò)展元素之間的應(yīng)用關(guān)系，按功能分為六個(gè)包(見(jiàn)圖2-1):基礎(chǔ)包(Basicspackage),數(shù)據(jù)類(lèi)型包(Types package)，數(shù)據(jù)包(Data package)，表達(dá)式包(Expressionspackage)，通信包(Communications package)，擴(kuò)展類(lèi)和擴(kuò)展?fàn)顟B(tài)機(jī)包(Modes andAgents packa

4、ge)。2.2 UML擴(kuò)展機(jī)制UML概要文件主要由原型組成，一個(gè)原型定義了與其關(guān)聯(lián)的UML類(lèi)(即元對(duì)象類(lèi))、這個(gè)類(lèi)的屬性及這個(gè)原型元素與其它元素如何進(jìn)行關(guān)聯(lián)的約束條件。在概要文件中對(duì)原型進(jìn)行描述，主要依照三種擴(kuò)展機(jī)制：(1)標(biāo)稱(chēng)值(TaggedValue)標(biāo)記值是對(duì)一個(gè)特性的顯式定義，是一種用于指定模型元素性質(zhì)的機(jī)制。它由一個(gè)標(biāo)記字符串和一個(gè)值字符串組成，可以連接到任何元素上，可以給一個(gè)元素增加一些新的語(yǔ)義。標(biāo)記值已成為一種用來(lái)提高模型質(zhì)量以提供附加信息的有效方法。(2)約束(Constrains)約束是指作用于一個(gè)或多個(gè)元素之上的語(yǔ)義條件或限制，即使用一個(gè)表達(dá)式把約束應(yīng)用于元素上。它是用大括

5、弧內(nèi)的字符串表達(dá)式來(lái)表示的，可以附加在依賴(lài)、注釋等元素上以表示約束和關(guān)系，因此可以用來(lái)對(duì)模型元素進(jìn)行語(yǔ)義上的限制。在定義一個(gè)約束時(shí)，應(yīng)該給出該用戶(hù)自定義約束將應(yīng)用于哪一種元素以及對(duì)相關(guān)元素的語(yǔ)義影響力。在UML2.0中，對(duì)象約束語(yǔ)言(Object Constraint Language.簡(jiǎn)稱(chēng)OCL)提供了一種標(biāo)準(zhǔn)方法來(lái)明確表達(dá)UML2.0模型上的約束。(3)構(gòu)造型(Stereotype)構(gòu)造型是最復(fù)雜的擴(kuò)展機(jī)制，這種機(jī)制是基于一個(gè)己存在的模型元素定義一種新的模型元素，通過(guò)構(gòu)造型來(lái)標(biāo)識(shí)那些可以被重用而不需要由轉(zhuǎn)換生成的元素。一方面，新的模型元素只是已有模型元素的子類(lèi)，通過(guò)泛化關(guān)系繼承了其元對(duì)象類(lèi)

6、的形式和特征；另一方面，由于添加了額外的語(yǔ)義，新的模型元素實(shí)現(xiàn)了對(duì)其基類(lèi)的擴(kuò)展。構(gòu)造型是原型的直觀(guān)表現(xiàn)形式，通常有兩種：普通構(gòu)造型(簡(jiǎn)稱(chēng)構(gòu)造型)和枚舉構(gòu)造型(簡(jiǎn)稱(chēng)枚舉)。對(duì)于表現(xiàn)形式為構(gòu)造型的原型，至少應(yīng)該具有1個(gè)(可有多個(gè))與它關(guān)聯(lián)的元對(duì)象類(lèi)。本文主要通過(guò)向構(gòu)造型加入屬性的方式來(lái)對(duì)元類(lèi)元素進(jìn)行結(jié)構(gòu)上的擴(kuò)展，或通過(guò)加注釋的形式進(jìn)行靜態(tài)語(yǔ)義的擴(kuò)展，這種概要文件擴(kuò)展機(jī)制，使得擴(kuò)展的定義更容易被理解，擴(kuò)展元素之間的相互關(guān)系、以及擴(kuò)展元素與UML模型之間的應(yīng)用關(guān)系都更加清晰、準(zhǔn)確而完整。2基于UML擴(kuò)展機(jī)制的列控系統(tǒng).92.1列控系統(tǒng)需求規(guī)范建模的.92.2UML擴(kuò)展機(jī)制.102.3面向列控系統(tǒng)需求規(guī)

7、范的.112.4RSA建模工具.183列控系統(tǒng)需求規(guī)范模型的.213.1列控系統(tǒng)需求規(guī)范分析.213.2列控系統(tǒng)需求模型驗(yàn)證分析.223.3列控系統(tǒng)需求規(guī)范驗(yàn)證支持.233.4列控系統(tǒng)需求規(guī)范驗(yàn)證支持工具.253.5列控系統(tǒng)需求規(guī)范驗(yàn)證支持工具.375結(jié)論我國(guó)軌道交通正處于高速發(fā)展時(shí)期，干線(xiàn)列車(chē)提速、客運(yùn)專(zhuān)線(xiàn)、高速鐵路建設(shè)需要安裝使用列車(chē)運(yùn)行控制系統(tǒng)來(lái)確保列車(chē)運(yùn)行安全。對(duì)于列控系統(tǒng)而言，離散的計(jì)算過(guò)程和連續(xù)的物理過(guò)程在開(kāi)放環(huán)境下持續(xù)交互并深度融合，為其建模和驗(yàn)證工作增添了不少難度。以列控系統(tǒng)需求規(guī)范為研宄對(duì)象，一方面，需要提出一種合理的框架結(jié)構(gòu)以對(duì)其混成特性進(jìn)行建模。統(tǒng)一建模語(yǔ)言(UML)作為

8、一種廣泛使用的面向?qū)ο蟮目梢暬y(tǒng)一建模語(yǔ)言，己被應(yīng)用到不同的領(lǐng)域，但混成特性的描述己經(jīng)遠(yuǎn)遠(yuǎn)超出了這種建模語(yǔ)言本身的能力范圍。另一方面，對(duì)系統(tǒng)進(jìn)行驗(yàn)證的需求來(lái)看，形式化方法為規(guī)范驗(yàn)證提供了一條重要的解決途徑，供研宄人員使的形式化驗(yàn)證工具種類(lèi)繁多，可集成幾種常用的形式化驗(yàn)證工具，支持列控系統(tǒng)規(guī)范的驗(yàn)證分析工作。因此，本文針對(duì)列控系統(tǒng)需求規(guī)范，著眼于運(yùn)用UML自身所提供的擴(kuò)展機(jī)制研宄一種有效的建模方法；并在Eclipse平臺(tái)上完成了一個(gè)驗(yàn)證支持工具的軟件原型開(kāi)發(fā)。重點(diǎn)包括了如下的幾個(gè)方面：(1)準(zhǔn)備工作階段，闡述了工作的選題目的和立體意義，概述了CTCS-3級(jí)列控系統(tǒng)的系統(tǒng)結(jié)構(gòu)，了解國(guó)內(nèi)外形式化建模驗(yàn)證方法的研究現(xiàn)狀，并借鑒國(guó)內(nèi)外已有的形式化驗(yàn)證工具集成平臺(tái)的開(kāi)發(fā)經(jīng)驗(yàn)。(2)建模階段，從列控系統(tǒng)需求規(guī)范建模的需求著手進(jìn)行分析，針對(duì)列