课程介绍-软件工程中的形式化方法(全英)
课程名称：软件工程中的形式化方法(全英)
课程类别：专业选修课
学分：2
先修课程：Discrete Mathematics
考核方式：课程论文
授课老师：陈清亮
本课程是计算机科学本科学生的一门选修的前沿基础理论课。从广义上讲，形式化方法是借助数学的方法来解决软件工程领域的问题，主要包括建立精确的数学模型以及对模型的分析活动。狭义的讲，形式化方法是运用形式化语言，进行形式化的规格描述、模型推理和验证的方法。就形式化建模而言，形式化表示必须包含一组定义其语法语义的形式化规则。这些规则可用于分析给定的表达式是否符合语法规定，或证明该表达式具有某种性质。具体来说，软件形式化方法包括以下几个主要教学内容： (1) 基础概念：复合、抽象、重用模型、数学理论组合、数据结构及算法。需要对如何复合方法、复合规格、复合模型、复合理论、复合证明等进一步的理解；需要开发出将整体特性分解为易于验证的局部特性的有效方法；实际系统在规格和验证之前都要进行某种程度上的抽象，需要研究出评判抽象层次合理与否的方法；重用不仅可以提高开发效率，而且可以提高软件的可靠性，应当研究可重用模型和理论；许多安全关键反应式系统是数字和模拟混合的，需要连续和离散两个范畴内数学基础支撑的混杂系统理论和技术支撑；大规模、复杂软件中搜索空间是巨大的，需要研究出新的数据结构和算法。在课程的教学过程中，要通过各个教学环节逐步培养学生的抽象思维能力、逻辑推理能力、建模与实践工程能力以及自学能力。
教材及主要参考书目
1. Michael Huth and Mark Ryan Title: Logic in Computer Science: Modelling and Reasoning about Systems Publisher: Cambridge Univ. Press Year: June 2004 (2nd edition)
2. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled Title: Model Checking Publisher: MIT Press Year: January 2000
