形式化方法是建立在严格数学基础上、具有精确数学语义的开发方法。从广义角度,形式化方法是软件开发过程中分析、设计及实现的系统工程方法。狭义地,形式化方法是软件规格和验证的方法。本书对软件开发的形式化方法进行了介绍和讨论,内容涵盖了SE2004的SEEK中关于“软件的形式化方法”的知识点,主要包括:有限状态机、Statecharts、Petri网、通信顺序进程、通信系统演算、一阶逻辑、程序正确性证明、时态逻辑、模型检验、Z、VDM、Larch等。
本书可作为计算机、软件工程等专业高年级本科生或研究生的教学用书,也可供相关领域的研究人员和工程技术人员参考。
- 第1章 软件及其开发概述
- 1.1 软件开发的历史
- 1.2 软件危机
- 1.3 软件工程
- 1.4 形式化方法
- 习题
- 第2章 有限状态机及其扩展
- 2.1 有限状态机
- 2.1.1 基本概念
- 2.1.2 有限状态机的复合
- 2.1.3 生产者-消费者系统
- 2.2 Statecharts
- 2.2.1 Statecharts中的状态
- 2.2.2 Statecharts中的迁移
- 2.2.3 电梯控制系统
- 习题
- 第3章 Petri网
- 3.1 位置/迁移Petri网
- 3.1.1 基本定义
- 3.1.2 特殊Petri网
- 3.1.3 Petri网的性质
- 3.1.4 Petri网的分析
- 3.1.5 Petri网规格的例
- 3.2 高级Petri网
- 3.2.1 谓词/迁移Petri网
- 3.2.2 有色Petri网
- 3.2.3 计时Petri网
- 习题
- 第4章 进程代数
- 4.1 通信顺序进程
- 4.1.1 进程及其表示
- 4.1.2 事件迹及其操作
- 4.1.3 进程的复合操作
- 4.1.4 进程的模型
- 4.1.5 进程之间的通信
- 4.1.6 CSP规格的例
- 4.2 通信系统演算
- 4.2.1 CCS的基本概念
- 4.2.2 AB协议的规格
- 习题
- 第5章 一阶逻辑
- 5.1 命题逻辑
- 5.1.1 命题与联结词
- 5.1.2 命题公式
- 5.1.3 命题逻辑演算
- 5.2 谓词逻辑
- 5.2.1 谓词公式
- 5.2.2 谓词逻辑演算
- 5.2.3 谓词逻辑的应用
- 5.3 程序正确性证明
- 5.3.1 归纳断言方法
- 5.3.2 公理化方法
- 5.3.3 良序集方法
- 5.3.4 计数器方法
- 5.3.5 最弱前置谓词方法
- 习题
- 第6章 时态逻辑
- 6.1 模态逻辑
- 6.2 线性时态逻辑
- 6.2.1 命题线性时态逻辑
- 6.2.2 一阶线性时态逻辑
- 6.3 计算树逻辑
- 6.4 模型检验
- 习题
- 第7章 Z
- 7.1 概述
- 7.2 表示抽象
- 7.2.1 集合、关系及函数
- 7.2.2 序列和包
- 7.2.3 自由类型
- 7.2.4 模式
- 7.3 操作抽象
- 7.4 Z规格的例
- 习题
- 第8章 VDM
- 8.1 概述
- 8.2 表示抽象
- 8.2.1 基本运算和基本类型
- 8.2.2 集合与序列
- 8.2.3 映射与函数
- 8.2.4 复合类型
- 8.2.5 状态和不变量
- 8.3 操作抽象
- 8.4 VDM规格的例
- 8.4.1 家庭供暖系统
- 8.4.2 计算机网络问题
- 习题
- 第9章 Larch
- 9.1 概述
- 9.2 Larch共享语言
- 9.3 Larch/C接口语言
- 9.4 Larch规格的例
- 习题
- 参考文献
