基于UML和UPPAAL的FAO系統(tǒng)典型運(yùn)營(yíng)場(chǎng)景的建模與驗(yàn)證.pdf

1、全自動(dòng)駕駛(Fully Automatic Operation，F(xiàn)AO)系統(tǒng)是一種解決高速度、高密度城市軌道交通系統(tǒng)的安全、節(jié)能、高效、靈活運(yùn)輸?shù)葐?wèn)題的重要手段，其核心是將列車(chē)駕駛員、調(diào)度員執(zhí)行的工作，完全由自動(dòng)化、智能化的系統(tǒng)所替代，是未來(lái)城市軌道交通發(fā)展方向之一。針對(duì)FAO系統(tǒng)核心部分高安全苛求的列控系統(tǒng)而言，在運(yùn)營(yíng)場(chǎng)景設(shè)計(jì)開(kāi)始階段，采用形式化方法分析運(yùn)營(yíng)場(chǎng)景的需求規(guī)范并驗(yàn)證其實(shí)時(shí)性，排除功能和性能隱患，對(duì)保障FAO系統(tǒng)安全高效運(yùn)行

2、具有非常重要的意義。
　　本文綜合分析了形式化方法在列控系統(tǒng)運(yùn)營(yíng)場(chǎng)景的應(yīng)用狀況，通過(guò)比較單獨(dú)采用UML時(shí)序圖或基于時(shí)間自動(dòng)機(jī)理論和模型檢測(cè)工具UPPAAL的優(yōu)缺點(diǎn)，形成了基于UML和UPPAAL的建模與驗(yàn)證流程，為FAO系統(tǒng)運(yùn)營(yíng)場(chǎng)景的形式化分析研究提供了重要參考和指導(dǎo)。主要內(nèi)容包括：⑴總結(jié)了FAO系統(tǒng)有別于現(xiàn)有CBTC系統(tǒng)三個(gè)具有代表性的典型運(yùn)營(yíng)場(chǎng)景:建立和取消保護(hù)區(qū)、自動(dòng)折返、出段作業(yè)，并從信號(hào)系統(tǒng)角度，詳細(xì)給出了場(chǎng)景的實(shí)現(xiàn)流程

3、、信息交互的數(shù)據(jù)流、以及功能和性能需求。⑵采用規(guī)范描述的方法對(duì)三個(gè)典型運(yùn)營(yíng)場(chǎng)景的功能和性能需求規(guī)范進(jìn)行整理和分類(lèi)，分別從術(shù)語(yǔ)、功能、通信、環(huán)境、特性等方面提取實(shí)時(shí)動(dòng)態(tài)行為，并整理出時(shí)序圖模型元素對(duì)應(yīng)圖表，實(shí)現(xiàn)了需求規(guī)范與模型元素的跟蹤管理。⑶構(gòu)建三個(gè)典型運(yùn)營(yíng)場(chǎng)景的時(shí)序圖模型，根據(jù)時(shí)序圖模型元素到時(shí)間自動(dòng)機(jī)的模型元素語(yǔ)義上的對(duì)應(yīng)關(guān)系，分別進(jìn)行了時(shí)序圖模型到時(shí)間自動(dòng)機(jī)模型轉(zhuǎn)換，并得到時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)模型。由于人工模型轉(zhuǎn)換的繁瑣，本文開(kāi)發(fā)了軟件