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

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

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

【相似文獻(xiàn)】

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

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

2 ;[J];;年期

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

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

，

本文編號：1187145