软件形式化开发关键部件的选取 一种基于水波优化的方法 郑宇军, 张蓓, 薛锦云

提 纲 引言 01 问题模型 02 优化算法 03 计算实验 04

引言 形式化方法（Formal Methods) 建立在严格数学模型上、具有精确数学语义的软件系统开发方法 CSBSE 2015, Nanjing, China 引言 形式化方法（Formal Methods) 建立在严格数学模型上、具有精确数学语义的软件系统开发方法 能够从根本上提高软件系统的质量与可靠性 Floyd断言法 (Floyd 1967) /Hoare公理系统 (Hoare 1969) VDM (Jones 1990) Z-Method (Spivey 1992; Lano and Haughton 1994) B-Method (Abrial 1996; 2010) PAR方法 (Xue 1997; 1999) Cleanroom software engineering (Stacy et al. 2000) SPEC# (Barnett et al. 2005) UML-B (Snook and Butler 2006) 郑宇军, 张蓓, 薛锦云

引言 形式化方法（Formal Methods) 对开发人员的高要求 高昂的开发代价 较低的开发效率 CSBSE 2015, Nanjing, China 引言 形式化方法（Formal Methods) 对开发人员的高要求 高昂的开发代价 较低的开发效率 其它局限性：非形式化的需求，COTS集成…… 不适合大型软件系统的全程开发 郑宇军, 张蓓, 薛锦云

Whether, Where, When, and to Which degree CSBSE 2015, Nanjing, China Whether, Where, When, and to Which degree 引言 在大型软件系统开发中部分引入形式化方法 对部分规约进行形式化验证 (Easterbrook & Callahan 1998) 指导性原则 (Russo 2013) 基于软件度量的选择 (Zheng et al. 2006) 郑宇军, 张蓓, 薛锦云

Whether, Where, When, and to Which degree CSBSE 2015, Nanjing, China Whether, Where, When, and to Which degree 引言 在大型软件系统开发中部分引入形式化方法 建立优化问题模型: 0-1 programming 基于元启发的搜索方法: Water wave optimization (WWO) 郑宇军, 张蓓, 薛锦云

问题模型 决策变量 软件总体结构: 所有类型 候选集: A\AE\AC\AU 目标子集: 用于(完整)形式化开发的类集 CSBSE 2015, Nanjing, China 问题模型 决策变量 软件总体结构: 所有类型 候选集: A\AE\AC\AU 目标子集: 用于(完整)形式化开发的类集 郑宇军, 张蓓, 薛锦云

问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 CSBSE 2015, Nanjing, China 问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 郑宇军, 张蓓, 薛锦云

问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 CSBSE 2015, Nanjing, China 问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 郑宇军, 张蓓, 薛锦云

问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 CSBSE 2015, Nanjing, China 问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 郑宇军, 张蓓, 薛锦云

问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 CSBSE 2015, Nanjing, China 问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 郑宇军, 张蓓, 薛锦云

问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 CSBSE 2015, Nanjing, China 问题模型 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 郑宇军, 张蓓, 薛锦云

问题模型 约束条件 总工作量约束 总费用约束 形式化开发的类的子集: CF(X) 非形式化开发的类的子集: CN(X) CSBSE 2015, Nanjing, China 问题模型 形式化开发的类的子集: CF(X) 非形式化开发的类的子集: CN(X) 约束条件 总工作量约束 总费用约束 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 求解问题的WWO算法 基本WWO算法: 基于浅水波理论的启发式算法 Newton (1687): 深水波的频率与波长的平方根成反比 Laplace运动方程(1776) Kelland 运动方程(1844) 2π/λ 波高 波速 Zheng YJ (2015) Water wave optimization: A new nature- inspired metaheuristic, Comput Oper Res 55: 1-11 doi:10.1016/j.cor.2014.10.008 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 求解问题的WWO算法 基本WWO算法: 基于浅水波理论的启发式算法 第一代浅水波模型(1960s) 第二代浅水波模型(1970s) 第三代浅水波模型(1980s-1990s) 波-波交互 输入 耗散 Zheng YJ (2015) Water wave optimization: A new nature- inspired metaheuristic, Comput Oper Res 55: 1-11 doi:10.1016/j.cor.2014.10.008 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 求解问题的WWO算法 基本WWO算法: 基于浅水波理论的启发式算法 第一代浅水波模型(1960s) 第二代浅水波模型(1970s) 第三代浅水波模型(1980s-1990s) 直线传播 量密度 增长和消退 Zheng YJ (2015) Water wave optimization: A new nature- inspired metaheuristic, Comput Oper Res 55: 1-11 doi:10.1016/j.cor.2014.10.008 曲率传播 折射 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 求解问题的WWO算法 基本WWO算法: 基于浅水波理论的启发式算法 解空间  海床 解  波浪 解的适应度  波的能量(高度) Zheng YJ (2015) Water wave optimization: A new nature- inspired metaheuristic, Comput Oper Res 55: 1-11 doi:10.1016/j.cor.2014.10.008 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 求解问题的WWO算法 基本WWO算法: 基于浅水波理论的启发式算法 Propagation (传播) Zheng YJ (2015) Water wave optimization: A new nature- inspired metaheuristic, Comput Oper Res 55: 1-11 doi:10.1016/j.cor.2014.10.008 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 求解问题的WWO算法 基本WWO算法: 基于浅水波理论的启发式算法 Propagation (传播) Refraction (折射) Zheng YJ (2015) Water wave optimization: A new nature- inspired metaheuristic, Comput Oper Res 55: 1-11 doi:10.1016/j.cor.2014.10.008 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 求解问题的WWO算法 基本WWO算法: 基于浅水波理论的启发式算法 Propagation (传播) Refraction (折射) Break (碎浪) Zheng YJ (2015) Water wave optimization: A new nature- inspired metaheuristic, Comput Oper Res 55: 1-11 doi:10.1016/j.cor.2014.10.008 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 求解问题的WWO算法 基本WWO算法: 基于浅水波理论的启发式算法 Propagation (传播): 平衡全局探索与局部开发 Refraction (折射): 避免陷入局部最优, 提高种群多样性 Break (碎浪): 强化局部搜索 Zheng YJ (2015) Water wave optimization: A new nature- inspired metaheuristic, Comput Oper Res 55: 1-11 doi:10.1016/j.cor.2014.10.008 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云

求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 邻域: 1 0 CSBSE 2015, Nanjing, China 求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 邻域: 1 0 011000101 011010101 郑宇军, 张蓓, 薛锦云

求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 邻域: 1 0 波长为λ: 执行λ步邻域操作 CSBSE 2015, Nanjing, China 求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 邻域: 1 0 波长为λ: 执行λ步邻域操作 011000101 011010101 011010100 011010110 郑宇军, 张蓓, 薛锦云

求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 邻域: 1 0 波长为λ: 执行λ步邻域操作 CSBSE 2015, Nanjing, China 求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 邻域: 1 0 波长为λ: 执行λ步邻域操作 选取n/λ个λ步邻域解中的最优一个 011000101 011010101 011010100 011010110 郑宇军, 张蓓, 薛锦云

求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 CSBSE 2015, Nanjing, China 求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 Refraction (折射): 避免陷入局部最优, 提高种群多样性 X向当前最优解X*学习 X*中为1而X中为0的类集 X*中为0而X中为1的类集 郑宇军, 张蓓, 薛锦云

求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 CSBSE 2015, Nanjing, China 求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 Refraction (折射): 避免陷入局部最优, 提高种群多样性 Break (碎浪): 强化局部搜索 在X*的所有一步和二步邻域解中进行搜索 郑宇军, 张蓓, 薛锦云

求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 CSBSE 2015, Nanjing, China 求解问题的WWO算法 Propagation (传播): 平衡全局探索与局部开发 Refraction (折射): 避免陷入局部最优, 提高种群多样性 Break (碎浪): 强化局部搜索 约束处理 违反工作量约束的程度 违反费用约束的程度 郑宇军, 张蓓, 薛锦云

计算实验 问题实例: 一个军事指挥软件系统 1168/1364个类型 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云

计算实验 比较算法 GA (Tan et al. 2008) Binary-PSO (Kennedy & Eberhart 1997) CSBSE 2015, Nanjing, China 计算实验 比较算法 GA (Tan et al. 2008) Binary-PSO (Kennedy & Eberhart 1997) IBPSO (Yuan et al. 2009) Binary-DE (Pampara et al. 2006) 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China 计算实验 实验结果 郑宇军, 张蓓, 薛锦云

结论与展望 贡献 提出了一个在软件系统中选取关键部件进行形式化开 发的 优化问题模型 提出了一个求解该问题的离散WWO算法 CSBSE 2015, Nanjing, China 结论与展望 贡献 提出了一个在软件系统中选取关键部件进行形式化开 发的 优化问题模型 提出了一个求解该问题的离散WWO算法 算法在给定测试实例上优于一组流行启发式算法 郑宇军, 张蓓, 薛锦云

结论与展望 展望 考虑不同程度的形式化方法应用：形式化需求导出、 规格说明、验证、代码推导…… CSBSE 2015, Nanjing, China 结论与展望 展望 考虑不同程度的形式化方法应用：形式化需求导出、 规格说明、验证、代码推导…… 考虑系统不同部分及执行不同任务的不同可靠性要求 融合其它软计算方法（神经网络、模糊推理……）进 行更精确的开发成本估算 郑宇军, 张蓓, 薛锦云

CSBSE 2015, Nanjing, China THANKS