ATS系統(tǒng)內(nèi)部通信協(xié)議的設(shè)計(jì)及形式化驗(yàn)證.pdf

1、在CBTC（基于通信的列車(chē)控制）系統(tǒng)中，ATS（自動(dòng)列車(chē)監(jiān)控）子系統(tǒng)實(shí)時(shí)監(jiān)控列車(chē)運(yùn)行線路及列車(chē)運(yùn)行狀況，為調(diào)度人員提供實(shí)際運(yùn)行線路上的大量現(xiàn)場(chǎng)信息。ATS系統(tǒng)設(shè)備間的數(shù)據(jù)交互都是通過(guò)通信協(xié)議來(lái)完成，通信協(xié)議將系統(tǒng)內(nèi)的設(shè)備聯(lián)系起來(lái)形成一個(gè)有機(jī)的整體，從而使系統(tǒng)中各子單元共同協(xié)作完成特定的功能，通信協(xié)議質(zhì)量的好壞直接關(guān)系到系統(tǒng)功能的完成和系統(tǒng)性能的優(yōu)劣。傳統(tǒng)的通信協(xié)議驗(yàn)證大多是通過(guò)大量的實(shí)踐來(lái)檢驗(yàn)協(xié)議設(shè)計(jì)的正確性，這樣的驗(yàn)證方法無(wú)法從理論的

2、角度來(lái)證明通信協(xié)議設(shè)計(jì)的正確性，同時(shí)也很難發(fā)現(xiàn)一些隱藏很深的設(shè)計(jì)漏洞。所以應(yīng)用形式化的驗(yàn)證方法對(duì)協(xié)議的設(shè)計(jì)模型進(jìn)行驗(yàn)證是非常有意義的。本文對(duì)實(shí)驗(yàn)室自主研發(fā)的ATS系統(tǒng)的內(nèi)部通信協(xié)議進(jìn)行了設(shè)計(jì)和形式化的驗(yàn)證工作，并給出了驗(yàn)證結(jié)果分析。主要研究?jī)?nèi)容如下： ⑴介紹了形式化的驗(yàn)證方法，形式化驗(yàn)證方法的意義在于它能夠證明待驗(yàn)證系統(tǒng)模型設(shè)計(jì)的正確性，它會(huì)遍歷系統(tǒng)內(nèi)所有的狀態(tài)遷移路徑來(lái)驗(yàn)證模式是否滿足指定的性質(zhì)。接下來(lái)闡述了符號(hào)模型檢驗(yàn)方法的

3、原理及其支持工具SMV，具體說(shuō)明了SMV的基本工作原理和語(yǔ)法，同時(shí)指出了在使用SMV的過(guò)程中發(fā)現(xiàn)的一些問(wèn)題。 ⑵依據(jù)需求對(duì)內(nèi)部通信協(xié)議進(jìn)行了設(shè)計(jì)。先簡(jiǎn)要介紹了設(shè)計(jì)工具Rational Rose，接著闡述了ATS系統(tǒng)內(nèi)部通信協(xié)議的需求以及相應(yīng)的設(shè)計(jì)策略，簡(jiǎn)單來(lái)說(shuō)內(nèi)部通信協(xié)議的需求即通信協(xié)議要滿足ATS系統(tǒng)對(duì)數(shù)據(jù)傳輸?shù)男枨?，接著針?duì)需求進(jìn)行了內(nèi)部通信協(xié)議的架構(gòu)設(shè)計(jì)和模塊劃分工作，最后以UML類圖、序列圖和活動(dòng)圖的方式對(duì)內(nèi)部通信協(xié)議的