一種基于進程代數(shù)的軟件可信性度量模型

楊文忠，黃傳河，張振宇

(1.新疆大學信息科學與工程學院，新疆烏魯木齊 830046;2.武漢大學計算機學院，湖北武漢 430072)

隨著人們的工作越來越依賴于各種軟件，軟件的可信性也變得越來越重要。然而隨著Internet的日益增長，基于Internet的軟件也越來越不可信。人們迫切需要可信的軟件，卻對軟件可信性的本質還沒有一致的認識，軟件可信性評估和度量也沒有一致的解決方案，這些都是可信軟件期待解決的問題。

文獻［1-2］認為軟件可信性是質量屬性的一個子集，即可信性是可靠性、可用性、可維護性和安全性等質量屬性的組合。但這只是從靜態(tài)的角度討論軟件的可信性，并沒有反映軟件的動態(tài)可信性。靜態(tài)可信性屬性該如何組合也是一個值得研究的問題［3-4］。從有關軟件可信性的定義來看，軟件可信性主要關注軟件動態(tài)行為的可信。文獻［5］提出了一種實用的基于Internet軟件的可信性概念模型及可信性保障框架。文獻［6］從Internet這個大的角度來保證軟件的可信性，其可信性保障框架由身份認證管理、服務高可用性保障機制和自動合作的刺激機制這3部分組成。

自從1972年ANDERSON［7］首次提出可信系統(tǒng)的概念后，人們對軟件系統(tǒng)的可信性從不同的角度進行了探討。ISO/IEC 15408規(guī)范認為，一個軟件系統(tǒng)可信是指系統(tǒng)的行為在任何條件下都是可預測的。TCG(trusted computing group)［8］認為，軟件系統(tǒng)的可信性是系統(tǒng)總是按照期望的方式向有意圖的目標發(fā)展。微軟認為可信賴的計算是一種可用的、可靠的、安全的計算。筆者認為軟件可信性是其行為總是與用戶的期望相一致。

筆者從軟件自身這個角度來評估和度量軟件的可信性，基于進程代數(shù)，提出了軟件行為可信性評估框架及軟件動態(tài)行為可信性度量指標，在可信性評估框架和度量指標的基礎上，還提出了軟件可信性評估和度量的算法。

1 進程代數(shù)基本概念

在進程代數(shù)方法中，系統(tǒng)的行為用進程來描述，進程由系統(tǒng)所能執(zhí)行的動作或事件組成。這里動作是一個抽象的概念，用來表示一個抽象的活動或行為。因此以進程代數(shù)為框架的并發(fā)系統(tǒng)分析都是建立在動作這個基礎概念上的。以動作為基礎，進程代數(shù)用算子的形式定義了進程間的各種相互作用，這樣，進程代數(shù)就能以一種組合化的方式來描述系統(tǒng)行為，這種組合化的系統(tǒng)描述方式將一個大的系統(tǒng)看成是由許多小的系統(tǒng)組合而成，因此比較適合描述大規(guī)模復雜并發(fā)系統(tǒng)。

1.1 進程代數(shù)定義

定義1 設a∈A，A?Obs，Obs為一個可以觀察到的所有動作集合，Var為一個進程變量的集合，x∈Var，進程代數(shù)PA由以下語法產生:

語法中，0為中止進程，即不能執(zhí)行任何動作的進程;a.P為動作前綴操作，表示系統(tǒng)先執(zhí)行動作a，然后執(zhí)行進程P;P1:P2為順序操作，表示系統(tǒng)先執(zhí)行進程P1的動作，P1成功結束后系統(tǒng)接著執(zhí)行進程P2;P1+P2為不確定性選擇操作，表示系統(tǒng)要么執(zhí)行進程P1，要么執(zhí)行進程P2;P1‖AP2為兩個進程P1和P2的并發(fā)操作，其中A中的動作是兩個進程需要同步的操作;PA為隱藏操作，其行為與P類似，不同的是集合A中的動作被看成是內部動作(τ);x和ux.P是為了支持遞歸操作引入的操作符，x為一個進程變量，ux.P為遞歸表達式。

定義2 一個標記遷移系統(tǒng)(LTS)是一個4元組(S，Act，→，s0)，其中:S為非空的狀態(tài)集合;Act?A為動作集合;→為S×Act×S狀態(tài)轉移關系;s0為初始狀態(tài)。

圖1 標記轉移系統(tǒng)圖示

定義4 設trs(P)和trs(Q)分別為進程P和Q的所有跡的集合。進程 P與Q交織跡等價［10-11］(即 P≈itQ)當且僅當 trs(P)=trs(Q)。

定義5 設P，Q為兩個進程，一個關系R?AS(P)×AS(Q)稱為進程P與Q之間的一個交織互模擬，當且僅當(P，Q)∈R，并且如果有(X，Y)∈R，則:

跟隨以前的模型[6]，每個節(jié)點v都有一個容量Cv，這是節(jié)點在每個時間步中可以處理的最大負載量.在人造網絡中，容量受到成本的限制.因此，很自然地假定節(jié)點v的容量Cv正比于其初始負載Lv(0)，即

兩個進程P和Q稱作交織互模擬等價(表示為P≈ibQ)，當且僅當進程P與Q之間存在一個交織互模擬關系。

1.2 進程代數(shù)結構化操作語義

結構化操作語義從數(shù)學方面提供了進程行為的嚴格描述，從而支持對系統(tǒng)行為的理解與推理。結構化操作語義如表1所示。

表1 進程代數(shù)結構化操作語義

2 軟件可信性度量模型框架

從軟件系統(tǒng)可信性的有關定義可看出，軟件的可信性本質上要從軟件的行為來評估和度量。軟件的行為越符合用戶的期望行為，軟件的可信性就越高;反之，其可信性就越低。軟件的預期行為主要是通過軟件需求來反映，其動態(tài)行為在需求分析中是通過UML［12］的協(xié)作圖、順序圖和狀態(tài)圖來建模。在正向工程期間可以得到軟件的協(xié)作圖和狀態(tài)圖即軟件的動態(tài)行為表示。可以通過轉換算法將需求階段的UML協(xié)作圖和狀態(tài)圖轉換成進程代數(shù)［13-15］，得到系統(tǒng)的高層需求行為進程。這個高層進程是進行軟件可信性評估的參照系，軟件動態(tài)行為可信評估的關鍵是將實現(xiàn)級進程和高層需求行為進程進行等價判斷，看其等價程度如何，等價程度越高，軟件的可信程度就越高，否則其可信程度就越低。在不等價時，計算軟件可信性度量指標TD，TD數(shù)值越大，則軟件可信性越高。軟件在運行過程中會產生方法調用序列或事件序列，這個序列稱為軟件的運行蹤跡［16-19］。通過對軟件蹤跡的分析去掉一些實現(xiàn)細節(jié)，如庫函數(shù)調用，構造函數(shù)等，可以得到軟件蹤跡的摘要。然后將軟件蹤跡摘要轉換成UML的順序圖，最后通過算法將該UML順序圖轉成進程代數(shù)［20］，這樣通過逆向工程便得到了軟件實現(xiàn)級進程。具體軟件可信評估框架如圖2所示。

圖2 軟件可信評估框架

3 可信性度量與算法

有了高層軟件需求行為進程和實現(xiàn)級進程，便可以進行軟件可信性的評估。設進程P和Q分別為軟件需求行為進程和軟件實現(xiàn)級進程，trs(P)，trs(Q)分別為進程P和進程Q的跡集合，則軟件的可信度可定義為符合用戶預期的行為占軟件行為總數(shù)的比例。即:

式中:分子為期望的進程的行為;vi為實現(xiàn)級進程Q在其第i次執(zhí)行過程中的行為蹤跡;wi為初始需求進程P的行為蹤跡，因而wi與vi的交集就是期望的進程行為。

軟件的動態(tài)可信度可以定義為:

式(2)即為軟件可信性最終度量，它是軟件各次期望行為的熵。由于軟件行為具有不確定性和動態(tài)性，因而利用熵來表示軟件行為可信性是合理可行的。

基于軟件可信性度量模型以及可信性度量公式，軟件可信性度量算法可以采用如下方法，輸入為需求級進程以及實現(xiàn)級進程。若需求級進程和實現(xiàn)級進程是互模擬等價，則說明軟件的實現(xiàn)完全符合用戶期望，因而算法輸出結果是高可信的;若需求級進程和實現(xiàn)級進程是交織跡等價，則說明軟件實現(xiàn)基本符合用戶期望，因而輸出結果為可信，當兩個進程不等價時則利用式(1)和式(2)計算軟件可信性，若TD值越高則軟件可信性越大，反之則越小。其算法流程如下:

輸入:需求行為進程P和實現(xiàn)級別進程Q

輸出:軟件可信性

IF進程P和進程Q滿足定義5 THEN

輸出高可信

ELSE IF進程P和進程Q滿足定義4 THEN

輸出可信

ELSE

利用式(1)和式(2)計算TD

END IF

輸出TD //TD為軟件的可信程度，數(shù)值越高，則軟件越可信

4 結論

筆者基于進程代數(shù)和軟件可信本質提出了軟件可信評估框架和軟件可信性度量指標TD。為了自動地評估軟件可信性，也提出了軟件可信性評估的算法。為了實現(xiàn)軟件可信評估，筆者還提出了UML協(xié)作圖、狀態(tài)圖和順序圖等向進程代數(shù)轉換的算法。今后將開發(fā)一套實際的軟件可信性評估系統(tǒng)。同時對某些問題進行更深入的研究，如軟件蹤跡摘要自動地轉換成UML順序圖，這對軟件的維護和理解很有意義。

［1］SHI H L，MA J，ZOU F Y.Software dependability evaluation model based on fuzzy theory［C］//Proceedings of the International Conference on Computer Science and Information Technology，ICCSIT 2008.［S.l.］:［s.n.］，2008:102-106.

［2］THOMAS T，YANG Y.An analysis to understand software trustworthiness［C］//Proceedings of the 9th International Conference for Young Computer Scientists，ICYCS 2008.［S.l.］:［s.n.］，2008:2366-2371.

［3］ZHANG Y，F(xiàn)ANG B，XU C Y.Trustworthiness metrics model for internetware［C］//First International Workshop on Education Technology and Computer Science.［S.l.］:［s.n.］，2009:1035-1037.

［4］ZHENG Z M，MA S L，LI W，et al.Dynamical characteristics of software trustworthiness and their evolutionary complexity［J］.Science in China Series F:Information Science，2009，52(12):1328-1334.

［5］WANG H M，TANG Y B，YIN G，et al.Trustworthiness of internet-based software［J］.Science in China Series F:Information Sciences，2006，49(6):759-773.

［6］VOAS J.Trusted software's holy grail system sciences［C］//Proceedings of the 36th Annual Hawaii Interna-tional Conference on 2003.［S.l.］:［s.n.］，2003:337-351.

［7］ANDERSON J P.Computer security technology planning study［M］.Bedford:Hanscom AFB，1972:59-114.

［8］Trusted Computing Group.TCG architecture overview［S］.

［9］BOLOGNESI T，BRINKSMA E.Introduction to the ISO specification language LOTOS［J］.Computer Networks and ISDN Systems，1987，14(1):25-59.

［10］GLABBEEK R J.The linear time-branching time spectrum［C］//CONCUR'90，Lecture Notes in Computer Science.［S.l.］:［s.n.］，1990:298-297.

［11］JIANG J，WU J.The preservation of interleaving equivalences［C］//Proceedings of the 10th IEEE International Conference on Engineering of Complex Computer Systems.［S.l.］:IEEE Computer Society Press，2005:580-589.

［12］Object Management Group.Unified modeling language［S］.

［13］POOLEY R.Using UML to derive stochastic process algebra models［M］.［S.l.］:Davies and Bradley，2008:23-33.

［14］TRIBASTONE M，GILMORE S.Automatic translation of UML sequence diagrams into PEPA models［C］//Quantitative Evaluation of Systems，QEST 2008.［S.l.］:［s.n.］，2088:205-214.

［15］AMSTEL M F，BRAND M G J，PROTIC Z，et al.Transforming process algebra models into UML state machines:bridging a semantic gap［J］.Theory and Practice of Model Transformations，2008，50(3):61-75.

［16］SYSTA T.Understanding the behavior of Java programs［C］//Reverse Engineering Working Conference Proceedings.［S.l.］:［s.n.］，2000:214-223.

［17］HAMOU-LHADJ A，LETHBRIDGE T.Summarizing the content of large traces to facilitate the understanding of the behaviour of a software system［C］//Proceedings of the 14th IEEE International Conference on Program Comprehension.［S.l.］:［s.n.］，2006:181-190.

［18］HAMOU-LHADJ A.Measuring various properties of execution traces to help build better trace analysis tools［C］//Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems.［S.l.］:［s.n.］，2005:559-568.

［19］JEREMY S，CHRIS K.Dynamic analysis of Java program concepts for visualization and profiling［J］.Science of Computer Programming，2008，70(2/3):111-126.

［20］PELAYO F L，CUARTERO F，VALERO V，et al.An example of performance evaluation by using the stochastic process algebra:ROSA［C］//Proceedings of the Seventh International Conference on Real-Time Systems and Applications.［S.l.］:IEEE Computer Society Press，2000:271-278.