[發(fā)明專利]一種基于可滿足性求解的同步語言程序自動驗證方法

有效

• 申請?zhí)枺?/td>: 202011103235.5
• 申請日: 2020-10-15
• 公開（公告）號: CN112269734B
• 公開（公告）日: 2022-04-26
• 發(fā)明（設計）人: 陳哲;孫毅;冉丹
• 申請（專利權）人: 南京航空航天大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 南京經(jīng)緯專利商標代理有限公司 32200
• 代理人: 施昊

1.一種基于可滿足性求解的同步語言程序自動驗證方法，其特征在于，包括如下步驟：

s1：將同步語言程序中的枚舉值、用戶自定義類型和常量內(nèi)聯(lián)到同步語言程序的節(jié)點里；

s2：在所述同步語言程序的主節(jié)點中遞歸地內(nèi)聯(lián)所有被調用的節(jié)點，得到一個包含單一節(jié)點N的同步語言程序；

s3：通過引入新的局部數(shù)據(jù)流將程序的內(nèi)存深度降為1，方法具體如下：

首先，假設所述單一節(jié)點N中的數(shù)據(jù)流集合V＝{x₁，x₂，...，x_p，y₁，y₂，...，y_q}，其中x₁～x_p為輸入數(shù)據(jù)流，y₁～y_q為局部數(shù)據(jù)流或輸出數(shù)據(jù)流，所述單一節(jié)點N中的數(shù)據(jù)流y₁～y_q在第n個時鐘上的值y₁(n)～y_q(n)構成的等式集合Δ(n)表示為：

其中，y_i(n)表示數(shù)據(jù)流y_i在第n個時鐘上的值，V(n)表示V中的數(shù)據(jù)流在第n個時鐘上的值，t₁～t_q表示對應的等式右邊的表達式，d是N中pre操作符的最大內(nèi)存深度，假設數(shù)據(jù)流y_i和數(shù)據(jù)流x_j之間存在一個包含d個pre操作符的等式y(tǒng)_i＝pre(pre(…(pre(x_j))))，則引入d-1個新的局部數(shù)據(jù)流y_ix_j1，…，y_ix_j(d-1)，將原等式替換為y_i＝pre(y_ix_j1)，并增加等式y(tǒng)_ix_j1＝pre(y_ix_j2)，…，y_ix_j(d-1)＝pre(x_j)，使得等式中pre操作符的最大內(nèi)存深度由d降低為1，此時，所述單一節(jié)點N的等式集合變?yōu)槿缦滦问剑?/p>

其中y_q+1～y_m是新增的局部數(shù)據(jù)流，t_q+1～t_m表示對應的等式右邊的表達式，將所述單一節(jié)點N中的數(shù)據(jù)流在第n個時鐘上的值V(n)稱為瞬時結構，Δ′(n)中的y_i(n)的值就是第n和n-1個時鐘上的瞬時結構構成的函數(shù)，因此所述單一節(jié)點N即為基于瞬時結構的約束型系統(tǒng)；

s4：將所述包含單一節(jié)點N的同步語言程序表示為在第n個時鐘上的命題邏輯公式N(n)，將其安全屬性P表示為命題邏輯公式P(n)，具體方法如下：

將包含所述單一節(jié)點N的同步語言程序及其安全屬性P分別表示為在第n個時鐘上的命題邏輯公式N(n)和P(n)，其中所述命題邏輯公式N(n)即為將所述Δ(n)中的等式用合取運算符相連得到的公式，所述命題邏輯公式P(n)為將所述安全屬性P中的變量標識符用該變量在第n個時鐘上的值替換后得到的表達式；

s5：基于所述命題邏輯公式N(n)和P(n)構造驗證公式，并利用可滿足性模理論驗證所述驗證公式是否成立。

2.根據(jù)權利要求1所述的一種基于可滿足性求解的同步語言程序自動驗證方法，其特征在于，

所述步驟s1中的內(nèi)聯(lián)操作使用映射數(shù)據(jù)結構來實現(xiàn)，且通過遍歷同步語言程序，將所述同步語言程序中所有映射數(shù)據(jù)結構中的鍵替換為其在映射中對應的值。