形式化方法  081202M05001H

学期:2020—2021学年(春)第二学期 | 课程属性:专业普及课 | 任课教师:张文辉
授课时间: 星期四,第5、6、7 节
授课地点: 教一楼125
授课周次: 1、2、3、4、5、6、7、8、9、10、11、12、13、14、15
课程编号: 081202M05001H 课时: 40 学分: 2.00
课程属性: 专业普及课 主讲教师:张文辉 助教:
英文名称: Formal Methods 召集人:

教学目的、要求

教学目的和要求:
    本课程为计算机软件与理论学科研究生的专业普及课。本课程讲授和讨论形式化方法前沿研究领域的主要思想和关键技术。主要内容有软件系统抽象模型、程序与时序逻辑、软件系统模型的分析与验证等。
    通过本课程的学习,希望学生能了解形式化方法的前沿研究领域,了解软件系统分析与验证方法方面的最新研究成果,掌握基本思想和关键技术,培养学生形式化方法方面的研究能力。

预修课程

数理逻辑与程序理论、形式语言与自动机理论

教 材

主要内容

第一章  绪论
1.1 软件正确性
1.2 软件系统行为

第二章  程序与软件系统模型
2.1  基于谓词的系统模型
2.2  基于状态的系统模型

第三章  程序与时序逻辑
3.1  线性时序逻辑
3.2  分支时序逻辑

第四章  程序的推理
4.1  卫式迁移模型的推理
4.2  流程图与结构化模型的推理

第五章  软件系统模型的模型检测
5.1  显式状态模型检测
5.2  符号与限界模型检测

参考文献

主要参考书:

J. Loeckx and K. Sieber. 
The Foundation of Program Verification. John Wiley & Sons Ltd., 1984.

E. M. Clarke, O. Grumberg, D. Peled. 
Model Checking. The MIT Press. 1999.

D. A. Peled.
Software Reliability Methods. Springer-Verlag. 2001.

C. Baier and J.-P. Katoen. 
Principles of Model Checking. MIT Press. 2008.

K. R. Apt, F. S. de Boer, E.-R. Olderog. 
Verification of Sequential and Concurrent Programs. Springer-Verlag. 2009.