本文關(guān)鍵詞：基于帶數(shù)據(jù)約束實時系統(tǒng)的互模擬檢測方法

  更多相關(guān)文章： 實時系統(tǒng) 接口自動機 Z語言 時間自動機 互模擬檢測

【摘要】：帶數(shù)據(jù)約束的實時系統(tǒng)是指一種既帶有時間約束又帶有數(shù)據(jù)變量約束的計算系統(tǒng),其廣泛存在于航空航天、工業(yè)控制、國防等安全攸關(guān)系統(tǒng),并發(fā)揮著至關(guān)重要的作用。針對這類系統(tǒng)的形式化建模與驗證是確保其正確性和可靠性的重要途徑。文中首先研究了組合接口自動機、Z語言、時間自動機的形式規(guī)范—CT-ZIA,其能同時描述帶數(shù)據(jù)約束的實時系統(tǒng)的時序行為性質(zhì)和數(shù)據(jù)結(jié)構(gòu)性質(zhì);其次,為了研究該規(guī)范上的互模擬形式化驗證,給出了CT-ZIA上的互模擬關(guān)系定義;然后,為了互模擬算法的可判定性,對CT-ZIA中的時鐘進行等價劃分,提出了有限論域CT-ZIA的定義;最后,基于有限論域CT-ZIA模型,給出了其上互模擬檢測算法,并說明其正確性。
【作者單位】： 南京航空航天大學(xué)計算機科學(xué)與技術(shù)學(xué)院;
【基金】：航空科學(xué)基金(20128052064) 中央高�；究蒲袠I(yè)務(wù)費專項資金(NZ2013306) 國家“973”重點基礎(chǔ)研究發(fā)展計劃項目(2014CB744903)
【分類號】：TP306;TP301
【正文快照】： 0引言帶數(shù)據(jù)約束的實時系統(tǒng)[1]是指一種既帶有時間約束,又帶有數(shù)據(jù)變量約束的計算系統(tǒng)。飛行控制、核反應(yīng)堆控制以及鐵路調(diào)度控制等計算機控制系統(tǒng)都屬于帶數(shù)據(jù)約束的實時系統(tǒng)。這些系統(tǒng)中許多動作的完成都與時間相關(guān),即要滿足一定的時間限制,如某個動作要在一秒鐘內(nèi)完成;同時

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前2條

1 鈕俊;曾國蓀;王偉;;綠色評價模型的互模擬等價及邏輯保持[J];計算機學(xué)報;2013年05期

2 ;[J];;年期

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前1條

1 鄧輝;基于可能性測度的計算樹邏輯與可能性互模擬[D];陜西師范大學(xué);2013年

，

本文編號：1187145