MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\(','\\)']]}}); function MyAutoRun() {    var topp=$(window).height()/2; if($(window).height()>450){ jQuery(".outline_switch_td").css({ position : "fixed", top:topp+"px" }); }  }    window.onload=MyAutoRun; $(window).resize(function(){ var bodyw=$win.width(); var _leftPaneInner_width = jQuery(".rich_html_content #leftPaneInner").width(); var _main_article_body = jQuery(".rich_html_content #main_article_body").width(); var rightw=bodyw-_leftPaneInner_width-_main_article_body-25;   var topp=$(window).height()/2; if(rightw<0||$(window).height()<455){ $("#nav-article-page").hide(); $(".outline_switch_td").hide(); }else{ $("#nav-article-page").show(); $(".outline_switch_td").show(); var topp=$(window).height()/2; jQuery(".outline_switch_td").css({ position : "fixed", top:topp+"px" }); } }); 软件形式化开发关键部件选取的水波优化方法
  软件学报  2016, Vol. 27 Issue (4): 933-942   PDF    
软件形式化开发关键部件选取的水波优化方法
郑宇军1, 2 , 张蓓1, 薛锦云2    
1. 浙江工业大学 计算机科学与技术学院, 浙江 杭州 310023;
2. 江西省高性能计算重点实验室(江西师范大学), 江西 南昌 330027
摘要: 形式化方法有助于从根本上提高软件系统的质量与可靠性,但其开发成本往往过于高昂.一种折衷的办法是在软件系统中选取关键性部件进行形式化开发,但目前尚无非常有效的定量选择方法.将软件系统中的形式化开发关键部件选取建模为一个0-1约束规划问题,以便使用元启发式搜索方法对其进行优化求解.另外,针对该问题专门设计了一种离散水波优化(water wave optimization,简称WWO)算法.在一个大型软件系统上的应用验证了问题模型的有效性,同时证明了WWO算法相对于其他若干典型元启发式搜索方法的优越性.
关键词形式化方法    可靠度    元启发式搜索方法    水波优化算法    
Selection of Key Software Components for Formal Development Using Water Wave Optimization
ZHENG Yu-Jun1, 2 , ZHANG Bei1, XUE Jin-Yun2    
1. College of Computer Science and Technology, Zhejiang University of Technology, Hangzhou 310023, China;
2. Jiangxi Provincial Key Laboratory of High Performance Computing(Jiangxi Normal University), Nanchang 330027, China
Foundation item: National Natural Science Foundation of China (61020106009, 61105073, 61272075, 61473263)
Abstract: Formal methods contribute to the fundamental improvement of software quality and reliability, but this methodology is often very expensive. A compromise is to select and apply formal methods to only a subset of key components of the software system. However, currently there are few effective approaches for such selection process. This paper proposes a 0-1 constrained programming model for selecting key components for formal development, which enables the use of metaheuristic search methods to effectively solve the selection problem. The paper also designs a discrete water wave optimization(WWO) algorithm for the problem. The application to a large-scale software system validates the effectiveness of the proposed problem model, and demonstrates that the WWO algorithm outperforms some other typical metaheuristic search methods.
Key words: formal method    reliability    metaheuristic search method    water wave optimization(WWO)    

软件形式化方法是指建立在严格数学模型上、具有精确数学语义的软件系统开发方法,它能够从根本上提高软件系统的质量与可靠性.受“软件危机”以及硬件领域形式化方法发展的影响,软件形式化方法自20世纪80年代末以来得到了学术界和工业界的广泛关注[1].但是,关于何时、何处以及何种程度上在软件系统开发中引入形式化方法,仍然存在较大的争论.很多软件开发机构对于使用形式化方法仍然持谨慎甚至怀疑的态度,其原因在于软件形式化方法自身在理论和实践上的一些局限性[2],其中最主要的一点就是软件形式化方法往往需要付出相对高昂的代价[3],这使得对大型软件系统进行全面形式化开发通常是不现实的.

一种折衷的办法是,在软件系统开发中部分引入形式化方法.Easterbrook和Callahan[4]实践了对大规模安全关键性系统的部分规约进行形式化验证,但未介绍应如何选择这些部分规约,实践时完全依靠主观经验. Russo[5]提出了一些指导性原则用于选取重要软件部件进行形式化开发,主要包括安全关键性部件、具有复杂控制逻辑的部件、手工开发容易出错的部件,但这些原则大都是定性的,缺乏量化的选择依据.薛锦云提出的形式化方法PAR则强调对软件中的复杂算法进行形式化开发,特别是对算法循环不变式进行推导和验证[6,7].在文献[8]中,我们首次提出了一种基于软件度量的选择方法,即:根据功能点数量、耦合度、继承复杂度等度量给定一个阈值,然后选取超过阈值的部件进行形式化开发.这虽然是一种定量的方法,但由于软件度量本身的局限性[9],选取的效果与实际期望之间往往还存在较大的距离.

基于搜索的软件工程[10]是研究利用元启发搜索方法来求解软件工程中的优化问题,相关技术已被应用在软件工程的多个领域[11],包括软件需求工程、费用估算、编译器优化、代码优化,特别是软件测试[12].但到目前为止,元启发搜索方法在形式化软件工程相关问题中的研究还极为罕见.

针对大型软件系统中形式化开发的关键部件选取(selection of key software components,简称SKSC)问题,本文提出了一个非线性0-1规划问题模型,其目标是在给定的开发工作量和费用约束下最大化整个系统的(预期)可靠性水平.为了有效地求解该问题,本文提出了一种离散水波优化(water wave optimization,简称WWO)算法[13],其中设计了特定的传播、折射和碎浪操作.在一个大型软件系统上的实验结果表明,所设计的离散WWO算法优于其他若干流行的元启发式算法.

1 形式化开发关键部件选取的优化问题模型 1.1 决策变量

本文考虑对选取的软件关键部件进行完整的形式化,即,从形式化的需求规格说明、验证直至代码生成(精化/转换)[14, 15, 16].形式化开发的最小部件单位为数据类型(以下简称为类).给定一个软件系统的总体结构,我们首先筛选出3种类:一是无需专门开发的类(如类库中已有的类),二是必须进行形式化开发的类(如执行安全攸关功能的类),三是不适合或尚无法进行形式化开发的类(如富媒体界面类).记剩余的类的集合为C,集合大小为n,需要从中选取用于形式化开发的类的子集.该问题是一个0-1规划问题,即:问题的解可编码为一个长度为n的向量,向量第i维为1表示部件i进行形式化开发,为0表示非形式化开发.

1.2 目标函数

对于已有的类,通过统计分析估算其可靠度:对于使用形式化方法开发的类,其可靠度直接估算为1;对于不使用形式化方法开发的类,可分别基于代码行数或功能点来估算其可靠度[17].不过我们发现,将二者组合起来的估算结果更为准确.对于类x,记其预计(需要手工编写的)代码行数为L(x),分配的功能点集合为F(x),则x的可靠度按如下经验公式进行估算:

$R(x) = 1 - \gamma \left[{0.2{{\left( {\frac{{L(x)}}{{{L_{\max }}}}} \right)}^a} + 0.8\frac{{\sum\limits_{f \in F(x)} {{b^{O(f)}}} }}{{{b^5}|F(x)|}}} \right]$ (1)

其中,Lmax为一个独立类的代码行数建议上限,O(f)为对功能点f的复杂度评值(在1~5之间,1为最简单,5为最复杂),ab是两个常数(本文中分别取经验值0.72和1.18),γ是代表开发团队能力的一个系数(在0~1之间,值越小代表能力越强).

基于部件可靠度来估算整个系统可靠度的方法大致可以分为3类.

(1) 基于结构复合的方法[18, 19, 20],其优点是计算方式简单,但缺点是假定每个部件的内部状态是固定的,因此估算准确度相对较低;

(2) 基于概率统计的方法,如基于状态转移概率和故障传播概率的方法[21, 22, 23],其优点是估算准确度相对较高,但缺点是计算量相对较大,且往往需要通过测试来统计先验概率值,不适合于尚未开发的软件;

(3) 基于软计算的方法,如基于神经网络和模糊计算的方法[24, 25, 26],其优点是几乎不需要关于系统的假定条件,但缺点是计算量较大,而且一般需要大量历史数据来进行训练.

后两类方法的前提条件在本文的场景中难以满足,且软件可靠度本身无法做到精确的估算,而进化算法的大量迭代也能部分补偿适应度函数的不准确度[27],故这里采用第1类方法,复合时考虑以下3种情况.

(1) K个部件x1,x2,…,xK的顺序(串联)组合(如图 1所示),其复合结构x的可靠度为

$R(x) = \prod\limits_{k = 1}^K {R({x_k})} $ (2)
Fig. 1 Serial composition of components 图 1 部件的串联结构

(2) K个部件x1,x2,…,xK的并行(并联)组合(如图 2所示),其复合结构x的可靠度为

$R(x) = 1 - \prod\limits_{k = 1}^K {(1 - R({x_k}))} $ (3)
Fig. 2 Parallel composition of components 图 2 部件的并联结构

(3) 一个部件x0K个部件x1,x2,…,xK的选择调用组合(如图 3所示),设其中每个部件的调用概率为hk(1≤kK),其复合结构x的可靠度为

$R(x) = R({x_0})\sum\limits_{k = 1}^K {{h_k}R({x_k})} $ (4)
Fig. 3 Conditional composition of components 图 3 部件的选择复合结构

其他更为复杂的结构大都可以由以上3种结构复合而成.通过自底向上地逐级复合,最后估算出整个系统S(X)的可靠度R(S(X))[18, 19, 20],其中,X为问题的决策向量.问题的目标就是最大化整个系统的可靠度.

$MaxR(S(X))$ (5)

对于大规模的软件系统,该目标函数涉及到大量部件及其复合结构的可靠度计算,是一个高度复杂、非线性的目标函数.

1.3 约束条件

考虑开发时间和费用两方面的约束条件,二者都是基于开发工作量来进行估算的.软件成本及工作量估算有算法模型、类比、回归分析、神经网络等多种方法[28].原则上,只要在估算时能够区分形式化和非形式化开发的区别,任何一种方法都可以用于本文的问题模型.给定问题的一个决策向量X,记其中形式化开发的类的子集(即Xi=1的元素集合)为CF(X),工作量估算函数为p1;非形式化开发的类的集合(即Xi=0的元素集合)为CN(X),工作量估算函数为p2,则CF(X)和CN(X)的开发工作量可分别计算为

${p_F}(X) = \sum\limits_{{x_i} \in {C_F}(X)} {{p_1}({x_i})} $ (6)
${p_N}(X) = \sum\limits_{{x_i} \in {C_N}(X)} {{p_2}({x_i})} $ (7)

我们的研究主要采用COCOMO-II模型[29]及其在形式化开发中的扩展模型[30]来估算开发工作量,单位为人·月(PM).不论是p1还是p2,都是基于如下的基础模型来估算每个类x的工作量p(x):

$p(x) = A \cdot {\left( {1 + \frac{{V(x)}}{{100}}L(x)} \right)^B} \cdot E$ (8)

其中,A为校准因子,B为工作量比例因子,E为成本因子,V(X)为类x的需求演化和变更因子.形式化开发与非形式化开发工作量的区别,主要就在于前3个因子取值的不同.

CF(X)∪CN(X)中所有类的开发工作量上限为Pmax,则对工作量的约束可表达为

${p_F}\left( X \right) + {p_N}\left( X \right) \le {P_{max}}$ (9)

再设非形式化开发中每PM的平均费用为c1,形式化开发的平均费用为c2,所有类的开发费用上限为Cmax,则对费用的约束可表达为

${c_1}{p_F}\left( X \right) + {c_2}{p_N}\left( X \right) \le {C_{max}}$ (10)

值得注意的是:上述对开发工作量和费用的估算都是针对基础类进行的,而不包括各级部件复合乃至最终系统集成的费用,因为我们只区分基础类的形式化和非形式化开发,而不同的选择策略对后期的复合和集成费用不会产生区别.因此,上述估算策略并不适用于对整个软件系统的开发工作量和费用的精确估算.

2 求解问题的水波优化算法

前一小节提出的SKSC问题是一个复杂的非线性0-1约束规划问题,可应用各种元启发式方法进行求解.本文设计了一种基于WWO的求解算法.

2.1 基本水波优化算法

WWO是一种基于浅水波理论[31]的启发式算法,它将问题的搜索空间类比为海床,将问题的每个解类比为一个“水波”,水波的适应度与其到海床的垂直距离成反比:距离海平面越近的点,对应的解越优,相应的水波能量越高,那么水波的波高h更大、波长λ更小,如图 4所示[13].

Fig. 4 Illustration of the WWO algorithm model 图 4 水波优化模型示意图

这使得较优的解在较小的范围内进行搜索,而较差的解在较大的范围内进行搜索,从而促进整个种群不断向更优的目标进化.

WWO算法在初始化时将每个水波的h值设置为一个整数常量hmax,λ值设置为0.5.在进化过程中,WWO提供了3种具体操作,即传播、折射和碎浪.

(1) 传播

在算法每次迭代过程中,种群中的每个水波都传播一次.设问题的维数为n,当前水波X在每一维的位置记为X(d),其传播后在每一维的新位置为

$X'\left( d \right) = X\left( d \right) + rand( - 1,1) \cdot \lambda L\left( d \right)$ (11)

其中,rand(-1,1)代表[-1,1]范围里的一个均匀分布随机数,L(d)代表搜索空间在第d维的长度(1≤dn).如果某一维的新位置超出了有效范围,则将其随机设置为有效范围内的一个位置.

f表示问题的适应度函数,传播后计算新波X'的适应度值,如果f(X')>f(X),则X'在种群中取代X,其波高重置为hmax;反之,X会被保留,且其波高h由于能量的损耗而减1.

每次迭代后,算法按下式对种群中的每个水波X的波长进行更新.

$\lambda = \lambda \cdot {\alpha ^{ - (f(X) - {f_{\min }} + \varepsilon )/({f_{\max }} - {f_{\min }} + \varepsilon )}}$ (12)

其中,fmaxfmin分别表示当前种群中的最大和最小适应度值,参数α表示波长的衰减系数,ε是一个极小的正数(以避免分母为0的情况发生).

(2) 折射

当某个水波Xh值递减为0时,对其折射操作以避免搜索停滞,折射后每一维的位置计算公式如下:

$X'(d) = N\left( {\frac{{{X^*}(d) + X(d)}}{2},\frac{{|{X^*}(d) - X(d)|}}{2}} \right)$ (13)

其中,X表示目前位置所找到的最优解,N(μ,σ)表示均值为μ、方差为σ的高斯随机数.折射后新波X'的波高同样重置为hmax,波长则按下式进行更新,这也会使得解的适应度与波长成反比.

$\lambda ' = \lambda \frac{{f(X)}}{{f(X')}}$ (14)

(3) 碎浪

水波能量的不断增加会使其波峰变得越来越陡峭,直至破碎成一连串的孤立波.WWO算法对每个新找到的最优解X*执行碎浪操作,具体方式是:先随机选择k维(这里,k是介于1和一个预定义参数kmax之间的一个随机数),在每一维d上产生一个孤立波X'.

$X'\left( d \right) = X\left( d \right) + N\left( {0,1} \right) \times \beta \cdot L\left( d \right)$ (15)

其中,参数β表示碎浪系数.如果生成的所有孤立波的适应度值均不优于X*,则保留X*;否则,将X*替换为最优的一个孤立波.

基本WWO算法步骤描述如下:

第1步. 随机初始化一个种群,计算其中每个解x的适应度值f(x),找出其中的最优解x*;

第2步. 若终止条件满足,算法结束,返回x*;

第3步. 对种群中的每个解x执行如下过程:

      第3.1步. 对x执行传播操作,得到一个新波x';

      第3.2步. 若f(x')>f(x),则用x'替换x:

            第3.2.1步. 若f(x')>f(x),则用x'替换x*,并对x执行碎浪操作;

      第3.3步. 否则,将x的波高h值减1;

            第3.3.1步. 若h=0,对x执行折射操作;

      第3.4步. 更新种群中所有解的波长,而后转第2步;

2.2 离散水波优化算法

基本WWO算法适用于连续空间中的全局优化问题.SKSC问题属于组合优化问题,因此需要对WWO的算子进行调整.

(1) 传播

WWO传播操作的原则就是使适应度值高的个体具有短波长,从而在较小的范围进行搜索;反之,适应度值低的个体在较大范围内进行搜索.针对SKSC问题,我们基于邻域结构来定义传播操作.给定任意一个解向量X,其直接邻域解可通过两种方式得到:一是将一个非形式化开发的类改为形式化开发(对应元素由0变为1),二是将一个形式化开发的类改为非形式化开发(对应元素由1变为0).那么对于维数为n的问题,邻域结构的大小就是n.算法初始化时,每个解的波长设为n1/4.对于波长为λ的解X,其传播操作就是随机生成它的一个λ步邻域解.每次迭代后,每个解的波长按下式进行更新.

$\lambda = {n^{0.5({f_{\max }} - f(X) + \varepsilon )/({f_{\max }} - {f_{\min }} + \varepsilon )}}$ (16)

特别地,当f(X)取最大值fmax时,λ=1,传播操作生成一个一步(直接)邻域解;当f(X)取最小值fmin时,λ=n1/2,传播操作随机执行|n1/2|步0-1变换.

(2) 折射

WWO折射操作的本质是向当前最优解X*学习.针对SKSC问题,我们定义在给定解X上的传播操作执行方式如下:

i) 计算C1=CF(X*)\CF(X),C2=CN(X*)\CN(X);

ii) 计算K=N(m,m-min(|C1|,|C2|)),其中,m=(|C1|+|C2|)/2;

iii) 在CF(X)\CF(X*)中随机取min(K,|CF(X)\CF(X*)|)个元素,将其值由1变为0;

iv) 在CN(X)\CN(X*)中随机取min(K,|CN(X)\CN(X*)|)个元素,将其值由0变为1.

也就是说,传播操作是将X中部分与X*不同的解分量改为与X*相同,且由1变为0的分量数与由0变为1的分量数大致持平.

(3) 碎浪

针对SKSC问题上定义的碎浪操作也是基于邻域结构的:每当传播操作得到一个新的当前最优解X*时,生成X*k个一步和二步邻域解;如果其中包含比X*更优的解,则再次更新当前最优解.

(4) 约束处理

这里,对SKSC问题的约束条件(9)和约束条件(10)采用惩罚函数的处理方法.对于每个解X,计算其对约束(9)和约束(10)的违反度Ψ1(X)=max(pF(X)+pN(X)-Pmax,0),Ψ2(X)=max(c1pF(X)+c2pN(X)-Cmax,0),再按下式计算其适应度值:

$f\left( X \right) = R\left( {S\left( X \right)} \right) - {M_1}{\Psi _1}\left( X \right) - {M_2}{\Psi _2}\left( X \right)$ (17)

其中,M1M2是两个很大的正数,其值通常要比PmaxCmax高几个数量级.

(5) 复杂度分析

设目标函数f的计算复杂度为O(f),邻域变换和随机数生成的计算复杂度均用常数c表示,算法种群规模为N.每次传播操作执行λ步邻域变换并对得到的邻域解进行估值,故每次迭代中传播操作的时间复杂度最坏情况下不超过O(N(nc+O(f))).折射操作产生一个介于当前波高为0的个体与当前最优个体之间的新个体,每次操作的时间复杂度为O(c+O(f)).碎浪操作只在当前最优个体上执行,每次操作生成其k个邻域解,时间复杂度不超过O(kmax(c+O(f))).每次迭代时,折射操作和碎浪操作不可能同时作用于同一个个体,故算法每次迭代的时间复杂度最坏情况下不超过O(N(nc+kmaxc+kmaxO(f))).

若设置算法最大迭代次数为T,则算法的计算复杂度为O(TN(nc+kmaxc+kmaxO(f))).

(6) 操作示例

假定问题维度为6,对一个编码为101011的解X,设波长为2,则传播操作执行二步随机邻域变换,不妨设先在第二维、后在第五维上变换,则变换后的结果为111001.若该解优于X,则用其取代X.

再设当前最优解X*为011010,则XX*在第1位、第5位、第6位上不同,则折射操作在X的第1位和第6位中随机选取一个(不妨设选取第6位)由1变0,并将X的第5位由0变1,故折射后的结果为111010.

X*执行碎浪操作,设k=rand(1,kmax)=3,则随机生成其3个一步或二步邻域解(如011110,011100,011000);若其中包含比X*更优的解,则用其替换X*.

3 计算实验

上述模型和算法应用于一个大型军事指挥控制软件的开发决策,其特点是可靠性要求较高、开发时间又较为紧迫.经初步设计,确定该系统包含1 364个基本类,其中1 168个类尚不确定是否要使用形式化方法来进行开发.该形式化开发部件的选取问题建模为第1节中的SKSC问题,并使用第2节中的离散WWO算法来进行求解.为验证算法性能,还在该问题实例上运行以下4种流行算法来进行比较.

• 一种用于子集选取的遗传算法(genetic algorithm,简称GA)[32];

• 二进制粒子群优化(binary particle swarm optimization,简称BPSO)算法[33];

• 一种改进的二进制PSO算法IBPSO,它将PSO搜索与Lambda迭代相结合[34];

• 二进制差分搜索(binary differential evolution,简称BDE)算法[35].

实验环境为一台使用Intel Core i5-2430M处理器、4GB DDR3内存、Windows 7操作系统的计算机,算法程序均使用Visual Studio 2010环境开发.所有算法的种群大小均设为50,WWO设置为h=6,kmax=6,其他4种算法的参数均按其原始文献进行设置.为公平比较,对所有算法设定统一的终止条件,即,适应度估值次数达到50 000次.每种算法随机运行30次,统计其各次求得最优解(最大可靠度,以%为单位)的中位数(median)、平均值(mean)、最大值(max)、最小值(min)、方差(std)以及平均运行时间(time,以秒为单位),结果见表 1.其他4种算法的结果与WWO的结果还分别进行了秩和校验,均值前的上标“+”表示WWO算法的结果显著优于该算法(置信度为95%).

Table 1 Computational results of the five algorithms on the given SKSC problem instance 表 1 5种算法在给定软件系统形式化开发部件选取问题上的运行结果

从计算时间来看,GA的运行时间最长,BDE运行时间最短,WWO的运行时间略长于BDE但短于其余3种算法.这说明WWO的算法速度也是较为理想的.总的来说,5种算法的运行时间相差不大,这是因为问题的适应度计算较为复杂,占用了算法的绝大多数运行时间,而5种算法的适应度估值次数上限是相同的.而且从算法每次接近1小时的运行时间来看,该问题的求解难度也是相当大的.

从计算结果来看:可靠度,median,max和min值最高的都是WWO算法,而mean值最高的是BDE算法(这主要是因为WWO的结果中出现了一个显著噪点而拉低了mean值).BPSO算法的综合表现最差,IBPSO对其进行了一定改进,但求解效果仍不如BDE和WWO;GA的性能大致介于BPSO和IBPSO之间.从统计检验的结果来看,WWO算法的结果比GA,BPSO和IBPSO都有显著提升,仅与BDE之间无显著性差异.按30次运行结果的中位数来比较,WWO求得的可靠度比GA,BPSO,IBPSO,BDE分别高1.86%,2.95%,1.35%,0.33%;而按30次运行结果的最大值来比较,WWO求得解的可靠度仍比其余4种算法分别高0.80%,1.17%,0.50%,0.26%.对于绝大多数重要软件系统,这种程度的可靠性提升对系统拥有者来说是极为重要的,在很多情况下,甚至能够决定系统关键任务的成败[36].

从理论上分析,SKSC问题不同解的目标函数值相差可能很大,解空间易形成多峰分布,而且峰附近可能存在较大起伏.上述算法都是将一个n维0-1规划问题的解编码为一个长度为n的二进制串.BPSO仍采用传统粒子群中向个体最优和全局最优的学习公式,而后将公式产生的实数位舍入为二进制位,这种转换策略在处理长串时学习效果很不理想.IBPSO和BDE对此进行了改进,增强了全局搜索能力,但在起伏较大的峰附近的局部搜索能力较弱.GA中的操作最适合本问题的编码方式,但它与其他很多GA算法一样,都容易过早地陷入局部最优.而WWO算法能够基于波长机制很好地平衡全局探索和局部开发,更容易通过水波群来定位多峰,通过折射操作避免搜索停滞,并通过碎浪操作来增强在起伏较大的峰附近的局部搜索,因此在SKSC问题上表现出了极佳的性能.

此外,我们还采用了文献[8]中基于软件度量的方法来对系统中的形式化开发部件进行选取,并基于选取结果来进行系统可靠度估算,得出的结果是91.05%,该值低于上述所有元启发式搜索算法的最差结果.这充分说明了本文所提出的SKSC优化问题模型的有效性以及所设计的算法的优越性.相比于基于软件度量的定量方法,WWO求得最佳结果的可靠度提升了5.41%,这是一个相当正面的结果.

该系统的开发决策最终采纳了WWO求得的最佳解(估算可靠度为95.98%).基于9个月的实际运行数据分析,系统的实测可靠度为94.80%.这种偏差的主要原因在于模型参数经验取值的误差,此外也存在系统用户早期使用的磨合问题.但即便如此,预计可靠度与实测可靠度的误差仍不超过1.25%,这也进一步说明了问题模型的有效性.总的说来,系统拥有者对基于本文问题模型和算法所做出的形式化开发决策非常满意.

4 结束语

形式化方法有助于从根本上提高软件系统的质量与可靠性,但其成本往往远高于传统的开发方法.本文提出了一个在软件系统中选取关键部件进行形式化开发的SKSC优化问题模型,并设计了一种离散WWO算法来对其进行有效求解.通过在一个典型系统上的应用,证明了本文提出的模型和算法的有效性.

本文针对SKSC智能优化进行了初步研究,目前正在以下几个方面开展进一步的工作.

• 当前模型考虑的是对选取部件进行完整的形式化开发,对此可作进一步细化,考虑不同程度的形式化方法的应用,如形式化需求导出、形式化规格说明、形式化验证、形式化代码推导/转换等,都可单独地应用到不同的部件上;

• 当前模型只对系统整体的可靠性进行一个粗略估算,下一步可考虑系统不同部分以及执行不同任务的不同可靠性需求,从而为形式化开发部件的选取提供更为精准的指导;

• 当前模型对开发成本的估算也较为粗略,可融合神经网络、模糊推理等技术进行更精确的估算.

此外,当前模型和算法只在一个特定软件系统上进行了测试.我们正在将其扩展应用于更多数量和类型的软件系统,以便为模型和算法改进提供更充足的数据支持.

参考文献
[1] Vienneau RL. A review of formal methods. In: Dorfman M, Thayer RH, eds. Proc. of the Software Engineering. Washington: IEEE Computer Society Press, 1996. 181-192.
[2] Kneuper R. Limits of formal methods. Formal Aspects of Computing, 1997,9(4):379-394 .
[3] Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J. Formal methods: Practice and experience. ACM Computing Surveys (CSUR), 2009,41(4):1-40 .
[4] Easterbrook S, Callahan J. Formal methods for verification and validation of partial specifications: A case study. Journal of Systems and Software, 1998,40(3):199-210 .
[5] Russo AG. Partial applications of formal methods. In: Boulanger JL, ed. Proc. of the Industrial Use of Formal Methods: Formal Verification. Hoboken: John Wiley & Sons, 2013. 195-214 .
[6] Xue JY. Two new strategies for developing loop invariants and their applications. Journal of Computer Science and Technology, 1993,8(2):147-154 .
[7] Xue JY. A unified approach for developing efficient algorithmic programs. Journal of Computer Science & Technology, 1997,12(4): 314-329 .
[8] Zheng YJ, Wang JQ, Wang K, Xue JY. Partially introducing formal methods into object-oriented development: Case studies using a metrics-driven approach. In: Misra J, Nipkow T, Sekerinski E, eds. Proc. of the Formal Methods. Berlin: Springer-Verlag, 2006. 190-204 .
[9] Kan SH. Metrics and Models in Software Quality Engineering. 2nd ed., Reading MA: Addison-Wesley, 2003.
[10] Harman M, Jones BF. Search-Based software engineering. Information and Software Technology, 2001,43(14):833-839 .
[11] Harman M. The current state and future of search based software engineering. In: Briand LC, Wolf AL, eds. Proc. of the Future of Software Engineering. Washington: IEEE Computer Society, 2007. 342-357 .
[12] McMinn P. Search-Based software test data generation: A survey. Software Testing, Verification and Reliability, 2004,14(2): 105-156 .
[13] Zheng YJ. Water wave optimization: A new nature-inspired metaheuristic. Computers & Operations Research, 2015,55:1-11 .
[14] Xue JY. A unified approach for developing efficient algorithmic programs. Journal of computer Science and Technology, 1997, 12(4):314-329 .
[15] Sekerinski E, Kaisa S, eds. Program Development by Refinement: Case Studies Using the B Method. Berlin: Springer-Verlag, 1998.
[16] Zheng YJ, Ling HF, Xue JY. Combinatorial optimization problem reduction and algorithm derivation. Ruan Jian Xue Bao/Journal of Software, 2011,22(9):1985-1993 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3948.htm
[17] Musa JD, Iannino A, Okumoto K. Software Reliability: Measurement, Prediction, Application. New York: McGraw-Hill, 1987.
[18] Zhu H. Toward a relationship between software reliability estimation and complexity analysis. Ruan Jian Xue Bao/Journal of Software, 1998,9(9):713-717 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/9/713.htm
[19] Hamlet D, Mason D, Woit D. Theory of software reliability based on components. In: Müller HA, ed. Proc. of the 23rd Int’l Conf. on Software Engineering. Washington: IEEE Computer Society, 2001. 361-370 .
[20] Xu SY. Design and Analysis of Dependable Computational Systems. Beijing: Tsinghua University Press, 2006 (in Chinese).
[21] Smidts C, Stutzke M, Stoddard RW. Software reliability modeling: An approach to early reliability prediction. IEEE Trans. on Reliability, 1998,47(3):268-278 .
[22] Wang WL, Pan D, Chen MH. Architecture-based software reliability modeling. Journal of Systems and Software, 2006,79(1): 132-146 .
[23] Palviainen M, Evesti A, Ovaska E. The reliability estimation, prediction and measuring of component-based software. Journal of Systems and Software, 2011,84(6):1054-1070 .
[24] Kiran NR, Ravi V. Software reliability prediction by soft computing techniques. Journal of Systems and Software, 2008,81(4): 576-583 .
[25] Guo P. Computational Intelligence in Software Reliability Engineering. Beijing: Science Press, 2012 (in Chinese).
[26] Bhuyan MK, Mohapatra DP, Sethi S. Measures for predicting software reliability using time recurrent neural networks with back- propagation. ACM SIGSOFT Software Engineering Notes, 2015,40(5):1-8 .
[27] Mansanne F, Carrere F, Ehinger A, Schoenauer M. Evolutionary algorithms as fitness function debuggers. In: Raś ZW, Skowron A, eds. Proc. of the Foundations of Intelligent Systems. Berlin: Springer-Verlag, 1999. 639-647 .
[28] Li MS, He M, Yang D, Su DF, Wang Q. Software cost estimation method and application. Ruan Jian Xue Bao/Journal of Software, 2007,18(4):775-795 (in Chinese with English abstract). http://www.jos.org.cn/1000-9825/18/775.htm
[29] Boehm BW, Abts C, Brown AW, Chulani S, Clark BK, Horowitz E, Madachy R, Reifer D, Steece B. Software Cost Estimation with COCOMO II. New York: Prentice Hall, 2000.
[30] Zheng YJ, Wang K, Xue JY. An extension of COCOMO II for the B-method. In: Sullivan K, Kazman R, eds. Proc. of the 7th Int’l Workshop on Economics Driven Software Engineering Research. New York: ACM Press, 2006. 11-14 .
[31] Huang H. Dynamics of Surface Waves in Coastal Waters: Wave-Current-Bottom Interactions. New York: Springer-Verlag, 2009.
[32] Tan F, Fu X, Zhang Y, Bourgeois AG. A genetic algorithm-based method for feature subset selection. Soft Computing, 2008,12(2): 111-120 .
[33] Kennedy J, Eberhart RC. A discrete binary version of the particle swarm algorithm. In: Tien JM, ed. Proc. of the IEEE Int’l Conf. on Systems, Man, and Cybernetics. Piscataway: IEEE, 1997. 4104-4108 .
[34] Yuan X, Nie H, Su A, Wang L, Yuan Y. An improved binary particle swarm optimization for unit commitment problem. Expert Systems with Applications, 2009,36(4):8049-8055 .
[35] Pampara G, Engelbrecht AP, Franken N. Binary differential evolution. In: Proc. of the IEEE Congress on Evolutionary Computation. Piscataway: IEEE, 2006. 1873-1879 .
[36] Schneidewind NF. Reliability modeling for safety-critical software. IEEE Trans. on Reliability, 1997,46(1):88-98 .
[16] 郑宇军,薛锦云,凌海风.组合优化问题简约与算法推演.软件学报,2011,22(9):1985-1993. http://www.jos.org.cn/1000-9825/3948.htm
[18] 朱鸿.软件可靠性估计与计算复杂性的关系浅析.软件学报,1998,9(9):713-717. http://www.jos.org.cn/1000-9825/9/713.htm
[20] 徐拾义.可信计算系统设计与分析.北京:清华大学出版社,2006.
[25] 郭平.软件可靠性工程中的计算智能方法.北京:科学出版社,2012.
[28] 李明树,何梅,杨达,舒风笛,王青.软件成本估算方法及应用.软件学报,2007,18(4):775-795. http://www.jos.org.cn/1000-9825/18/775.htm