形式化方法
(基于B方法的软件开发,2010年春季)

通知:(请相互转告)

请各位同学把最后作业开发的系统和报告打包,最迟7月2日发给我
北京大学数学学院信息科学系“软件形式化方法”研究生课。

本课程是软件形式化方法的基础课程,主要讨论基于 B 方法的形式化规范、验证和精化。

课程信息:周二下午7-9节(2:40~5:30);文史楼204教室。

课程动态进展 (随课程进展更新)
课程通知(更新: 2015-11-28 讲义下载(更新: 2015-11-28 课程作业页(更新: 2015-11-28
课程参考书和材料
本课程以《B方法, Jean-Raymond Abrial》作为主要参考书。中译本由电子工业出版社2004

课程中使用的工具系统和文档(来自Clearsy公司,放在这里只为课程学习):

这里有一个 B 方法所用数学符号的 Latex 包
以前形式化方法课程(Z语言)页面链接
下面是有关B方法的一些资源网址:
其他参考书:
  • 缪怀扣,软件工程语言-Z,上海科学技术文献出版社,1999
  • Jim Woodcock and Jim Davies, Using Z, Specification, Refinement, and Proof, 下载该书的PDF文件和其中参考材料
  • Carroll Morgan, Programming From Specification, Printice Hall, 1998 (中译本:从规范出发的程序设计,裘宗燕译,中信出版社&机械工业出版社,2002)
部分书籍可以从网上书店找到。
阅读材料
JIM WOODCOCK, PETER GORM LARSEN, JUAN BICARREGUI, JOHN FITZGERALD,
Formal Methods: Practice and Experience, Computing Survey, 2009, ACM

Jean-Raymond Abrial,
《工业开发中的形式化方法:成就,问题和未来》, 2006年国际软件工程大会特邀报告(中文翻译版)

Jean-Raymond Abrial,
Faultless Systems: Yes We Can! Computer, 2009.9, IEEE CS

D.L. Parnas,
Really Rethinking 'Formal Methods', Computer, 2009.12, IEEE CS

相关资料
软件形式化的文献汇编(收集中。更新: 1970-01-01
其他信息汇编(北京大学图书馆的有关图书目录,有关重要国际杂志等)。
十大IT灾难
Can Software Kill You?
Outsmarted: Victoria pays the price
本页及相关页面(除另声明者外)由裘宗燕创建维护,可自由用于各种学习活动。 其他使用需得到作者许可。

访问数(2010.02开始):38531 最后更新: 2015-11-28