本文關(guān)鍵詞：基于模擬關(guān)系的精化檢測(cè)方法

  更多相關(guān)文章： 精化檢測(cè) 模擬 failures divergence 時(shí)間自動(dòng)機(jī)

【摘要】：精化檢測(cè)是一種重要的形式化驗(yàn)證方法,將系統(tǒng)實(shí)現(xiàn)和性質(zhì)規(guī)約用相同的形式化語(yǔ)言進(jìn)行建模,如能證明兩者間存在某種精化關(guān)系,且該關(guān)系能夠維持性質(zhì),可得出系統(tǒng)實(shí)現(xiàn)滿足性質(zhì)規(guī)約.為驗(yàn)證不同類型的系統(tǒng)性質(zhì),traces,stable failures和failures-divergence精化檢測(cè)方法已被提出.精化檢測(cè)算法依賴于子集構(gòu)造,因而其面臨狀態(tài)空間爆炸問(wèn)題.近年來(lái),已有學(xué)者針對(duì)NFA語(yǔ)言包含問(wèn)題提出了基于模擬關(guān)系的狀態(tài)空間消減方法,極大地提高了算法的性能,且該方法能夠直接用于traces精化檢測(cè).在此基礎(chǔ)上,提出了基于模擬關(guān)系的stable failures和failuresdivergence精化檢測(cè)方法.此外,還將精化檢測(cè)擴(kuò)展到了時(shí)間系統(tǒng)的驗(yàn)證中,提出了基于模擬關(guān)系的時(shí)間自動(dòng)機(jī)traces精化檢測(cè)方法.實(shí)驗(yàn)結(jié)果表明,基于模擬關(guān)系的算法效率有很大提高.
【作者單位】： 浙江工業(yè)大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;School
【關(guān)鍵詞】： 精化檢測(cè) 模擬 failures divergence 時(shí)間自動(dòng)機(jī)
【基金】：國(guó)家自然科學(xué)基金(61103044,U1509214) 浙江省自然科學(xué)基金(LQ15E050006,LY16F020035)~~
【分類號(hào)】：TP301.1
【正文快照】： 精化(refinement)方法已在理論研究和工程實(shí)踐中被廣泛應(yīng)用,一般過(guò)程是通過(guò)對(duì)抽象模型的逐步求精得到具體的系統(tǒng)實(shí)現(xiàn),系統(tǒng)實(shí)現(xiàn)和抽象模型間即存在精化關(guān)系.兩者均能滿足某種性質(zhì),使得系統(tǒng)實(shí)現(xiàn)在代替抽象模型時(shí)能夠保持一致性和正確性.在形式化驗(yàn)證方面,利用精化關(guān)系的驗(yàn)證(以

【相似文獻(xiàn)】

中國(guó)期刊全文數(shù)據(jù)庫(kù) 前6條

1 祁方民;;Petri網(wǎng)結(jié)點(diǎn)精化及其應(yīng)用[J];計(jì)算機(jī)與現(xiàn)代化;2014年07期

2 王云峰 ,龐軍 ,查鳴 ,楊朝暉 ,鄭國(guó)梁;精化演算支撐工具的分析[J];計(jì)算機(jī)應(yīng)用與軟件;2002年02期

3 劉瑜,張世琨,鄔倫,葉燕林;地理信息系統(tǒng)中的設(shè)計(jì)模式——以過(guò)濾和精化為例[J];北京大學(xué)學(xué)報(bào)(自然科學(xué)版);2001年06期

4 熊建;陳曉克;;基于Wiki技術(shù)可持續(xù)精化精品課教學(xué)平臺(tái)[J];福建電腦;2010年12期

5 楊朝暉;王云峰;鄭國(guó)梁;;精化演算支撐工具PRT的研究[J];計(jì)算機(jī)科學(xué);2000年03期

6 ;[J];;年期

中國(guó)重要會(huì)議論文全文數(shù)據(jù)庫(kù) 前5條

1 周鑫;;面對(duì)新形勢(shì)、樹(shù)立新觀念、迎接新挑戰(zhàn)——談企業(yè)職工面對(duì)“精化分立、分業(yè)經(jīng)營(yíng)”新形勢(shì)的感想[A];陜西省體制改革研究會(huì)2006-2007優(yōu)秀論文集[C];2007年

2 高陽(yáng);王敏中;;拉伸矩形梁的精化理論[A];北京力學(xué)會(huì)第11屆學(xué)術(shù)年會(huì)論文摘要集[C];2005年

3 高陽(yáng);王敏中;;橫觀各項(xiàng)同性壓電矩形直梁的精化理論[A];中國(guó)力學(xué)學(xué)會(huì)學(xué)術(shù)大會(huì)'2005論文摘要集（下）[C];2005年

4 趙紅麗;范景輝;郭小方;劉廣;陳建平;;CR輔助的基線參數(shù)精化方法研究[A];第十七屆中國(guó)遙感大會(huì)摘要集[C];2010年

5 江東;王慶賓;王凱;;重力場(chǎng)精化的空間插值方法研究[A];中國(guó)測(cè)繪學(xué)會(huì)2010年學(xué)術(shù)年會(huì)論文集[C];2010年

中國(guó)重要報(bào)紙全文數(shù)據(jù)庫(kù) 前10條

1 羅平華;彩虹精化氣霧漆龍頭今日掛牌[N];證券時(shí)報(bào);2008年

2 證券時(shí)報(bào)記者 羅平華;彩虹精化出口收入逆勢(shì)增長(zhǎng)三成[N];證券時(shí)報(bào);2009年

3 證券時(shí)報(bào)記者 向南;彩虹精化 涉足室內(nèi)環(huán)保業(yè)務(wù)[N];證券時(shí)報(bào);2010年

4 記者 翟敏;彩虹精化上半年業(yè)績(jī)平平 管理層就“巨額訂單”事件致歉[N];上海證券報(bào);2011年

5 記者 王健杰;彩虹精化營(yíng)收內(nèi)降外增[N];北京商報(bào);2009年

6 中國(guó)空空導(dǎo)彈研究院 綜合管理處;精化軍品能力 優(yōu)化民品結(jié)構(gòu)[N];中國(guó)航空?qǐng)?bào);2004年

7 本報(bào)通訊員 周善良 記者 李雨農(nóng);精化分立 一所多制[N];中國(guó)航空?qǐng)?bào);2002年

8 武連寅邋蔡軍;淮化精化再次入選國(guó)家高新企業(yè)[N];中國(guó)化工報(bào);2007年

9 記者 孫燕飚　劉瓊;萬(wàn)潤(rùn)精化再上會(huì) 日德企業(yè)“鎖喉”難改觀[N];第一財(cái)經(jīng)日?qǐng)?bào);2011年

10 記者 況玉清;彩虹精化虛假陳述案下月開(kāi)庭[N];北京商報(bào);2012年

中國(guó)博士學(xué)位論文全文數(shù)據(jù)庫(kù) 前4條

1 陳桂芝;解大規(guī)模非對(duì)稱矩陣特征問(wèn)題的一些精化算法[D];大連理工大學(xué);2000年

2 梁紅瑾;并發(fā)程序精化驗(yàn)證及其應(yīng)用[D];中國(guó)科學(xué)技術(shù)大學(xué);2014年

3 牛大田;計(jì)算大規(guī)模矩陣部分奇異值分解的精化Lanczos型算法[D];大連理工大學(xué);2003年

4 梁坤;高靈敏度GPS接收技術(shù)中幾個(gè)關(guān)鍵問(wèn)題的研究[D];中國(guó)科學(xué)院研究生院（國(guó)家天文臺(tái)）;2008年

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

1 錢潔;軌旁系統(tǒng)的形式化建模精化與驗(yàn)證[D];華東師范大學(xué);2015年

2 劉婷婷;雙層梁的精化理論[D];遼寧科技大學(xué);2015年

3 劉穩(wěn);隱式重啟和精化的全局Lanczos方法與塊Lanczos方法[D];南京航空航天大學(xué);2014年

4 付亞軍;面向多主體的基于政策的運(yùn)行機(jī)制研究[D];湖南大學(xué);2009年

5 吳鋼;解大規(guī)模非對(duì)稱矩陣特征問(wèn)題Lanczos方法的兩種精化版本[D];大連理工大學(xué);2001年

，

本文編號(hào)：985370