高可信软件工程
课程编码：085400M05007T
英文名称：Trustworthy Software Engineering
课时：39
学分：2.00
课程属性：专业普及课
主讲教师：张健等
教学目的要求
本课程是为电子信息专业研究生开设的专业普及课，其目的是使学生掌握高可信软件质量保障的基本原理和方法。通过课程教学，使学生掌握常用的软件规约与建模方法、测试与分析方法以及形式验证技术，并能够使用相关软件测试、分析与验证工具进行实践。
预修课程
程序设计语言、离散数学、软件工程
大纲内容
第一章 绪论 3.0学时
第1节 高可信软件概述
第2节 课程组织及要求
第二章 软件规约与建模 3.0学时
第1节 软件规约
第2节 系统建模
第三章 新型程序设计范式 6.0学时
第1节 并发编程原理
第2节 同步机制及其应用
第四章 软件测试与分析 12.0学时
第1节 黑盒测试
第2节 白盒测试
第3节 符号执行
第4节 程序分析
第五章 新型软件测试与分析 9.0学时
第1节 并发测试
第2节 深度学习测试
第3节 智能合约分析
第六章 形式验证技术简介 6.0学时
第1节 定理证明
第2节 模型检测
参考书
1、
软件建模与设计（ Software Modeling & Design），软件测试基础教程（Foundations of Software Testing），Principles of Program Analysis，多处理器编程的艺术（英文版）
Hassan Gomaa著，彭鑫，吴毅坚，赵文耘等译，Aditya P. Mathur著，王峰等译，Flemming Nielson et al.，Maurice Herlihy，Nir Shavit著
2014，2011，2005，2008
机械工业出版社，机械工业出版社，Springer，机械工业出版社
课程教师信息
张健，中国科学院软件研究所研究员。主要研究兴趣包括：自动推理、约束求解、软件测试与分析。曾先后获得中创软件人才奖、国家杰出青年科学基金、国务院政府特殊津贴，指导的多名研究生获得了中国科学院院长奖、中国计算机学会优秀博士论文提名奖等荣誉。目前担任《计算机学报》，J. of Computer Sci. and Tech.，Frontiers of CS，IEEE Trans. on Reliability，《中国科学：信息科学》，《计算机科学与探索》编委。
朱雪阳，中国科学院软件研究所副研究员。主要研究方向为：嵌入式系统设计、形式化方法、智能合约分析与验证等。
吴鹏，中国科学院软件研究所副研究员、硕士生导师。主要研究兴趣包括：并发理论、并发程序的形式化验证和测试、机器学习等。曾主持、参与多项国家自然科学基金项目、国家重点研发计划项目；在相关领域重要国际会议ATVA、ICECCS和期刊IEEE Transactions on Software Engineering、Information and Software Technology等发表多篇学术论文；担任中国科学院大学《多处理器系统编程》、《软件测试与安全分析》和《并发数据结构与多核编程》等课程的主讲教师。