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

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

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

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