形式化方法（Formal Methods：Modeling in Event-B）

Professor Jean-Raymond Abrial

上课时间 周一3/4节（10:10-12:00，授课）
周二10/11节（18:40-20:30，课堂实践）
周三5/6节（13:00-14:50，授课）
上课教室 理科一号楼1556/1560教室（第一次在理科楼一号楼 1114 教室）
教学材料>>>>>>>>>> (Course Materials)   有关材料将随着课程进展逐步提供。

课程简介

本课程关注“正确”和“可靠”的计算机软件（及硬件）系统的开发，介绍软件（系统）的形式化开发技术和过程。课中将以 Event-B 方法和 Rodin 平台作为工具，阐释系统的分析、严格描述、建模、验证、精化等重要工作如何在形式化和数学化的框架里进行。

本课程将展示：

  • 软件（及其他系统）如何能构造即正确（correct by construction）
  • 如何用 Event-B 进行对各种系统的建模和形式化推理
  • 如何在支持 Event-B 的 Rodin 平台中完成这些工作
课程中将讨论许多建模和开发示例，开展课题实践练习及指导。通过此课程的所获可能包括：
  • 学习如何写出严格的系统需求文档（requirement document）
  • 理解建模和程序设计之间的关系
  • 理解抽象和精化（abstraction/refinement）在软件开发工作中的意义和作用
  • 掌握对系统和程序进行推理的数学技术
  • 取得将证明作为构造程序的重要方法的工作经验
  • 使用 Event-B 和 Rodin 的经验
在航空航天、高速铁路、核电、大型船舶等关键性设备和系统，以及金融、社会管理、国防等各种重要领域越来越依靠计算机系统的今天，采用传统的个人技巧加调试的方法开发的系统，越来越不能满足社会对具有高可靠性、高安全性的系统的需要。本课程可能帮助你理解今天和未来的重要计算机系统的开发领域和技术。
 课程计划 (Course Plan) 　
 17 lectures:
   September: 5, 7, 14, 19, 21, 26, 28
   October: 10, 12, 17, 19, 24, 26, 31
   November: 2, 7, 9		  9 Practices:
   September: 6, 13, 20, 27
   October: 11, 18, 25
   November: 1, 8
  1. Introduction
    (September 5, 7)
  2. Cars on a Bridge
    (September 14, 19, 21)
  3. Mechanical Press
    (September 26, 28)
  4. File Transfer Protocol
    (October 10)
  5. Math Refresher
    (October 12, 17)
  6. Mobile Phone Routing
    (October 19)
  7. Hardware Development
    (October 24, 26)
  8. Access Control System
    (October 31, November 2)
  9. Hypervisor Development（微软正在进行的一个重要项目）
    (November 7, 9)
  1. Writing a Requirement Document
    (September 6)
  2. Introducing the Rodin Platform
    (September 13)
  3. Developing a small Motor Controller
    (September 20)
  4. Practicing Interactive Proofs
    (September 27, October 11, 18)
  5. Another Formal Development
    (October 25)
  6. Developing a Business Protocol
    (November 1, 8)
2011.8