顧名宇

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

?

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

顧名宇

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

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

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

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

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

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

1　數(shù)理邏輯

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

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

1.1命題演算

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

1.2謂詞演算

謂詞演算也叫做命題函數(shù)演算。在謂詞演算里，把命題的內(nèi)部結構分析成具有主詞和謂詞的邏輯形式，由命題函數(shù)項、邏輯連接詞和量詞構成命題，然后推導命題之間的邏輯關系。命題函數(shù)項就是指除了含有常項以外還含有變項的邏輯公式。常項是指一些確定的對象或者確定的屬性和關系，變項是指一定范圍內(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)程序可靠性驗證，主要是把命題演算和謂詞演算結合起來，使用相應的推導公式完成目標推理的驗證過程。

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

2.1程序可靠性定義

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

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

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

2.2程序可靠性驗證步驟

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

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

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

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

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

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

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

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

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

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

->S

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

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

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

->T

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

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

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

同理可以完成的證明。

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

在客戶端服務器程序設計中，常常有客戶端向服務器提交一系列任務（R1..Rn），該序列任務是具有某個呼叫計劃標志。而服務端將該呼叫任務標志添加到R1……Rn呼叫隊列中，該隊列是一維數(shù)組R_Work[Max]，Max是提交任務最大量。往該數(shù)組添加計劃呼叫標志的條件是數(shù)組R_Work[i].bz=0 (0<=i < Max)?？蛻舳嗣看蜗蚍斩颂峤蝗蝿照埱螅斩吮仨殢脑摽蛻舳撕艚嘘犃刑崛∪蝿?，并完成相應的執(zhí)行任務。

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

提交任務

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

程序F2：

程序完成相應的任務

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

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

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

從前面看出存在：

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

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

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

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

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

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

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

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

有任務R1,….,Rn,存在任意Ri、Rk，Ri

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

證明目標：證明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ù)組下標k，k=(R_Nextpoll+ i)%Max，如果i> 0，有Rk后于Ri被處理。Rk為數(shù)組k下標對應的時間序任務。

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

4　小結

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

參考文獻

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

[2]李興鋒,張新常,楊美紅,等.基于SPIN的模塊化模型檢測方法研究[J].電子與信息學報,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]黃達明,曾慶凱.基于分離邏輯的程序驗證技術[J].軟件學報,2009,20(8):2051-2061

[6]單卓為,魚濱.基于SPIN的CSCW系統(tǒng)的驗證[J].計算機技術與發(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

文獻標識碼:A

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