一种基于进程代数的软件可信性度量模型

杨文忠，黄传河，张振宇

(1.新疆大学信息科学与工程学院，新疆乌鲁木齐 830046;2.武汉大学计算机学院，湖北武汉 430072)

随着人们的工作越来越依赖于各种软件，软件的可信性也变得越来越重要。然而随着Internet的日益增长，基于Internet的软件也越来越不可信。人们迫切需要可信的软件，却对软件可信性的本质还没有一致的认识，软件可信性评估和度量也没有一致的解决方案，这些都是可信软件期待解决的问题。

文献［1-2］认为软件可信性是质量属性的一个子集，即可信性是可靠性、可用性、可维护性和安全性等质量属性的组合。但这只是从静态的角度讨论软件的可信性，并没有反映软件的动态可信性。静态可信性属性该如何组合也是一个值得研究的问题［3-4］。从有关软件可信性的定义来看，软件可信性主要关注软件动态行为的可信。文献［5］提出了一种实用的基于Internet软件的可信性概念模型及可信性保障框架。文献［6］从Internet这个大的角度来保证软件的可信性，其可信性保障框架由身份认证管理、服务高可用性保障机制和自动合作的刺激机制这3部分组成。

自从1972年ANDERSON［7］首次提出可信系统的概念后，人们对软件系统的可信性从不同的角度进行了探讨。ISO/IEC 15408规范认为，一个软件系统可信是指系统的行为在任何条件下都是可预测的。TCG(trusted computing group)［8］认为，软件系统的可信性是系统总是按照期望的方式向有意图的目标发展。微软认为可信赖的计算是一种可用的、可靠的、安全的计算。笔者认为软件可信性是其行为总是与用户的期望相一致。

笔者从软件自身这个角度来评估和度量软件的可信性，基于进程代数，提出了软件行为可信性评估框架及软件动态行为可信性度量指标，在可信性评估框架和度量指标的基础上，还提出了软件可信性评估和度量的算法。

1 进程代数基本概念

在进程代数方法中，系统的行为用进程来描述，进程由系统所能执行的动作或事件组成。这里动作是一个抽象的概念，用来表示一个抽象的活动或行为。因此以进程代数为框架的并发系统分析都是建立在动作这个基础概念上的。以动作为基础，进程代数用算子的形式定义了进程间的各种相互作用，这样，进程代数就能以一种组合化的方式来描述系统行为，这种组合化的系统描述方式将一个大的系统看成是由许多小的系统组合而成，因此比较适合描述大规模复杂并发系统。

1.1 进程代数定义

定义1 设a∈A，A⊆Obs，Obs为一个可以观察到的所有动作集合，Var为一个进程变量的集合，x∈Var，进程代数PA由以下语法产生:

语法中，0为中止进程，即不能执行任何动作的进程;a.P为动作前缀操作，表示系统先执行动作a，然后执行进程P;P1:P2为顺序操作，表示系统先执行进程P1的动作，P1成功结束后系统接着执行进程P2;P1+P2为不确定性选择操作，表示系统要么执行进程P1，要么执行进程P2;P1‖AP2为两个进程P1和P2的并发操作，其中A中的动作是两个进程需要同步的操作;PA为隐藏操作，其行为与P类似，不同的是集合A中的动作被看成是内部动作(τ);x和ux.P是为了支持递归操作引入的操作符，x为一个进程变量，ux.P为递归表达式。

定义2 一个标记迁移系统(LTS)是一个4元组(S，Act，→，s0)，其中:S为非空的状态集合;Act⊆A为动作集合;→为S×Act×S状态转移关系;s0为初始状态。

图1 标记转移系统图示

定义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]，每个节点v都有一个容量Cv，这是节点在每个时间步中可以处理的最大负载量.在人造网络中，容量受到成本的限制.因此，很自然地假定节点v的容量Cv正比于其初始负载Lv(0)，即

两个进程P和Q称作交织互模拟等价(表示为P≈ibQ)，当且仅当进程P与Q之间存在一个交织互模拟关系。

1.2 进程代数结构化操作语义

结构化操作语义从数学方面提供了进程行为的严格描述，从而支持对系统行为的理解与推理。结构化操作语义如表1所示。

表1 进程代数结构化操作语义

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

从软件系统可信性的有关定义可看出，软件的可信性本质上要从软件的行为来评估和度量。软件的行为越符合用户的期望行为，软件的可信性就越高;反之，其可信性就越低。软件的预期行为主要是通过软件需求来反映，其动态行为在需求分析中是通过UML［12］的协作图、顺序图和状态图来建模。在正向工程期间可以得到软件的协作图和状态图即软件的动态行为表示。可以通过转换算法将需求阶段的UML协作图和状态图转换成进程代数［13-15］，得到系统的高层需求行为进程。这个高层进程是进行软件可信性评估的参照系，软件动态行为可信评估的关键是将实现级进程和高层需求行为进程进行等价判断，看其等价程度如何，等价程度越高，软件的可信程度就越高，否则其可信程度就越低。在不等价时，计算软件可信性度量指标TD，TD数值越大，则软件可信性越高。软件在运行过程中会产生方法调用序列或事件序列，这个序列称为软件的运行踪迹［16-19］。通过对软件踪迹的分析去掉一些实现细节，如库函数调用，构造函数等，可以得到软件踪迹的摘要。然后将软件踪迹摘要转换成UML的顺序图，最后通过算法将该UML顺序图转成进程代数［20］，这样通过逆向工程便得到了软件实现级进程。具体软件可信评估框架如图2所示。

图2 软件可信评估框架

3 可信性度量与算法

有了高层软件需求行为进程和实现级进程，便可以进行软件可信性的评估。设进程P和Q分别为软件需求行为进程和软件实现级进程，trs(P)，trs(Q)分别为进程P和进程Q的迹集合，则软件的可信度可定义为符合用户预期的行为占软件行为总数的比例。即:

式中:分子为期望的进程的行为;vi为实现级进程Q在其第i次执行过程中的行为踪迹;wi为初始需求进程P的行为踪迹，因而wi与vi的交集就是期望的进程行为。

软件的动态可信度可以定义为:

式(2)即为软件可信性最终度量，它是软件各次期望行为的熵。由于软件行为具有不确定性和动态性，因而利用熵来表示软件行为可信性是合理可行的。

基于软件可信性度量模型以及可信性度量公式，软件可信性度量算法可以采用如下方法，输入为需求级进程以及实现级进程。若需求级进程和实现级进程是互模拟等价，则说明软件的实现完全符合用户期望，因而算法输出结果是高可信的;若需求级进程和实现级进程是交织迹等价，则说明软件实现基本符合用户期望，因而输出结果为可信，当两个进程不等价时则利用式(1)和式(2)计算软件可信性，若TD值越高则软件可信性越大，反之则越小。其算法流程如下:

输入:需求行为进程P和实现级别进程Q

输出:软件可信性

IF进程P和进程Q满足定义5 THEN

输出高可信

ELSE IF进程P和进程Q满足定义4 THEN

输出可信

ELSE

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

END IF

输出TD //TD为软件的可信程度，数值越高，则软件越可信

4 结论

笔者基于进程代数和软件可信本质提出了软件可信评估框架和软件可信性度量指标TD。为了自动地评估软件可信性，也提出了软件可信性评估的算法。为了实现软件可信评估，笔者还提出了UML协作图、状态图和顺序图等向进程代数转换的算法。今后将开发一套实际的软件可信性评估系统。同时对某些问题进行更深入的研究，如软件踪迹摘要自动地转换成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，FANG 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.