软件形式化开发关键部件的选取gist.ppt

计算实验 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 实验结果 结论与展望 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 贡献 提出了一个在软件系统中选取关键部件进行形式化开发的 优化问题模型 提出了一个求解该问题的离散WWO算法 算法在给定测试实例上优于一组流行启发式算法 结论与展望 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 展望 考虑不同程度的形式化方法应用：形式化需求导出、规格说明、验证、代码推导…… 考虑系统不同部分及执行不同任务的不同可靠性要求 融合其它软计算方法（神经网络、模糊推理……）进行更精确的开发成本估算 THANKS CSBSE 2015, Nanjing, China 软件形式化开发关键部件的选取一种基于水波优化的方法 郑宇军, 张蓓, 薛锦云 提 纲 01 02 03 引言 问题模型 优化算法 04 计算实验 引言 形式化方法（Formal Methods) 建立在严格数学模型上、具有精确数学语义的软件系统开发方法 能够从根本上提高软件系统的质量与可靠性 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 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) 对开发人员的高要求 高昂的开发代价 较低的开发效率 其它局限性：非形式化的需求，COTS集成…… 不适合大型软件系统的全程开发 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 引言 在大型软件系统开发中部分引入形式化方法 对部分规约进行形式化验证 (Easterbrook Callahan 1998) 指导性原则 (Russo 2013) 基于软件度量的选择 (Zheng et al. 2006) CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 Whether, Where, When, and to Which degree 引言 在大型软件系统开发中部分引入形式化方法 建立优化问题模型: 0-1 programming 基于元启发的有哪些信誉好的足球投注网站方法: Water wave optimization (WWO) CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 Whether, Where, When, and to Which degree 决策变量 软件总体结构: 所有类型 候选集: A\AE\AC\AU 目标子集: 用于(完整)形式化开发的类集 问题模型 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 问题模型 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 问题模型 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 问题模型 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 问题模型 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 目标函数: 系统可靠度 形式化开发的类的可靠度: 1 非形式化开发的类的可靠度 类结构的复合 问题模型 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 约束条件 总工作量约束 总费用约束 问题模型 CSBSE 2015, Nanjing, China 郑宇军, 张蓓, 薛锦云 形式化开发的类的子集: CF(X) 非形式化开发的类的子集: CN(X) 基本WWO算法: 基于浅水波理论的启发式算