基于SysML的CTCS-3級列控系統(tǒng)建模和分析.pdf

1、列控系統(tǒng)需求工程是列控系統(tǒng)開發(fā)的起點和基礎(chǔ)。對需求規(guī)范進(jìn)行建模分析是提高規(guī)范質(zhì)量、降低系統(tǒng)開發(fā)風(fēng)險和成本的有效手段。CTCS-3級列控系統(tǒng)的研究采用了“標(biāo)準(zhǔn)先行”的國際通用方法，即先制訂系統(tǒng)的標(biāo)準(zhǔn)規(guī)范，以便于指導(dǎo)系統(tǒng)后續(xù)的研發(fā)。而需求規(guī)范的制定多數(shù)是依靠領(lǐng)域?qū)＜业慕?jīng)驗，自然語言以及人為因素不可避免地存在某些漏洞或表意不清，這為系統(tǒng)的設(shè)計與開發(fā)帶來了不利影響。因此對列控系統(tǒng)需求規(guī)范進(jìn)行形式化建模與驗證顯得十分必要。
　　本文以CTC

2、S-3級列控系統(tǒng)需求規(guī)范為主要研究對象，并對其建模與形式化驗證分析方法展開研究。主要內(nèi)容包括：⑴著眼于研究一種有效的列控系統(tǒng)規(guī)范建模分析方法，該方法從系統(tǒng)需求、靜態(tài)結(jié)構(gòu)以及動態(tài)行為三方面描述了列控系統(tǒng)的主要特征，并對SysML建模語言進(jìn)行了擴展，設(shè)計了SysML概要文件，從而增強了建模語言的刻畫能力。⑵從定性和定量分析兩個方面提出了兩種需求規(guī)范的形式化分析方法。其中，基于屬性的需求分析方法是對規(guī)范模型進(jìn)行定性分析，從系統(tǒng)規(guī)范的一致性、系

3、統(tǒng)的可實現(xiàn)性、設(shè)計意圖以及相關(guān)性質(zhì)的確認(rèn)方面進(jìn)行了分析驗證。而基于MITLFG的需求分析方法是對規(guī)范中帶有時間約束的需求進(jìn)行定量刻畫，兩者之間起到了互補的作用。⑶為了更好地運用列控系統(tǒng)規(guī)范的建模與分析方法，開發(fā)了一款軟件:ReqTool。該軟件實質(zhì)是一個工具集，它以Eclipse平臺為基礎(chǔ)，通過擴展Eclipse接口與RATSY、Topcased進(jìn)行集成，實現(xiàn)模型提取、模型構(gòu)建以及模型分析三大主要功能，大大地提高了建模與驗證的效率，較好