Tuesday, May 30, 2006

I change the template

I find the font size of the previous template is too big. So I selected this one. If anybody is not satisfied with this, please feel free to choose another one.

Monday, May 29, 2006

A Chinese Tutorial of RAISE Language

As I have posted in the email, there are some materials on the homepage of RAISE. Since this blog does not support the uploading of attachment, the link is given in the following:

A Tutorial on Raise in Chinese

Introduction of Dines Bjorner and the books Software Engineering (Volume 1-3)

This Introduction is done by Bochao LIU, which can be used as a first-hand document to contact with Chinese publishers. The following text is in Chinese.

--------------------------------------------------------------------------------------

1. Dines 先生简介

《软件工程》三卷书的作者Dines Bjorner是世界著名的丹麦计算机科 学家。他主要研究形式化方法。Dines先生与Cliff Jones等创建了著 名的维也纳开发模式。后来他参与创建了RAISE(工业软件开发的严格 方法)的形式化方法以及相关的工具支持。

Bjorner先生是丹麦科技大学的教授。90年代他负责在澳门创建了联 合国大学软件科技国际学院, 担任第一届校长。 他研究的巨著《软件 工程》三卷于2005/6年出版。 为了支持维也纳开发模式, Bjorner创 建了维也纳开发模式-欧洲组织, 后来演变成了今天的形式化方法 -欧洲组织。2003年他发起成立了形式化技术工业联合会。

Dines Bjorner先生于1994年获得了冯诺依曼奖章。他是IEEE和ACM的院士(fellow)。

目前他日本北陆先端科学技术大学院大学(Japan Advanced Institute of Science and Technology)做客座教授。Dines教授非 常希望我们在北陆大学的中国研究人员能够翻译他的这部著作。于是 我们组建了翻译团队。Dines先生给我们介绍了出版《软件工程》德国 施普林格(Sringer)出版公司编辑Ronan Nugent先生。经过协商,他 建议我们委托中国的出版公司和施普林格联系合作事宜。


2. 《软件工程》介绍

这三本主要讲述了如何用形式化方法指导软件工程的开发模式。 在 软件的面向领域分析, 需求分析, 软件设计,软件开发各个阶段, 如果都能够采用这种形式化的软件开发模式,将能够极大的保证 软 件开发的正确性,有效性。

第一卷 抽象与建模

该卷介绍了抽象与建模基本的原理和技术。

首先该卷给出了一个可靠和基本的离散数学的介绍,包括数字,集 合,笛卡尔,类型,函数,lambda演算, 代数和数理逻辑。

然后该卷讲授和培养读者基本的面向属性与面向模型规范的基本原理 和技术。

一些其他的规约语言,比如B,VDM-SL,Z都具有面向模型的概念。 本书通过RAISE的规约语言RSL来讲解这个概念。

最后该卷介绍了关于函数式,命令式,并行式的规约编程。 并行式规约编程基于CSP的使用: 霍尔(Hoare)的通信顺序进程(Communicating Sequential Processes)。


第二卷 系统与语言的规约

该卷介绍了描述系统与语言规约的基本原理和技术。

首先该卷讲授和培养读者一些高级的原理和技术: 分层与组合, 指 称与计算,构型:环境与状态的抽象与建模。

然后该卷讲授和培养读者符号学建模的基本原理和技术: 语用,语 义,系统和语言的语法。

其中重要的一部分给出了空间和简单时态现象建模的基本原理和技术 的介绍。

该卷的主要的章节用于介绍一些专门的主题,比如模块(包括UML的类 图);Petri网;活动序列图;状态图; 时态逻辑,包括时段演算。这

一部分体现了格言:我们 "UML"化形式化技术。 这样读者能够在坚 实,精确,形式化的基础上(可信的)专业的使用这些方法。同样的,在

UML中这些方法也是其主要的组成部分。

最后该卷给出了开发函数式,命令式以及并行编程语言的可靠和有效 的解释器和编译器的基本原理和技术。

第二卷要求读者已经学习过第一卷。

第三卷 领域,需求与软件设计

该卷介绍了整体软件开发的基本原理和技巧:从领域,经过需求,直到 软件设计。

基于下面的格言,该卷倡导一种全新的软件工程的方式:在需求被形 式化之前,人们必须理解应用领域。

因此该卷采取结构: 从(1)领域描述的原理和技术,经过(2)从领域模型导 出需求规则的原理和技术,直到(3) 细化需求到软件设计的原理和技

术: 体系结构和组件设计。

在介绍领域和需求工程的过程中强调了"什么构成了合适的领域描述"和" 需求规则",以及"如何获取和分析领域知识","需求期望"和"如何检查 和验证领域和需求模型"。

该卷的结构组织面向两类不同读者: 那些明确标出结构,注重于非形 式化的部分,主要面向在第二学期上软件工程课程的本科生和软件工 程领域的大学教师;整卷书则面向高年级学生, 教师以及研究人员。

这是做为教科书使用的一个新特点。

第三卷的简单版本对读者没有要求。 完整版的第三卷需要读者学习 过第二卷。


为了方便教学,该书提供了幻灯片课件
第一卷: 71个主题,1790页
第二卷: 95个主题,1531页
第三卷: 83个主题,2563页

三卷书所有的章节平均都有5个练习。答案通过向作者提出请 求的方 式给与提供。

3. 章节目录
第一卷 抽象与建模

第一部分 首章

1. 介绍

第二部分 离散数学

2. 数字
3. 集合
4. 笛卡尔
5. 类型
6. 函数
7. Lambda演算
8. 代数
9. 数理逻辑

第三部分 简单RSL

10. RSL的原子类型和值
11. RSL的函数定义
12. 面向属性 与 面向模型的抽象
13. RSL的集合
14. RSL的笛卡儿
15. RSL的列表
16. RSL的映射
17. RSL的高阶函数

第四部分 规约类型

18. RSL的类型

第五部分 规约编程

19. 应用式规约编程
20. 命令式规约编程
23. 并发式规约编程

第六部分 其余部分

24. 其余

第七部分 附录

A. 练习
B. 术语表
C. 索引

参考文献


第二卷 系统与语言规约

第一部分 首章

1. 介绍

第二部分 规约刻面

2. 分层与组合
3. 指称与计算
4. 构型: 环境与状态

第三部分 关键领域与计算刻面

5. 时间,空间 与 时间/空间

第四部分 语言学

6. 语用
7. 语义
8. 语法
9. 符号

第五部分 高级规约技术

10. 模块化
11. 自动机和机器

第六部分 并发与时态

12. Petri网
13. 消息与活动序列图
14. 状态图
15. 时间的量化模型

第七部分 解释器与编译器定义

16. SAL 简单应用语言
17. SIL 简单命令语言
18. SMIL 简单模块,命令语言
19. SPIL 简单并行,命令语言

第八部分 尾章

20. 尾章

第九部分 附录

21. 命名规约
22. 索引

参考文献


第三卷 领域, 需求与软件设计

第一部分 首章

1. 三联式
2. 文档

第二部分 概念框架

3. 方法和方法论
4. 模型和建模

第三部分 描述:理论与实践

5. 现象和概念
6. 下定义与定义
7. Jackson的描述原理

第四部分 领域工程

8. 领域工程概述
9. 领域参与者
10. 领域属性
11. 领域刻面
12. 领域获取
13. 领域分析与概念形成
14. 领域验证与检查
15. 领域理论相关
16. 领域工程过程模型

第五部分 需求工程

17. 需求工程概述
18. 需求参与者
19. 需求刻面
20. 需求获取
21. 需求分析与概念形成
22. 需求验证与建成
23. 需求可满足性与可行性
24. 需求工程过程模型

第六部分 计算系统设计

25. 硬件/软件 协同设计
26. 软件体系结构设计
27. 构建设计案例学习
28. 领域特定体系结构
29. 其它: 编码及相关
30. 计算系统设计过程模型

第七部分 尾章

31. 三联式开发过程模型
32. 尾章

第八部分 附录

A. RSL教程
B. 术语表
C. 索引

------------------------------------------------------------------------------------------