Visiting Professor: Jean-Raymond Abrial

Jean-Raymond Abrial

Visiting Professor (2011.8.16-11.15)

国际著名软件和软件理论专家，Z 语言和 B 方法的创建者，软件形式化开发领域的最主要奠基人之一

参与和指导了欧洲许多重要的关键性软件开发项目

其开发的 B 软件开发方法被欧洲等地区的许多重要企业和部门（如欧洲航天局、西门子、阿尔斯通等）用于轨道交通、高铁、航空、电站等重要领域的信号、控制、调度、自动驾驶等各种关键性系统的建模、验证和系统开发

近年领导和参与 B 方法后继的 Event-B 开发和应用的欧共体项目，其参与开发的 Event-B 公开免费工具 Rodin 已被全世界软件/硬件和其他领域的许多理论和实际工作者使用

办公室：理科一号楼1281 Tel: 62759530 电子邮件：jrabrial AT math.pku.edu.cn

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

课号：00113140

J-R Abrial 教授来访期间为研究生和高年级本科生开设软件形式化方法课程（2011.9.5 - 11.9），内容为基于 Event-B 的软件（和硬件）系统设计、建模和形式化验证

课程页 (Course Page)>>>>>>>（课程介绍、详细计划和相关材料）

通知和下次阅读建议

本课程中使用的 Event-B 工具 Ridin 平台系统及文档下载>>>>>>>> (Rodin Plateform)

Event-B Web Site, with Rodin and Docs links

课程助理：刘海洋　　　联系人：裘宗燕

本课程面向数学、信息等学院研究生和高年级本科生。如果你想了解并掌握

已在国际上成功用于开发许多关键性软件系统的新技术
对软件系统（和一般的基于计算机的系统）的深入分析和建模的严格技术
基于严格的数学和证明的软件（硬件）系统建模和开发过程

本课程适合你的需要。欢迎选课（请到数学学院/研究生课程中选课，接受本科生）

本课程将采用课题讲解和实践相结合的方式。每位上课同学需要带一台笔记本计算机。Abrial 教授将讲授系统的形式化建模和验证技术，并基于 Event-B 给出许多软件（及硬件）系统开发实例。课程中将深入细致地讲解如何严格地分析实际问题，描述系统需求；如何用 Event-B 做系统建模，严格证明所建立的系统模型的正确性；等等。参与本课程的学习，可能帮助人更深入地理解计算机和软件系统，软件开发过程及其问题，并为参与未来的关键性软件的开发打下很好的基础。