基于STeC的列控系統(tǒng)的建模與驗(yàn)證.pdf

1、隨著嵌入式、計(jì)算機(jī)和網(wǎng)絡(luò)技術(shù)快速發(fā)展，人類對(duì)于相關(guān)產(chǎn)品的依賴逐漸增強(qiáng)。在此需求下，信息物理融合系統(tǒng)(CPS, Cyber P hysical Systems)應(yīng)運(yùn)而生，各國(guó)學(xué)術(shù)界和商業(yè)界都引起高度重視。CP S的典型應(yīng)用包括：智能交通、生物醫(yī)療以及自主運(yùn)算等領(lǐng)域。CP S應(yīng)用對(duì)安全性的要求很高，保證智能體的時(shí)間、空間一致性是其研究領(lǐng)域的一大熱點(diǎn)。針對(duì)該類系統(tǒng)的時(shí)空一致性，運(yùn)用實(shí)時(shí)系統(tǒng)規(guī)范語(yǔ)言STeC進(jìn)行建模，并在系統(tǒng)設(shè)計(jì)的需求層面驗(yàn)證系

2、統(tǒng)的正確性。
　　論文對(duì)列車晚點(diǎn)問(wèn)題進(jìn)行深入研究，針對(duì)不同晚點(diǎn)類型問(wèn)題研究相應(yīng)的不停車超車策略。主要研究工作包括以下幾點(diǎn)：
　　1，針對(duì)智能交通領(lǐng)域中的兩種典型晚點(diǎn)類型，設(shè)計(jì)不同的不停車超車策略，代入實(shí)例數(shù)據(jù)測(cè)試驗(yàn)證策略的正確性和實(shí)用性。
　　2，運(yùn)用ST eC語(yǔ)言對(duì)CPS(列控系統(tǒng))建模，通過(guò)形式化描述兩種晚點(diǎn)類型的不停車超車策略，使用STeC工具驗(yàn)證其描述的邏輯正確性以及時(shí)空一致性。
　　3，針對(duì)不同實(shí)例，通