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

有效

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

本發(fā)明公開了一種基于可滿足性求解的同步語言程序自動驗證方法，包括將同步語言程序中的枚舉值、用戶自定義類型和常量內聯(lián)到同步語言程序的節(jié)點里，在同步語言程序的主節(jié)點中遞歸地內聯(lián)所有被調用的節(jié)點，得到一個包含單一節(jié)點的同步語言程序，然后通過引入新的局部數(shù)據(jù)流將程序的內存深度降為1，最后將包含單一節(jié)點的同步語言程序及其安全屬性表示為命題邏輯公式，并利用可滿足性模理論求解器驗證同步語言程序是否滿足待驗證的安全屬性。本發(fā)明支持直接驗證大規(guī)模復雜同步語言程序，能夠提高驗證能力和效率、保證程序的可靠性和安全性。

技術領域

本發(fā)明涉及計算機軟件領域，尤其涉及一種基于可滿足性求解的同步語言程序自動驗證方法。

背景技術

航空、航天、核能、交通等安全關鍵領域的嵌入式系統(tǒng)軟件大都使用同步數(shù)據(jù)流語言(簡稱同步語言)開發(fā)實現(xiàn)，比如SCADE，Esterel，Lustre和Signal等語言。同步語言是一種聲明式語言，其基本的數(shù)據(jù)抽象是數(shù)據(jù)流。一個同步語言程序由一個或多個節(jié)點構成，類似于C/C++中的函數(shù)。每個節(jié)點具有零個或更多的輸入數(shù)據(jù)流和局部數(shù)據(jù)流、以及一個或更多的輸出數(shù)據(jù)流。數(shù)據(jù)流就是一個值的序列，而且同步語言只支持布爾型、整型和實數(shù)型數(shù)據(jù)流。數(shù)據(jù)流通常用序列(x₁,x₂,x₃,...)表示，括號內的x₁,x₂,x₃分別表示這個數(shù)據(jù)流在第1、2、3個時鐘上的值。在同步語言程序中，任何變量和表達式都表示一個由多個時鐘上的值所構成的數(shù)據(jù)流，例如變量x表示數(shù)據(jù)流(x₁,x₂,x₃,...)。

同步語言中常用的操作符包括：算術符(+，-，*，/，div，mod)、布爾操作符(and，or，not)、關系操作符(，＝，，＝)、條件符(if-then-else)和時序操作符，其中，時序操作符主要包括如下幾種：

(1)pre(X)表示用表達式X在前一個時鐘上的值構成一個新的數(shù)據(jù)流。例如，如果整型變量X的值序列為X＝(x₁,x₂,x₃,...,x_n,...)，那么pre(X)的值序列為pre(X)＝(nil,x₁,x₂,...,x_n-1,...)，其中nil表示空值。

(2)X-Y表示用表達式X和Y構成一個新的數(shù)據(jù)流，該數(shù)據(jù)流在第1個時鐘上的值與X相同，在其余時鐘上的值與Y相同。例如，如果X＝(x₁,x₂,x₃,...,x_n,...)和Y＝(y₁,y₂,y₃,...,y_n,...)是具有相同類型和相同時鐘的兩個表達式，那么X-Y是與X和Y具有相同類型和相同時鐘的表達式，且X-Y＝(x₁,y₂,y₃,...,y_n,...)。也就是說，除了第一個時鐘，X-Y總是等于Y。在SCADE等同步語言中還有一個類似的操作符fby，fby(Y,n,X)是與X和Y具有相同類型和相同時鐘的表達式，其中n是一個靜態(tài)整數(shù)，且fby(Y,n,X)＝X-pre(X-pre(...pre(X-pre(Y))...))。