【摘要】：軟件的安全性問題越來越突出,當(dāng)下,除了應(yīng)用同行評(píng)審和軟件測試等進(jìn)行驗(yàn)證外,還可應(yīng)用形式化驗(yàn)證在項(xiàng)目早期盡快發(fā)現(xiàn)軟件缺陷。形式化驗(yàn)證指采取數(shù)學(xué)方式對(duì)軟件系統(tǒng)建模并分析,目的是通過嚴(yán)格的數(shù)學(xué)推理來建立正確的系統(tǒng)。而且,對(duì)于一些要求較高安全性的系統(tǒng)而言,形式化方法是最佳的驗(yàn)證技巧。對(duì)這些系統(tǒng)的驗(yàn)證一般是通過提供基于系統(tǒng)的抽象數(shù)學(xué)模型上的形式化證明、數(shù)學(xué)模型和被驗(yàn)證的系統(tǒng)之間的相關(guān)性來實(shí)現(xiàn)的。當(dāng)前,用于建模系統(tǒng)的一些數(shù)學(xué)模型包括:有限狀態(tài)集,標(biāo)記遷移系統(tǒng),Petri網(wǎng),向量加法系統(tǒng),時(shí)間自動(dòng)機(jī),進(jìn)程代數(shù)等。并發(fā)理論是理論計(jì)算機(jī)科學(xué)中眾多一直比較活躍的研究領(lǐng)域之一。一些用于建模和驗(yàn)證并發(fā)系統(tǒng)的形式化模型被相繼提出,比如Petri網(wǎng)和向量加法系統(tǒng)、進(jìn)程演算等。盡管Petri網(wǎng)主要是提供在物理世界上的計(jì)算方法,而向量加法系統(tǒng)主要用于并發(fā)編程的形式化模型,但之后他們被證明是數(shù)學(xué)上等價(jià)的。向量加法系統(tǒng)由有限個(gè)整數(shù)向量組成,系統(tǒng)的格局是自然數(shù)向量的集合,每一步的遷移是對(duì)當(dāng)前的格局應(yīng)用一個(gè)整數(shù)向量而到達(dá)另一個(gè)格局。向量加法系統(tǒng)上的一些研究主要圍繞的問題包括可達(dá)性問題、可覆蓋性問題等。為了增加向量加法系統(tǒng)的表達(dá)能力,在其基礎(chǔ)上進(jìn)行擴(kuò)增又衍生出了一些其他模型,如帶狀態(tài)的向量加法系統(tǒng)、遞歸向量加法系統(tǒng)、交替向量加法系統(tǒng)等。Cai和Ogawa將下推系統(tǒng)和向量加法系統(tǒng)相結(jié)合,提出良結(jié)構(gòu)下推系統(tǒng),可用于建模遞歸多線程程序。良結(jié)構(gòu)下推系統(tǒng)具有強(qiáng)大的表達(dá)能力,向量加法系統(tǒng)及一些對(duì)其擴(kuò)展的模型可被規(guī)約到良結(jié)構(gòu)下推系統(tǒng)上,例如分支向量加法系統(tǒng)、遞歸向量加法系統(tǒng)等。因此,良結(jié)構(gòu)下推系統(tǒng)的研究結(jié)論可直接被用于這些模型上。盡管向量加法系統(tǒng)的擴(kuò)展模型的一些可覆蓋性問題還未被解決,但可以對(duì)該問題的難度進(jìn)行一定的衡量,即可以通過尋找該問題難度的上界和下界,通過二者之間差距的不斷縮小而確定。本文提出一個(gè)用于證明模型可覆蓋性問題下界的一般性框架,并基于重置0(即不測試一個(gè)變量值的情況下直接對(duì)其賦值為0),利用規(guī)約的方式得到下界。基于本文提出的框架,驗(yàn)證了下推向量加法系統(tǒng)的可覆蓋性問題的難度下界為TOWER難的,與已知的Lazic提出的下界難度相一致。并證明了對(duì)以3維自然數(shù)向量為狀態(tài)的且棧字符集有限的良結(jié)構(gòu)下推系統(tǒng)和狀態(tài)集有限且以3維自然數(shù)向量為棧字符集的良結(jié)構(gòu)下推系統(tǒng),其可覆蓋性問題的難度下界是Ackermann難的;狀態(tài)集有限且棧字符集為n+3維良擬序集的良結(jié)構(gòu)下推系統(tǒng),其可覆蓋性問題的下界是Hyper-Ackermann難的。本文還提出良結(jié)構(gòu)的帶有范圍限制匹配關(guān)系的多棧下推系統(tǒng)(簡記為WSMPDS),對(duì)多棧下推系統(tǒng)中的彈棧操作進(jìn)行限制,即僅當(dāng)一個(gè)棧頂符號(hào)是上k個(gè)輪回里被壓入棧中的才可被執(zhí)行彈棧操作(其中k為某個(gè)固定的常量),而且棧字符集為良擬序集,然后介紹其可覆蓋性問題的定義。并通過向量加法系統(tǒng)的可覆蓋性問題到此模型的可覆蓋性問題的規(guī)約,得出了其可覆蓋性問題的下界是EXPSPACE難的。
【圖文】：

Fig 1 1 Compute function (2 ) using one local variable規(guī)則。例 1.2. 圖1 2左側(cè)為計(jì)算 的程序。因?yàn)槲覀儾辉试S零測試， 是布爾表達(dá)式，可不確定地計(jì)算出true或false，與良結(jié)構(gòu)下推系統(tǒng)中不允許 0 測試（測試一個(gè)值是否為 0）相一致。該程序不能精確地計(jì)算出 ，但保證計(jì)算出的最大值是 。圖1 3中列出了 的計(jì)算過程，顯然圖1 2左側(cè)的程序可模擬此計(jì)算過程。而且,用函數(shù) 模擬；用函數(shù) 模擬；用函數(shù) 模擬；該程序可以被形式化為右側(cè)的良結(jié)構(gòu)下推系統(tǒng)，其中狀態(tài)是一個(gè)由全局變量 的當(dāng)前值和左側(cè)程序代碼的行號(hào)組成的序?qū)Γ瑮Ｗ址癁樽髠?cè)程序的函數(shù)名集合（除去 MAIN 函數(shù)）。狀態(tài)間的遷移規(guī)則描述了操作全局變量和棧的方式。例如在右側(cè)的良結(jié)構(gòu)下推系統(tǒng)中

Fig 1 1 Compute function (2 ) using one local variable規(guī)則。例 1.2. 圖1 2左側(cè)為計(jì)算 的程序。因?yàn)槲覀儾辉试S零測試， 是布爾表達(dá)式，可不確定地計(jì)算出true或false，與良結(jié)構(gòu)下推系統(tǒng)中不允許 0 測試（測試一個(gè)值是否為 0）相一致。該程序不能精確地計(jì)算出 ，，但保證計(jì)算出的最大值是 。圖1 3中列出了 的計(jì)算過程，顯然圖1 2左側(cè)的程序可模擬此計(jì)算過程。而且,用函數(shù) 模擬；用函數(shù) 模擬；用函數(shù) 模擬；該程序可以被形式化為右側(cè)的良結(jié)構(gòu)下推系統(tǒng)，其中狀態(tài)是一個(gè)由全局變量 的當(dāng)前值和左側(cè)程序代碼的行號(hào)組成的序?qū)�，棧字符集為左�?cè)程序的函數(shù)名集合（除去 MAIN 函數(shù)）。狀態(tài)間的遷移規(guī)則描述了操作全局變量和棧的方式。例如在右側(cè)的良結(jié)構(gòu)下推系統(tǒng)中
【學(xué)位授予單位】：上海交通大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2018
【分類號(hào)】：TP311.53

【參考文獻(xiàn)】

相關(guān)期刊論文 前1條

1 靳陽;蔡小娟;李國強(qiáng);;良結(jié)構(gòu)下推系統(tǒng)的表達(dá)能力[J];上海交通大學(xué)學(xué)報(bào);2015年08期

本文編號(hào)：2658339