列控系統(tǒng)規(guī)范驗證的反例可視化研究 i 列控系統(tǒng)規(guī)范驗證的反例可視化研究 摘 要： 列控系統(tǒng)的規(guī)范已逐漸成形，而且對于列控系統(tǒng)這樣安全苛求系統(tǒng)而言，系統(tǒng)需求規(guī)范中的任何缺陷都有可能由潛在的風(fēng)險演變成系統(tǒng)失效從而導(dǎo)致安全事故的發(fā)生，因此對規(guī)范的形式化驗證就很有必要。但是由于形式化驗證的結(jié)果往往過于繁雜，工程技術(shù)人員不能很好地對結(jié)果進(jìn)行分析和追蹤，進(jìn)而提出了一些將得到的反例進(jìn)行可視化操作的研究。 目前存在許多研究，試圖結(jié)合 形式化方法的優(yōu)點(diǎn)，提供一種易于使用的并且根據(jù)需求提供相應(yīng)程度形式化驗證的軟件方法。這些方法一般先使用系統(tǒng)規(guī)范進(jìn)行 建模，然后將 形轉(zhuǎn)換成相應(yīng)的形式化規(guī)范語言，并使用相應(yīng)工具進(jìn)行驗證。但是形式化驗證和驗證結(jié)果的反例追蹤，目前并不能很好地標(biāo)注在 各類圖上，這為驗證錯誤的定位設(shè)置了極大障礙。 針對現(xiàn)有問題，本文結(jié)合密歇根大學(xué)計算機(jī)科學(xué)軟件工程與網(wǎng)絡(luò)系統(tǒng)實驗室提出的 視化框架，進(jìn)行列控系統(tǒng)規(guī)范驗證的反例可視化研究，利用 臺開發(fā)模型檢驗反例可視化插件，通過集成反例可視化與 模和驗證工具鏈，實現(xiàn)了列控系統(tǒng)規(guī)范建模、驗證和結(jié)果顯示的自動化。 關(guān)鍵詞： 列控規(guī)范；反例驗證；可視化 列控系統(tǒng)規(guī)范驗證的反例可視化研究 of of I as as if of is to of in of so its to to of So of At to ML an to on of ML to ML of of in ML so 控系統(tǒng)規(guī)范驗證的反例可視化研究 in of “is we do of of to 控系統(tǒng)規(guī)范驗證的反例可視化研究 錄 1 緒論 1 研究背景 1 研究現(xiàn)狀 2 國內(nèi)列控系統(tǒng)規(guī)范驗證現(xiàn)狀 2 可視化框架研究現(xiàn)狀 3 研究的目的和意義 5 論文的研究內(nèi)容 6 2 臺下列控系統(tǒng)規(guī)范的建模 7 件下的 模 7 統(tǒng)一建模語言 述 7 建模機(jī)制 8 臺及 件簡介 11 模示例 13 其他 臺 輯插件 17 19 述 19 列控聯(lián)鎖系統(tǒng)的建模 19 3 模型檢驗與反例的語法描述 21 模型檢驗 21 列控系統(tǒng)規(guī)范驗證的反例可視化研究 v 模型檢驗概述 21 模型檢驗算法 22 模型檢驗工具 25 反例的語法描述 26 言簡介 26 例應(yīng)用 29 4 反例文件的生成及文件格式的轉(zhuǎn)換 32 反例文件的生成 32 反例文件格式的轉(zhuǎn)換 33 可擴(kuò)展標(biāo)記語言（ 述 33 具簡介 34 式的反例文件 36 5 析 例文件 37 析算法概述 37 析 式反例文件 39 6 臺可視化插件的集成 40 界面的制作及功能的實現(xiàn) 40 插件界面的制作 40 插件功能的實現(xiàn) 42 反 例可視化插件效果演示 43 簡單的照明燈開關(guān)控制系統(tǒng) 43 列控系統(tǒng)站場圖聯(lián)鎖系統(tǒng) 44 列控系統(tǒng)規(guī)范驗證的反例可視化研究 總結(jié) 與展望 47 論文總結(jié) 47 展望 48 參考文獻(xiàn) 50 第 1 頁 1 1 緒論 研究背景 自 20 世紀(jì) 90 年代，歐美各國為制定軌道交通系統(tǒng)的技術(shù)規(guī)范做了許多工作，先后已制定多個有關(guān)軌道交通系統(tǒng)技術(shù)規(guī)范。而近年來，國內(nèi)逐漸開始重視列控系統(tǒng)規(guī)范的研究，鐵道部在 2002 年提出發(fā)展 國列車運(yùn)行控制系統(tǒng)）。因而，列控系統(tǒng)的規(guī)范已逐漸成形，而且對于列控系統(tǒng)這樣安全苛求系統(tǒng)而言，系統(tǒng)需求規(guī)范中的任何缺陷都有可能由潛在的風(fēng)險演變成系統(tǒng)失效從而導(dǎo)致安全事故的發(fā)生，因此對規(guī)范的形式化驗證就很有必要。目前存在許多研究，試圖結(jié)合 形式化方法的優(yōu)點(diǎn)，提供一種 易于使用的并且根據(jù)需求提供相應(yīng)程度形式化驗證的軟件方法。這些方法一般先使用 系統(tǒng)規(guī)范進(jìn)行建模，然后將 形轉(zhuǎn)換成相應(yīng)的形式化規(guī)范語言，并使用相應(yīng)工具進(jìn)行驗證。但是形式化驗證和驗證結(jié)果的反例追蹤，目前并不能很好地標(biāo)注在 各類圖上，這為驗證錯誤的定位設(shè)置了極大障礙。 目前國外有對安全系統(tǒng)形式化驗證的可視化框架，提出 目并利用 型驅(qū)動開發(fā)）的模式進(jìn)行開發(fā)，目的是將模型驗證的輸出文件解析后，利用 好地跟蹤標(biāo)注。但是依然存在兩個問題，一個是對反例的描述需要詳細(xì)、客觀 ;二是需要將導(dǎo)致錯誤的原因和路徑清楚地標(biāo)注在最原始的 上面。 針對這些問題，本課題列控系統(tǒng)規(guī)范驗證的反例可視化研究，就是通過解析模型檢驗的日志文件，提取反例涉及的狀態(tài)和遷移信息，實現(xiàn)規(guī)范 型的反例軌跡著色。利用 臺開發(fā)模型檢驗反例可視化插件是主要任務(wù)。反例可視化方便了規(guī)范錯誤的定位和查找；通過集成反例可視化與 現(xiàn)了列控系統(tǒng)規(guī)范建模、驗證和結(jié)果顯示的自動化，為將來的工程應(yīng)用奠定基礎(chǔ)。 第 2 頁 2 研究現(xiàn)狀 隨著世界各國軌道交通列車控制系統(tǒng)規(guī)范的重視，多個有關(guān)軌道 交通系統(tǒng)技術(shù)規(guī)范已經(jīng)成形并且投入使用，而國際上對于高可靠性系統(tǒng)的形式化驗證也已經(jīng)有了完善的可視化框架。本課題是將二者結(jié)合起來，將 視化框架應(yīng)用于列車控制系統(tǒng)規(guī)范的驗證當(dāng)中，下面分別介紹一下這兩者目前研究的現(xiàn)狀。 國內(nèi)列控系統(tǒng)規(guī)范驗證現(xiàn)狀 近年來，隨著我國鐵路跨越式發(fā)展戰(zhàn)略的實施，鐵路建設(shè)進(jìn)入了前所未有的高速發(fā)展時期?！笆晃濉逼陂g，我國先在膠濟(jì)、合寧線路上使用 2級列車控制系統(tǒng)，完成了第六次大提速任務(wù)。隨后不久又有使用 3 級列車控制系統(tǒng)的武廣、鄭西線路開始運(yùn)營，其 運(yùn)營速度最高達(dá)到 350/h?！笆濉逼陂g是中國鐵路高速發(fā)展的時期，干線鐵路將進(jìn)一步提速、多條客運(yùn)專線將開工建設(shè)、高速鐵路正在醞釀中。 在高速運(yùn)行條件下，迫切需要先進(jìn)的列車運(yùn)行控制系統(tǒng) (以下簡稱“列控系統(tǒng)” )保證列車運(yùn)行的安全和高效。列控系統(tǒng)是指將先進(jìn)的控制技術(shù)、計算機(jī)技術(shù)、通信技術(shù)與鐵路信號技術(shù)融為一體的行車指揮、控制、管理自動化系統(tǒng)。我國在參考?xì)W洲列車控制系統(tǒng) 的基礎(chǔ)上制定了中國列車控制系統(tǒng) 技術(shù)規(guī)范，保證列車安全運(yùn)行，并以分級形式滿足我國不同線路運(yùn)輸需求。 隨著計算機(jī)技術(shù)的提高，應(yīng)用在列控系統(tǒng)中計算機(jī)系統(tǒng)變得越來越復(fù)雜，規(guī)模也越來越大。復(fù)雜的系統(tǒng)很難設(shè)計開發(fā)，快速尋找錯誤和安全隱患也比較困難，一般的測試方法很難發(fā)現(xiàn)系統(tǒng)所有的設(shè)計故障，這會給軌道交通系統(tǒng)的安全、高效運(yùn)行帶來一定的安全隱患。因此，研究如何快速定位以及將錯誤的位置很好地標(biāo)注出來，以此保證系統(tǒng)設(shè)計正確性和安全性對列控系統(tǒng)來說顯得 第 3 頁 3 至關(guān)重要。 根據(jù)國際標(biāo)準(zhǔn) 1，對于安全苛求系統(tǒng)需求規(guī)范驗證，強(qiáng)烈推薦使用形式化方法。形式化方法提供了驗證系統(tǒng)設(shè)計正確性的一個重要途徑。它用數(shù)學(xué)方法表達(dá)系統(tǒng)的規(guī)范或系統(tǒng)的性質(zhì)，并且根據(jù)數(shù)學(xué)理論來證明所設(shè)計系統(tǒng)滿足系統(tǒng)的規(guī)范或具有期望的性質(zhì)。在不能證明所期望的性質(zhì)時，則可能發(fā)現(xiàn)設(shè)計錯誤。形式化方法是列控系統(tǒng)規(guī)范的建模和驗證的重要方法，代表著安全苛求系統(tǒng)規(guī)范建模、驗證研究和工程應(yīng)用的方向。 現(xiàn)階段，形式化方法在工業(yè)開發(fā)中的應(yīng)用還是比較少的。原因來自多個方面，首先，驗證一個計算機(jī)系統(tǒng)的規(guī)范、設(shè)計或?qū)崿F(xiàn)的正確性這個問題本身是一個非常復(fù)雜的問題。其次，傳統(tǒng)的工程人員對于形式化的描述方法 和分析、驗證技術(shù)不熟悉，而且這些概念和方法也不是很容易理解和掌握，因此難于在實際工程中運(yùn)用。 為了能夠在列車控制系統(tǒng)規(guī)范的驗證中使用形式化驗證的方法，因此提出一個驗證反例可視化的研究，希望通過可視化工具的使用快速定位錯誤，這樣工程技術(shù)人員可以最大地避免接觸形式化驗證繁雜的語法，以及花費(fèi)很大的代價去追溯產(chǎn)生規(guī)范錯誤的路徑。 可視化框架研究現(xiàn)狀 由 出的符合模型驅(qū)動架構(gòu)開發(fā) (面向?qū)ο蠼＜夹g(shù)，統(tǒng)一建模語言 (是模型驅(qū)動開發(fā) (一項重要建模技術(shù)，它已經(jīng)日益普遍地應(yīng)用于 工業(yè)系統(tǒng)開發(fā)當(dāng)中。模型驅(qū)動開發(fā) (就是從最初的需求設(shè)計分析到最后的代碼生成。如果將 型轉(zhuǎn)換成形式化驗證的一般語言，那么就能用模型檢驗工具去分析。但是，因為分析結(jié)果繁雜龐大，工程開發(fā)人員往往不能充分利用分析的結(jié)果，也就是，無法解析反例生成文件并將錯誤的原因清晰地標(biāo)注在最初的 上。 第 4 頁 4 這里我們引用由密歇根大學(xué)計算機(jī)科學(xué)軟件工程與網(wǎng)絡(luò)系統(tǒng)實驗室提出的視化框架（如圖 1），它是一種通用的可視化框架，基于模型分析可以在原始的 上得到可視化的分析結(jié)果。利用這個框架，我們能將違背模 型檢驗的反例執(zhí)行路徑清晰地標(biāo)注在最初的 態(tài)圖和順序圖上，這樣可以清楚地將問題描述出來。由于 持 模型驗證工具，工業(yè)上已經(jīng)將 用于各個領(lǐng)域的系統(tǒng)開發(fā)當(dāng)中。 圖 1 視化框架 支持從一般的模型驗證工具生成的模型驅(qū)動可視化輸出分析文件。在 架中，有三大任務(wù)必須完成，第一，由于各種模型驗證工具生成的文件各不相同，我們必須構(gòu)造一個通用的詞法語法解析器來分析各種不同格式的輸出文件，解析器為每個路徑文件生成一個語法樹 (第二，我們必須構(gòu)造一個通用的翻譯器將語法樹轉(zhuǎn)換成一個通用 式的文件， 關(guān)的模型元素，比如狀態(tài)名稱、轉(zhuǎn)換名稱、屬性等。解析器和翻譯器將集成在專門的路徑分析工具中 ;第三，我們必須開發(fā)一個可視 第 5 頁 5 化引擎用來處理以 式呈現(xiàn)的反例文件，并且支持 態(tài)圖和順序圖的生成。這三者結(jié)合起來，就可以實現(xiàn)以 型和模型驗證的反例路徑文件為輸入，以標(biāo)注了反例的狀態(tài)圖和順序圖為輸出的自動化過程。使用者不僅可以通過動畫一步一步運(yùn)行，也可以一下執(zhí)行所有的反例文件，這樣狀態(tài)和問題路徑將通過顏色 的改變呈現(xiàn)出來。 研究的目的和意義 近年來，國內(nèi)逐漸開始重視列控系統(tǒng)規(guī)范的研究。鐵道部 2002 年提出發(fā)展中國列車運(yùn)行控制系統(tǒng)（ 實施引進(jìn)和自主研發(fā)并舉的發(fā)展戰(zhàn)略，在消化吸收國外先進(jìn)技術(shù)的同時，實現(xiàn)引進(jìn)設(shè)備的國產(chǎn)化，發(fā)展 統(tǒng)。技術(shù)規(guī)范是軌道交通系統(tǒng)的核心，為保證我國軌道交通持續(xù)穩(wěn)定發(fā)展，必須在借鑒歐美國家軌道交通系統(tǒng)相關(guān)技術(shù)標(biāo)準(zhǔn)的基礎(chǔ)上，結(jié)合中國軌道交通需要，研究制定 范。 對于列控系統(tǒng)這樣安全苛求系統(tǒng)而言，系統(tǒng)規(guī)范的驗證就顯得尤為重要，主要的有效實用的驗證方法是形式化驗證 。形式化語言雖然具有嚴(yán)格的語法和語義定義，可以準(zhǔn)確地描述系統(tǒng)模型，但所包含的數(shù)學(xué)理論，限制了大多數(shù)設(shè)計人員的學(xué)習(xí)和使用。大多數(shù)的形式化語言和形式化驗證技術(shù)對于設(shè)計人員來說，并不熟悉而且難以理解，因此造成了形式化方法實用方面的困難。在這其中，可理解性起了很重要的作用。這樣就會造成不必要的人力物力浪費(fèi)，為了很好地解決這個問題，本課題旨在開發(fā)一個通用的列車控制系統(tǒng)規(guī)范驗證的反例可視化框架，通過集成一些軟件工具，可以大大地提高效率，是工程開發(fā)人員不必再去糾結(jié)于繁瑣的形式化驗證語言，而且可視化的插件能夠很好地將錯誤快 速地定位在原始的模型圖上，并且將造成反例的路徑通過顏色的改變標(biāo)注出來，這樣可以很好地進(jìn)行追蹤定位。 通過集成反例可視化與 模和驗證工具鏈，實現(xiàn)了列控系統(tǒng)規(guī)范建模、驗證和結(jié)果顯示的自動化。 第 6 頁 6 論文的研究內(nèi)容 第一章 緒論 本章主要介紹了課題研究背景及其意義、發(fā)展現(xiàn)狀、本課題的研究內(nèi)容以及本文的主要研究內(nèi)容。 第二章 臺下列控系統(tǒng)規(guī)范的建模 本章主要介紹了在 臺下 件下的 模和 種建模 方式，并分別給出了簡單的照明燈開關(guān)控制系統(tǒng)和列控站場聯(lián)鎖系統(tǒng)兩個案例模型，作為后續(xù)進(jìn)一步研究的基礎(chǔ)。 第三章 模型檢驗與反例的語法描述 本章主要介紹了模型檢驗的基礎(chǔ)知識，并以此為基礎(chǔ)，對反例模型檢驗實現(xiàn) 言描述。 第四章 反例文件的生成及文件格式的轉(zhuǎn)換 本章主要介紹了可擴(kuò)展標(biāo)記語言（ 具的基礎(chǔ)知識，并借助 具完成對反例生成文件 式的轉(zhuǎn)換。 第五章 析 例文件 本章主要介紹了 析算法的基礎(chǔ)知識，并利用 析 件的 法實現(xiàn)對 式反例文件的解析，同時對 析算法進(jìn)行了初步改進(jìn)。 第六章 臺可視化插件的集成 本章主要展示了可視化插件的界面和功能，并呈現(xiàn)模型最后的可視化效果。 第七章 總結(jié)和展望 本章主要介紹了已經(jīng)完成的工作、存在的問題以及將來研究方向的展望。 第 7 頁 7 2 臺下列控系統(tǒng)規(guī)范的建模 件下的 模 統(tǒng)一建模語言 述 統(tǒng)一建模語言 (是用來對軟件密集系統(tǒng)進(jìn)行可視化建模的一種語言，用 于對軟件進(jìn)行描述、可視化處理、構(gòu)造和建立軟件系統(tǒng)制品的文檔。它記錄了對必須構(gòu)造的系統(tǒng)的決定和理解，可用于對系統(tǒng)的理解、設(shè)計、瀏覽、配置、維護(hù)和信息控制。 用于各種軟件開發(fā)方法、軟件生命周期的各個階段、各種應(yīng)用領(lǐng)域以及各種開發(fā)工具， 一種總結(jié)了以往建模技術(shù)的經(jīng)驗并吸收當(dāng)今優(yōu)秀成果的標(biāo)準(zhǔn)建模方法。 括概念的語義，表示法和說明，提供了靜態(tài)、動態(tài)、系統(tǒng)環(huán)境及組織結(jié)構(gòu)的模型。它可被交互的可視化建模工具所支持，這些工具提供了代碼生成器和報表生成器。 準(zhǔn)并沒有定義一種標(biāo)準(zhǔn)的開發(fā)過程，但它適用于迭代 式的開發(fā)過程。它是為支持大部分現(xiàn)存的面向?qū)ο箝_發(fā)過程而設(shè)計的。 由 3 位杰出的方法論學(xué)家 ( 發(fā)起，在 示法、 法和 法的基礎(chǔ)上，反復(fù)修改而完成的，是非專利的第三代建模和規(guī)約語言。 在開發(fā)階段，說明，可視化，構(gòu)建和書寫一個面向?qū)ο筌浖芗到y(tǒng)的制品的開放方法。 一種用來建模和開發(fā)軟件系統(tǒng)的圖形化語言，主要用于為系統(tǒng)建造模型。它提供了軟件開發(fā)的各個階段的可視化建模支持，包括從需求分析到規(guī)格 書寫，以及系統(tǒng)開發(fā)和建立等。它為面向?qū)ο蟮姆治雠c設(shè)計提供詳細(xì)描述系統(tǒng)結(jié)構(gòu)的方法，為規(guī)范化、可視化、文檔化軟件系統(tǒng)提供了一致的建模語言。目前， 許多領(lǐng)域的軟件開發(fā)中得到應(yīng)用。 持可視化建模，包括動態(tài)和靜態(tài)兩種建模機(jī)制以及多種類型的圖 第 8 頁 8 表，通過使用這些圖表我們可以對系統(tǒng)運(yùn)行過程中各部件及其運(yùn)行模式進(jìn)行詳細(xì)描述。因此它非常適用于以面向?qū)ο蠹夹g(shù)來描述任何類型的系統(tǒng)，而且適用于系統(tǒng)開發(fā)的不同階段，面向?qū)ο蟮姆椒墒褂?供的用例圖、靜態(tài)圖、行為圖、交互圖和實現(xiàn)圖 5 類圖進(jìn)行系統(tǒng)開發(fā)中不同階段的建模。 建模機(jī)制 同所有語言一樣， 語法和語義組成。其中，元模型是 語義，解釋 意思，圖 (表示法 )是 語法。下面將分別介紹這兩方面的內(nèi)容。 (1) 義 語義定義在一個四層建模框架中，它們分別是元元模型層、元模型層、模型層和用戶模型層。 元元模型層是元模型結(jié)構(gòu)的基礎(chǔ)，定義元模型描述語言的模型，它比元模型具有更高的抽象層次，為準(zhǔn)確定義元模型的元素和各種機(jī)制提供最基本的概念和機(jī)制。 元模型是元元模型的實例，定義模型描述語言的模型 。元模型通過把屬性、操作、結(jié)合和通信進(jìn)一步抽象為結(jié)構(gòu)元素、行為元素來表達(dá)模型，并提供表達(dá)系統(tǒng)的機(jī)制 (包 )。 模型是元模型的實例，定義特定信息域描述余姚的模型。模型規(guī)定了對象的屬性、操作以及聚集、結(jié)構(gòu)和通信，保證用戶對象層的語義正確描述。 用戶模型 (用戶數(shù)據(jù) )是模型的實例，描述了一個特定的信息域，它是按照某一領(lǐng)域的域模型組織的。任何軟件系統(tǒng)在用戶看來都是相互通信的具體對象。如果排除面向?qū)ο笳Z言表示的細(xì)節(jié)，這些具體對象構(gòu)成一個對象體系結(jié)構(gòu)，并完成具體的相互通信，其目的是實現(xiàn)軟件系統(tǒng)的功能和性能。如下表 1 所示： 第 9 頁 9 層 描述 例子 元元模型 基本的元素，元建模體系結(jié)構(gòu)的基礎(chǔ) 元類、元屬性、元操作 元模型 基本元素，包括面向?qū)ο蠛兔嫦蚪M件的概念。元元模型的實例。定義說明模型語言。 類、屬性、操作、組件 模型 模型。元模型的實例。定義描述信息領(lǐng)域的語言。 例如：課程、查詢、成績 用戶模型 型的實例。定義特定的信息領(lǐng)域。 例如：數(shù)據(jù)結(jié)構(gòu)等 表 1 四層元模型體系結(jié)構(gòu) (2) 法 概念和模型可以分成以下幾個概念域 :靜態(tài)結(jié)構(gòu)、動態(tài)行為、實現(xiàn)構(gòu)造、模型組織、擴(kuò)展機(jī)制。作為一種建模語言， 定義包括 義和 示法兩個部分： 義描述基于 精確元模型定義 ;號的表示法，為開發(fā)者或開發(fā)工具使用這些圖形符號和文本語法為系統(tǒng)建模提供了標(biāo)準(zhǔn)。 的各種組件和概念之間沒有明顯的劃分界限，但為方便起見，我們用視圖來劃分這些概念和組件。視圖只是表達(dá)系統(tǒng)某一方面特征的 模組件的子集。視圖的劃分帶有一定的隨意性。在最上一層，視圖被劃分成三個視圖域：結(jié) 構(gòu)分類、動態(tài)行為和模型管理。 包括多種具有擴(kuò)展能力的組件，這些擴(kuò)展能力有限但很有用。這些組件包括約束、構(gòu)造型和標(biāo)記值，它們適用于所有的視圖元素。表 2 列出了 第 10 頁 10 的視圖和視圖所包括的圖以及與每種圖有關(guān)的主要概念。 主要的域 描述 圖 主要概念 結(jié)構(gòu) 靜態(tài)視圖 類圖 類、關(guān)聯(lián)、泛化、依賴關(guān)系、實現(xiàn)、接口 用例視圖 用例圖 用例、參與者、關(guān)聯(lián)、擴(kuò)展、包含、泛化 實現(xiàn)視圖 構(gòu)件圖 構(gòu)件、接口、依賴關(guān)系、實現(xiàn) 配置視圖 配置圖 節(jié)點(diǎn)、構(gòu)件、依賴關(guān)系、位置 動態(tài) 狀態(tài)機(jī)視圖 狀態(tài)機(jī)圖 狀態(tài)、事件、轉(zhuǎn)換、動作 活動視圖 活動圖 狀態(tài)、活動、完成轉(zhuǎn)換、分叉、結(jié)合 交互視圖 順序圖 交互、對象、消息、激活 協(xié)作圖 協(xié)作、交互、協(xié)作對象、消息 模型管理 模型管理視圖 類圖 包、子系統(tǒng)、模型 可擴(kuò)展性 所有 所有 約束、版型、標(biāo)記值 表 2 視圖和圖 標(biāo)準(zhǔn)建模語言 圖 (9種圖形 )定義：一是用例圖 ( 二是靜態(tài)圖 (包括類圖、對象圖和包圖 ;三是行為圖 (包括狀態(tài)圖和活動圖 ; 四是交互圖 (包括順序圖、合作圖 ;五是實現(xiàn)圖 (其中構(gòu)件圖描述代碼部件的物理結(jié)構(gòu)及各部件之間的依賴關(guān)系。多個視圖共存于一個模型中，它們的元素之間有很多關(guān)系，其中一些關(guān)系如下表 3 所示。 第 11 頁 11 元素 元素 關(guān)系 類 擁有 狀態(tài)機(jī) 操作 交互 實現(xiàn) 用例 合作 實現(xiàn) 用例 交互實例 樣本場景 構(gòu)件實例 節(jié)點(diǎn)實例 位置 動作 操作 調(diào)用 動作 信號 發(fā)送 表 3 不同視圖元素之間的部分關(guān)系 應(yīng) 用 計系統(tǒng)時，首先應(yīng)建立系統(tǒng)的邏輯模型，然后建立相應(yīng)的物理模型。 建立系統(tǒng)邏輯模型的過程大致分為三步 :第一步用用例圖描述系統(tǒng)需求 ;第二步根據(jù)系統(tǒng)需求建立系統(tǒng)的靜態(tài)模型，包括類圖、對象圖和包圖。類圖描述系統(tǒng)中類的靜態(tài)結(jié)構(gòu)對象圖是類圖的實例包圖由包或類組成，表示包與包之間的關(guān)系 ;第三步是描述系統(tǒng)的行為，主要用狀態(tài)圖和順序圖。狀態(tài)圖描述類的對象所有可能的狀態(tài)以及事件發(fā)生時狀態(tài)的轉(zhuǎn)移條件。順序圖顯示對象之間的動態(tài)合作關(guān)系，它強(qiáng)調(diào)對象之間消息發(fā)送的順序，同時顯示對象之間的交互。 采用 析和設(shè)計系統(tǒng)，將復(fù)雜 的系統(tǒng)用簡單明了的可視化圖形表示出來，對整個系統(tǒng)軟件的開發(fā)提供靈活、一致、易讀的表達(dá)，不僅可以解決系統(tǒng)軟件開發(fā)中眾多領(lǐng)域人員之間難以互相交流理解的難題，為系統(tǒng)的分析、設(shè)計、維護(hù)及擴(kuò)展提供了有利的條件，還可提高系統(tǒng)的可重用性和可維護(hù)性，具有廣泛的應(yīng)用前景。 臺及 件簡介 (1) 述 第 12 頁 12 一個開放源代碼的、基于 可擴(kuò)展開發(fā)平臺。就其本身而言，它只是一個框架和一組服務(wù)，用于通過 插件 組件構(gòu)建開發(fā)環(huán)境。幸運(yùn)的是，帶了一個標(biāo)準(zhǔn)的插件集，包括 發(fā)工具（ 雖然大多數(shù)用戶很樂于將 作 使用，但 目標(biāo)不僅限于此。 包括插件開發(fā)環(huán)境（ 這個組件主要針對希望擴(kuò)展 軟件開發(fā)人員，因為它允許他們構(gòu)建與 境無縫集成的工具。由于 的每樣?xùn)|西都是插件，對于給 供插件，以及給用戶提供一致和統(tǒng)一的集成開發(fā)環(huán)境而言，所有工具開發(fā)人員都具有同等的發(fā)揮場所。 件開發(fā)者包）是 生產(chǎn)的組件合并，它們可以一次下載。這些部分在一起提供了一個具有豐富特性的開發(fā)環(huán)境，允許開發(fā)者有效地建造可以無縫集成到 三方軟件 組合而成。目生產(chǎn)的軟件以 布，第三方組件有各自自身的許可協(xié)議。 (2) 件簡介 一個基于 臺 模工具。遵從 持由 定的 準(zhǔn)和 準(zhǔn)、 新的代碼生成器等、支持 發(fā)、嵌套 持等。 第 13 頁 13 模示例 (1) 簡單的照明燈開關(guān)控制系統(tǒng) 照明燈控制系統(tǒng)由人員、照明燈、開關(guān)三部分構(gòu)成，利用 義它們?yōu)楦髯缘念悾渲腥藛T類包括的屬性 有姓名 +別 +;照明燈類包括的屬性有序號 +強(qiáng)度 +作有 ;開關(guān)類包括的屬性有狀態(tài) +作有 。在件里得到如下圖 2. 圖 2 照明燈控制系統(tǒng)類圖 第 14 頁 14 照明燈包括三個狀態(tài)：照明、熄滅、損壞。這三者的關(guān)系可以用圖 3 來表示 圖 3 照明控制系統(tǒng)的狀態(tài)圖 (2) 車控制系統(tǒng) 列控系統(tǒng)包括地面設(shè)備和 車載設(shè)備。地面設(shè)備有無線閉塞中心(列控中心 ( 2000(列軌道電路、應(yīng)答器 (含 R 通信接口設(shè)備等組成 ;車載設(shè)備由車載安全計算機(jī) ( R 無線通信單元 (人機(jī)界面 (列車接口單元 (組成。列控系統(tǒng)模型庫的類見表 4，當(dāng)然這些類還具備一些約束條件，這里不進(jìn)行深入討論 列控系統(tǒng)規(guī)范管理提取的術(shù)語 模型庫中的類 司法記錄器 機(jī)界面 機(jī) 駛臺 第 15 頁 15 天線 載安全計算機(jī) 速模塊 車 答器轉(zhuǎn)換模塊 道電路信息接收單元 R R 聯(lián)鎖 答器 道電路 線閉塞中心 時限速服務(wù)器 度中心 面電子單元 車控制中心 表 4 列控系統(tǒng)模型庫的類 這里從靜態(tài)角度表示 3 級列控 系統(tǒng)，首先，提取了與模式轉(zhuǎn)換有關(guān)的 6 個類，分別為： 機(jī)）、 機(jī)交互界面）、 線閉塞中心）、 答器）、 車）、 載設(shè)備）。然后，確定模式轉(zhuǎn)換過程中每個類體現(xiàn)出的屬性及操作，從列控系統(tǒng)類圖模型庫中直接提取。例如 在模式轉(zhuǎn)換過程中體現(xiàn)出工作狀態(tài)的變換，并且有刪除列出數(shù)據(jù)、檢查調(diào)車報告等操作，在模型庫中直接提取屬性 作狀態(tài)）、操作 刪除列車數(shù)據(jù)）等等。最后，根據(jù)模式轉(zhuǎn)換 第 16 頁 16 的具 體過程，建立出模式轉(zhuǎn)換過程中各個類之間的關(guān)聯(lián)關(guān)系，例如 與是一對一的關(guān)聯(lián)等等。在 件里得到類圖如下圖 4. 圖 4 列車控制系統(tǒng)部分類圖 對于列控系統(tǒng)規(guī)范模型中常規(guī)狀態(tài)圖的建立，首先應(yīng)根據(jù)系統(tǒng)具體的工作過程確定類圖中每個類的狀態(tài)，然后再由規(guī)范中對該工作過程的具體描述，確定類的各狀態(tài)相互轉(zhuǎn)化的條件。首先，在 圖中，主要對載設(shè)備類）、 進(jìn)行狀態(tài)圖的建模，其中對車載設(shè)備 9 種工作模式的狀態(tài)轉(zhuǎn)移進(jìn)行建模是狀態(tài)圖建模的重點(diǎn)。因此針對前述類 圖種涉及的各個類，從列控系統(tǒng)狀態(tài)圖模型庫種，提取出和模式轉(zhuǎn)換過程相關(guān)的各個類的狀態(tài)。例如 的 態(tài)， 的 9 種工作模式狀態(tài)等等。然后，根據(jù)規(guī)范所描述的模式轉(zhuǎn)換的過程，建立出每個類的各狀態(tài)之間的遷移關(guān)系。例如， 在模式轉(zhuǎn)換過程中的工作過程為： 知司機(jī)車載設(shè)備準(zhǔn)備進(jìn)入 導(dǎo)）模式，然后司機(jī)確認(rèn)并按壓按鈕選擇。據(jù)此建立狀態(tài)遷移條件，構(gòu)成完整的狀態(tài)遷移圖。如圖 5 所示。 第 17 頁 17 圖 5 的 態(tài)圖 其他 臺 輯插件 (1) 一款開源的 模工具 ， 支持所有 標(biāo)準(zhǔn)圖 第 18 頁 18 形 .。 它可以運(yùn)行在任何 臺上 ， 并且支持 10 種語言 (地區(qū)語言而不是編程語言 )。 前的最新版本是 支持 多種操作系統(tǒng) 。 圖形的顯示方式有多種可選 (默認(rèn)有 C+ 三種 )。 可生成代碼 、 還具備對齊 ， 等間距 ， 調(diào)整層次和保存圖片等功能 。 能不算豐富 ， 界面也有待加強(qiáng) ， 但作圖操作卻是相當(dāng)?shù)姆奖?。 (2) 一個插件，是一種先進(jìn)的還簡單的 圖的工具，主要學(xué)生開發(fā)使用。它是 輯器，因此可以很容易地從一個圖生成 碼。它有很好的可擴(kuò)展性。 就是說它支持軟件工程和逆向工程技術(shù)。您可以使用它創(chuàng)建一個圖，或生成代碼。它發(fā)展的目標(biāo)是教學(xué)方面，重點(diǎn)放在學(xué)生的設(shè)計。但它已被證明是一個功能強(qiáng)大和靈活的 工具，可以很容易地在任何環(huán)境中提供支持。所有關(guān)系插件擴(kuò)展都基于它。簡單的編輯功能界面。右鍵單擊編 第 19 頁 19 輯器便彈出了靈活的菜單，其中包括的功能，如重構(gòu)和快速修復(fù)。它支持的導(dǎo)出格式包括 述 一個開放源代碼的模型驅(qū)動應(yīng)用程序開發(fā)框架。它可以基于 經(jīng)過注釋的 指定的模型，創(chuàng)建 碼，實現(xiàn)圖形化的數(shù)據(jù)編輯、操縱、讀取和序列化。通過采用 數(shù)據(jù)交換（ 式描述的模型規(guī)范， 供了工具和運(yùn)行時支持，從而為模型生成一組 ；核心 架包括用于描述模型的元模型 (并為模型提供運(yùn)行時支持，包括 更改通知、采用缺省 列化的保存支持以及用于對 象進(jìn)行常規(guī)操作的非常高效的反射應(yīng)用程序編程接口（ 列控聯(lián)鎖系統(tǒng)的建模 為了保證行車安全，通過技術(shù)方法，使進(jìn)路、進(jìn)路道岔和信號機(jī)之間按一定程序、一定條件建立起的既相互聯(lián)系，而又制約關(guān)系，這種制約關(guān)系即聯(lián)鎖。信號機(jī)、進(jìn)路和進(jìn)路上的道岔相互制約的要求： 1、 進(jìn)路上的有關(guān)道岔