[發(fā)明專利]基于加權(quán)下推系統(tǒng)的中斷驗(yàn)證方法

有效

• 申請(qǐng)?zhí)枺?/td>: 201710139115.2
• 申請(qǐng)日: 2017-03-09
• 公開（公告）號(hào): CN106940659B
• 公開（公告）日: 2018-09-18
• 發(fā)明（設(shè)計(jì)）人: 黃滟鴻;郭欣;史建琦;何積豐;李昂;方徽星
• 申請(qǐng)（專利權(quán)）人: 華東師范大學(xué);上海豐蕾信息科技有限公司
• 主分類號(hào): G06F9/48
• 分類號(hào): G06F9/48
• 代理公司: 北京辰權(quán)知識(shí)產(chǎn)權(quán)代理有限公司 11619
• 代理人: 郎志濤

1.一種基于加權(quán)下推系統(tǒng)的中斷驗(yàn)證方法，其特征在于，包括：

步驟1：提取需要驗(yàn)證的不同任務(wù)的程序的目標(biāo)代碼，將其轉(zhuǎn)換為加權(quán)下推系統(tǒng)；

步驟2：根據(jù)所述加權(quán)下推系統(tǒng)的可達(dá)性算法以及問題的需求計(jì)算出Pre加權(quán)自動(dòng)機(jī)或Post加權(quán)自動(dòng)機(jī)，Pre加權(quán)自動(dòng)機(jī)或Post加權(quán)自動(dòng)機(jī)可接受的語(yǔ)言作為可達(dá)格局；

步驟3：遍歷步驟2獲得的所有的可達(dá)格局，在遍歷的過程中，判斷當(dāng)前格局信息是否滿足驗(yàn)證需求性質(zhì)，如果不滿足，判讀錯(cuò)誤類型，跳轉(zhuǎn)至步驟4，若遍歷完所有格局均滿足驗(yàn)證需求性質(zhì)，返回正確，則跳轉(zhuǎn)至步驟5；

步驟4：根據(jù)當(dāng)前格局進(jìn)行回溯，找出不滿足所需驗(yàn)證性質(zhì)的路徑，給出該程序不滿足驗(yàn)證需求性質(zhì)的結(jié)果，并且給出反例路徑，算法結(jié)束；

步驟5：給出所述程序滿足驗(yàn)證需求性質(zhì)的結(jié)果。

2.根據(jù)權(quán)利要求1所述的基于加權(quán)下推系統(tǒng)的中斷驗(yàn)證方法，其特征在于，所述加權(quán)下推系統(tǒng)包括三元組W＝(P,S,f)，其中P＝(P,Γ,Δ)為下推系統(tǒng)，為有界冪等半環(huán)，f：Δ→D是將下推規(guī)則映射到權(quán)重；

所述下推系統(tǒng)P＝(P,Γ,Δ)中，P是有限的控制位置集合，Γ是有限的棧字符集合，Δ是有限的遷移規(guī)則的集合，規(guī)則的形式為：<p,v→q,w>，其中，(p,v,q,w)∈Δ；

所述有界冪等半環(huán)中，D為權(quán)重集，0，1∈D，為D上的二元操作，其中運(yùn)算符定義為取最小值，運(yùn)算符定義為算數(shù)加法：

1)為以0為中性元的可交換的幺半群，并且是冪等的；

2)為以1為中性元的幺半群；

3)對(duì)可分配，即對(duì)于所有a,b,c∈D，有

4)0為操作的零化子，即對(duì)于所有a∈D，

5)D上偏序關(guān)系＜定義為當(dāng)且僅當(dāng)在此關(guān)系下不存在無窮降鏈。

3.根據(jù)權(quán)利要求1所述的基于加權(quán)下推系統(tǒng)的中斷驗(yàn)證方法，其特征在于，所述可達(dá)性包括給定一個(gè)初始格局和一個(gè)目標(biāo)格局，判斷能否從初始格局出發(fā)，通過有限步的格局遷移到達(dá)目標(biāo)格局。

4.根據(jù)權(quán)利要求1所述的基于加權(quán)下推系統(tǒng)的中斷驗(yàn)證方法，其特征在于,所述Pre加權(quán)自動(dòng)機(jī)為接受所有從當(dāng)前格局可以到達(dá)的所有pre可達(dá)格局的自動(dòng)機(jī)，所有pre可達(dá)格局為所有可以通過有限步的格局遷移到達(dá)該格局的格局集合。

5.根據(jù)權(quán)利要求1所述的基于加權(quán)下推系統(tǒng)的中斷驗(yàn)證方法，其特征在于,所述Post加權(quán)自動(dòng)機(jī)為接受所有從當(dāng)前格局可以到達(dá)的所有post可達(dá)格局的自動(dòng)機(jī)，所有post可達(dá)格局為該格局通過有限步的格局遷移可以到達(dá)的格局集合。

6.根據(jù)權(quán)利要求1所述的基于加權(quán)下推系統(tǒng)的中斷驗(yàn)證方法，其特征在于，所述的驗(yàn)證需求性質(zhì)包括：

1).程序運(yùn)行時(shí)是否滿足規(guī)定的時(shí)序邏輯；

2).程序是否會(huì)出現(xiàn)因中斷產(chǎn)生優(yōu)先級(jí)反轉(zhuǎn)的情況，即優(yōu)先級(jí)低的任務(wù)可以打斷優(yōu)先級(jí)高的任務(wù)及其子任務(wù)；

3).程序運(yùn)行是否滿足實(shí)時(shí)性，即能夠在規(guī)定的時(shí)間內(nèi)完成某項(xiàng)任務(wù)；

4).程序運(yùn)行時(shí)是否有因?yàn)橹袛喈a(chǎn)生的內(nèi)存訪問沖突。