顧名宇

安順職業(yè)技術(shù)學(xué)院信息工程系,貴州安順561000

?

數(shù)理邏輯的程序可靠性驗證

顧名宇

安順職業(yè)技術(shù)學(xué)院信息工程系,貴州安順561000

摘要:程序可靠性驗證往往占用軟件開發(fā)周期很長的時間，而現(xiàn)行的軟件可靠性驗證方法主要是基于形式化的方法如基于SPIN的模型檢測方法等，但這種方法可能由于模型建立的問題導(dǎo)致驗證的復(fù)雜性極大提高，造成最后驗證失敗的結(jié)果比比皆是。為解決此問題，本文使用數(shù)學(xué)方法從數(shù)理邏輯角度用推理的方法實現(xiàn)了程序可靠性驗證，并完成了客戶服務(wù)器程序的可靠性驗證，證明了該方法切實有效。

關(guān)鍵詞:數(shù)理邏輯;程序;可靠性

在計算機(jī)系統(tǒng)中，軟硬件都有可靠性指標(biāo)的要求并必須經(jīng)過驗證。對于軟件設(shè)計者來說，如果軟件沒有通過驗證,那么整個系統(tǒng)的可靠性仍是沒有保證的。軟件可靠性驗證方法多種多樣，比如有基于SPIN模型檢測方法及各種形式分化分析方法等[2][6]，很多方法停留在抽象的理論研究上，而在實際應(yīng)用中很少使用到。

而對于大多數(shù)程序員來說，對于程序的可靠性的驗證采用了比較熟悉的軟件工程的方法，比如軟件工程中的白盒、黑盒等測試，但這些測試的統(tǒng)計故障率不能完全作為可靠性評估的依據(jù)。例如，即使白盒測試的語句覆蓋率達(dá)100%，分支覆蓋率為90%以上，程序路徑覆蓋率為70%以上，只能說明這些語句的分支、程序路徑?jīng)]有錯誤,不能保證程序已達(dá)到了很高的可靠性。因為畢竟只覆蓋了一部份,也許在未覆蓋的部分仍存在著故障率很高的缺陷。

所以，本文結(jié)合軟件開發(fā)實踐，探索了一種切實可用的方法，即用基于數(shù)學(xué)方法的數(shù)理邏輯法實現(xiàn)程序可靠性的邏輯推理驗證。

1　數(shù)理邏輯

數(shù)理邏輯又稱符號邏輯[5]，是用數(shù)學(xué)方法研究邏輯或形式邏輯的學(xué)科。早在1847年，英國數(shù)學(xué)家布爾建立了一系列的運算法則，利用代數(shù)的方法研究邏輯問題，初步奠定了數(shù)理邏輯的基礎(chǔ)。之后，德國數(shù)學(xué)家弗雷格讓數(shù)理邏輯的符號系統(tǒng)更加完備，使現(xiàn)代數(shù)理邏輯最基本的理論基礎(chǔ)逐步形成，并成為一門獨立的學(xué)科。

數(shù)理邏輯包括兩個最基本的也是最重要的“命題演算”和“謂詞演算”。

1.1命題演算

命題演算是研究關(guān)于命題如何通過一些邏輯連接詞構(gòu)成更復(fù)雜的命題以及邏輯推理的方法。命題是指具有具體意義的又能判斷它是真還是假的句子。如果把命題看作運算的對象，如同代數(shù)中的數(shù)字、字母或代數(shù)式，而把邏輯連接詞看作運算符號，就象代數(shù)中的“加、減、乘、除”那樣，那么由簡單命題組成復(fù)合命題的過程，就可以當(dāng)作邏輯運算的過程，也就是命題的演算。比如：如果x==0, 則y=5;

1.2謂詞演算

謂詞演算也叫做命題函數(shù)演算。在謂詞演算里，把命題的內(nèi)部結(jié)構(gòu)分析成具有主詞和謂詞的邏輯形式，由命題函數(shù)項、邏輯連接詞和量詞構(gòu)成命題，然后推導(dǎo)命題之間的邏輯關(guān)系。命題函數(shù)項就是指除了含有常項以外還含有變項的邏輯公式。常項是指一些確定的對象或者確定的屬性和關(guān)系，變項是指一定范圍內(nèi)的任何一個，這個范圍叫做變項的變域。命題函數(shù)項和命題演算不同，它無所謂真和假。如果以一定的對象概念代替變項，那么命題函數(shù)項就成為真的或假的命題。例如，如果x==0,則y=5，使用謂詞演算來描述，用P(x,y)表示x==y,Q(x,y)表示x=y,x是整數(shù)，y是整數(shù)，則可描述為P(x,0)->Q(y,5)。

用數(shù)理邏輯推理實現(xiàn)程序可靠性驗證，主要是把命題演算和謂詞演算結(jié)合起來，使用相應(yīng)的推導(dǎo)公式完成目標(biāo)推理的驗證過程。

2　使用數(shù)理邏輯驗證程序可靠性方法

2.1程序可靠性定義

程序可靠性定義有多種，為方便證明，先看當(dāng)前的標(biāo)準(zhǔn)的程序可靠性定義：美國IEEE計算機(jī)學(xué)會對“軟件可靠性”作出了明確定義，此后該定義被美國標(biāo)準(zhǔn)化研究所接受為國家標(biāo)準(zhǔn)，多年后，我國也接受該定義為國家標(biāo)準(zhǔn)。該定義包括兩方面的含義：

（1）在規(guī)定的條件下，在規(guī)定的時間內(nèi)，軟件不引起系統(tǒng)失效的概率；

（2）在規(guī)定的時間周期內(nèi)，在所述條件下程序執(zhí)行所要求的功能的能力。

2.2程序可靠性驗證步驟

這里的驗證排除了軟件開發(fā)階段的各種錯誤，主要考慮系統(tǒng)失效和程序功能問題。使用數(shù)理邏輯驗證程序的步驟可分為以下三步：

（1）根據(jù)程序需求建立模型[5]，對所要驗證的程序或模塊進(jìn)行抽象化[3]，構(gòu)建檢測模型。

從程序可靠性定義得知，主要涉及到到程序系統(tǒng)失效和功能問題。

程序的失效主要涉及數(shù)據(jù)輸入和函數(shù)調(diào)用問題，建立如下數(shù)學(xué)描述：x1,x2,x3,…,xn是n個變量或輸入數(shù)據(jù)，用V(xi)(0<=i<=n)表示xi取值合法，用F1,F2,…Fm表示函數(shù)調(diào)用,因參數(shù)數(shù)量各不相同，故參數(shù)略，用P1,P2,…PK表示函數(shù)的參數(shù)調(diào)用，S表示程序正常。

用y1,y2,…yl表示要完成的功能項，W(yj)表示完成的第yj個功能,其中0<=j<=l,

（2）使用邏輯公式表示所要驗證的性質(zhì)，公式要能正確地表達(dá)所要驗證的內(nèi)容。

為便于描述驗證性質(zhì)，規(guī)定：

=F1（）?F2（）?…?Fn（）

=F1（）?F2（）…?Fn（）

程序的失效主要是通過合法和非法數(shù)據(jù)獲取或錄入，調(diào)用規(guī)定的函數(shù)及參數(shù)實現(xiàn)結(jié)果S，當(dāng)滿足規(guī)定的條件時，下面公式為真：

->S

其中0<=l<=n,0<=t<=n。

從一名大學(xué)畢業(yè)生到田園創(chuàng)客，從農(nóng)資店長到合作社理事長，又從農(nóng)場經(jīng)理到“正陽牛”打藥團(tuán)隊隊長，牛超憑著一股“牛勁兒”和 “牛脾氣”，扎根田園，不懈努力，帶領(lǐng)“正陽?！眻F(tuán)隊自主研發(fā)農(nóng)機(jī)植保設(shè)備，與廣西田園植保公司聯(lián)盟，在正陽成立“正陽牛”民兵植保服務(wù)隊136個，分別與全縣60多家農(nóng)機(jī)合作社、60家家庭農(nóng)場、60家種糧大戶簽訂了農(nóng)藥統(tǒng)防統(tǒng)治和莊稼植保托管合同，植保面積達(dá)100萬畝，每年勞務(wù)收入近300萬元。牛超被當(dāng)?shù)剞r(nóng)民稱贊為追夢田園創(chuàng)業(yè)的“植保達(dá)人”和“正陽牛人”。

對于程序功能正確性證明，當(dāng)滿足程序規(guī)定的條件時，可以描述為：

->T

T表示“真”，->T為真，說明程序功能都正確。

（3）驗證，通過對輸入值或變量設(shè)置合法和非法的數(shù)據(jù)，程序能正常結(jié)束，且所有變量在所有函數(shù)路徑中取值都符合要求[1]，每條語句所包括的所有變量的取值都滿足相互的邏輯關(guān)系，能完成規(guī)定的功能，即說明程序是可靠的。

在數(shù)理邏輯證明以上公式過程中，所有命題公式和謂詞演算的推理理論都實用。如果程序較為復(fù)雜，可按其定義的函數(shù)或把其分解為多個函數(shù)后用相應(yīng)可能的參數(shù)代入來進(jìn)行測試，確保每個都是真即得到S。

同理可以完成的證明。

3　用數(shù)理邏輯法驗證客戶服務(wù)器程序

在客戶端服務(wù)器程序設(shè)計中，常常有客戶端向服務(wù)器提交一系列任務(wù)（R1..Rn），該序列任務(wù)是具有某個呼叫計劃標(biāo)志。而服務(wù)端將該呼叫任務(wù)標(biāo)志添加到R1……Rn呼叫隊列中，該隊列是一維數(shù)組R_Work[Max]，Max是提交任務(wù)最大量。往該數(shù)組添加計劃呼叫標(biāo)志的條件是數(shù)組R_Work[i].bz=0 (0<=i < Max)?？蛻舳嗣看蜗蚍?wù)端提交任務(wù)請求，服務(wù)端必須從該客戶端呼叫隊列提取任務(wù)，并完成相應(yīng)的執(zhí)行任務(wù)。

客戶端向R_Work[Max]添加任務(wù)采用如下程序F1：

提交任務(wù)

服務(wù)端檢測某個客戶端的提交任務(wù)采用如下的方式：

程序F2：

程序完成相應(yīng)的任務(wù)

這里涉及到兩個函數(shù)F1和F2，函數(shù)F1可提交1-MAX個任務(wù)，F(xiàn)2可以執(zhí)行相應(yīng)的任務(wù)，由程序可靠性驗證可以進(jìn)一步抽象出：對于任意的任務(wù)i，當(dāng)滿足R_Work[i].bz=0時，有F1(i),0<=i

再來看看程序可靠性第二方面的證明，即程序功能性證明：

設(shè)：提交第i個任務(wù)簡寫為F1(i),執(zhí)行第j個任務(wù)簡寫成F2(j)

從前面看出存在：

當(dāng)R_Work[i].bz=0時，F(xiàn)1(i)為真

當(dāng)R_Work[j].bz !=0是，F(xiàn)2(j)為真

當(dāng)iT成立，但F2(j)->T（i==j）并不一定成立，這就說明了本程序第二方面得不到滿足。

實際上，通過閱讀程序F1、程序F2，很容易就可以發(fā)現(xiàn)在F2很有可能先處理后添加進(jìn)來的任務(wù)，而前面添加的任務(wù)得不到執(zhí)行。

所以必須修改代碼程序F1、F2，使其按照時間順序執(zhí)行任務(wù)。如果在R_Work[i]中增加一個時間成員，那么每次檢測隊列即數(shù)組時要對R_Work進(jìn)行排序，使用最快的算法也要增加Max*log（Max）次運算。

所以考慮對每個任務(wù)，添加了一個R_Nextwork變量(初始為0)，對程序F1、F2做了如下的修改：

對修改過的程序，除了增加幾個變量外[4]，程序代碼和F1、F2區(qū)別不大，所以程序可靠性第一方面證明沒有問題，下面進(jìn)一步證明程序可靠性的第二方面，即功能性證明：

現(xiàn)在建立模型：

有任務(wù)R1,….,Rn,存在任意Ri、Rk，Ri

F3(Ri)->T，F(xiàn)3(Rk)->T，F(xiàn)4(Rk)->T為重言式

證明目標(biāo)：證明F4(Ri)先于F4(Rk)執(zhí)行,即F4(Ri)->T也成立。

現(xiàn)在來分析：

（1）對于程序F3，因為有：F3(Ri)->T，F(xiàn)3(Rk)->T，且Ri

（2）對于程序F4，因為F4(Rk)->T成立，所以F4(Rk)被執(zhí)行。同時，對于任意Ri，存在R_Nextpoll=Ri；對于數(shù)組下標(biāo)k，k=(R_Nextpoll+ i)%Max，如果i> 0，有Rk后于Ri被處理。Rk為數(shù)組k下標(biāo)對應(yīng)的時間序任務(wù)。

綜合（1）（2），得出：當(dāng)Ri和Rk都被提交后,只要F4(Rk)->T成立，那么F4(Ri)->T也成立，并在F4(Rk)之前執(zhí)行。

4　小結(jié)

在程序的可靠性驗證中，程序驗證的復(fù)雜性在于執(zhí)行流程、時間和環(huán)境的不確定性使驗證的內(nèi)容與目標(biāo)的關(guān)系難以把握，如果采用適當(dāng)?shù)尿炞C方法，將會極大減少程序的測試和驗證時間，特別是隨著程序復(fù)雜性越來越高，采用單一的驗證方法滿足不了程序可靠性的要求。本文研究了采用數(shù)理邏輯的方法實現(xiàn)程序的可靠性驗證，數(shù)理邏輯對程序的可靠性驗證需要根據(jù)程序構(gòu)建驗證模型，然后根據(jù)條件，推導(dǎo)出相應(yīng)的結(jié)果是否符合要求。數(shù)理邏輯方法可以不拘泥于形式，如果在其基礎(chǔ)上把數(shù)學(xué)工具中的方法綜合運用將會起到事半功倍的效果，也為廣大軟件開發(fā)人員及測試人員快速實現(xiàn)程序驗證提供了一種新的嘗試。

參考文獻(xiàn)

[1]萬良.基于隔離邏輯的并行程序可靠性驗證方法[J].計算機(jī)工程,2014,40(2):86-91,96

[2]李興鋒,張新常,楊美紅,等.基于SPIN的模塊化模型檢測方法研究[J].電子與信息學(xué)報,2011,33(4):902-907

[3] Alexey G, Honseok Y. Modular Verification of Preemptive OSKernels[J].ACM SIGPLAN Notices,2011,46(9):404-417

[4] Cohen E, Schulte W, Tobies S. Local Verification of Global Invariants in Concurrent Programs[C]//Proceedings of the 22nd international conference on Computer Aided Verification.Berlin:Springer 2010:480-494

[5]黃達(dá)明,曾慶凱.基于分離邏輯的程序驗證技術(shù)[J].軟件學(xué)報,2009,20(8):2051-2061

[6]單卓為,魚濱.基于SPIN的CSCW系統(tǒng)的驗證[J].計算機(jī)技術(shù)與發(fā)展,2008,18(4):9-12,15

[7] 0’Heam P W. Tutorial on Separation Logic[C]//Proeeedings of the 20th International Conference on Computer Aided Verification.Berlin: Springer, 2008:15-21

Validation of Reliability on Mathematical Logic Program

GU Ming-yu

Anshun Vocational and Technical College of Information Engineering, Anshun 561000, China

Abstract:The reliability verification of program often takes a very long time to develope the software, while the current software reliability verification method is mainly based on formal methods such as SPIN based on model checking method, but this method may lead to the complexity of verification to improve greatly bing due to model problems, and then finally fails in validation results everywhere. In order to solve this problem, this paper used mathematical methods from mathematical logic perspective to realize the program reliability verification, and completed the reliability verification of client server program, the method was be proved the validity in true.

Keywords:Mathematical logic; program; validation

作者簡介:顧名宇(1960-),男,貴州安順人,副教授.研究方向:項目管理,信息安全. E-mail:gumingyu60@126.com

收稿日期:2013-07-13修回日期: 2013-07-24

中圖法分類號:TP301

文獻(xiàn)標(biāo)識碼:A

文章編號:1000-2324(2015)04-0621-04