形式化方法
课程编码：180086081202M3001H
英文名称：Formal Methods
课时：40
学分：2.00
课程属性：专业课
主讲教师：朱雪阳等
教学目的要求
本课程讲授和讨论形式化方法研究领域的基础理论和关键技术。主要内容有软件系统抽象模型、时序逻辑、软件系统抽象模型的时序逻辑性质的分析与验证方法等。通过本课程的学习，学生有望了解形式化方法的基本思想和软件系统分析与验证方法方面的研究成果，掌握基础理论和关键技术，培养学生形式化方法方面的研究能力。
预修课程
数理逻辑与程序理论、形式语言与自动机理论
大纲内容
第一章 形式化方法概述
第1节 形式化方法概述 3学时 朱雪阳
第二章 交互式定理证明
第1节 Coq简介 3学时 施晓牧
第2节 函数式编程基础 3学时 施晓牧
第3节 命题与证明 3学时 施晓牧
第4节 函数与证明 3学时 施晓牧
第5节 归纳谓词与依赖类型 3学时 施晓牧
第三章 形式建模基础
第1节 迁移系统 6学时 朱雪阳
第2节 线性时序逻辑 2学时 朱雪阳
第四章 建模与验证实践
第1节 基于TLA+的建模与验证 9学时 朱雪阳
第2节 基于UPPAAL的实时系统建模与验证 3学时 朱雪阳
第五章 形式化方法应用实例
第1节 形式化方法实例 2学时 朱雪阳
参考书
1、
The Foundation of Program Verification
J. Loeckx and K. Sieber
1984
Wiley & Sons Ltd
2、
Model Checking
E. M. Clarke, O. Grumberg and D. Peled
1999
The MIT Press
3、
Software Reliability Methods
D. A. Peled
2001
Springer-Verlag
4、
Principles of Model Checking
C. Baier and J.-P. Katoen
2008
MIT Press
5、
Verification of Sequential and Concurrent Programs
K. R. Apt, F. S. de Boer and E.-R. Olderog
2009
Springer-Verlag
课程教师信息
朱雪阳，中国科学院软件研究所副研究员、硕士生导师。主要研究方向为：嵌入式系统设计、形式化方法、智能合约分析与验证等。曾主持、参与多项国家自然科学基金项目、国家重点研发计划项目；在相关领域重要国际会议和期刊I发表多篇学术论文；担任中国科学院大学《高可信软件工程》等课程的主讲教师。个人学术主页：http://lcs.ios.ac.cn/~zxy/
施晓牧，中国科学院软件研究所高级工程师、硕士生导师。主要研究方向为：使用定理证明器对计算机软硬件基础设施的正确性与安全性进行形式验证，包括编译器、密码程序、SMT求解器等。主持国家自然科学基金青年基金、广东省自然科学基金面上项目、深圳市自然科学基金面上项目各一项；论文发表于CAV、CCS、ASE等国际会议。