（4）“生产者与消费者”实例

消费者在进行“消费”动作后，状态由C1转变为 C2；而在“读”动作后，状态由C2恢复为C1。 如果缓存器是满的，那么生产者进程必须等待， 直到消费者进程从缓存器中取出一个消息，使缓 存器产生一个消息空位。同样，如果缓存器是空 的，那么消费者进程就必须等待，直到生产者进 程产生一个消息并把所产生的消息写入缓存器中。 缓存器在进行“读”动作后，缓存器大小减“1”， 而在“写”动作后，缓存器大小加“1”。
q1 a c q0 c q3 b q2 a
图7.1 有限状态机
（4）“生产者与消费者”实例

“生产者－消费者”系统中，包含一个生产 者和一个消费者。生产者进程产生消息， 并把产生的消息写入一个能容纳两个消息 的缓存区中。生产者在进行“生产”动作 后，状态由P1转变为P2；而在“写”动作 后，状态由P2恢复为P1。消费者进程能读 取消息，并把消息从缓存器中取走。
（2）节约成本的需要

有证据显示，形式方法的使用减少了项目 成本。例如，IBM的大型CICS事务处理项 目的独立审核表明，9％的成本节约要归功 于形式方法的使用。对T800型变换计算机 的Inmos浮点单元的独立审核也证明，形 式方法的使用估计可以减少12个月的测试 时间。
（3）形式方法和复用


有效的软件复用有助于提高软件开发的生 产率，这在应用软件的快速开发中具有特 殊的意义。 软件复用的思想是开发出可在未来项目中 使用的基本部件，这就要求部件具有高质 量和高可用性，而且部件的实际行为和使 用环境也要具备一个文档化的描述。
（3）形式方法和复用

形式方法在软件复用中也占有一席之地，因为它 可提高部件正确性的置信度，并对某个部件的行 为进行明确的形式描述。可以对部件进行广泛的 测试，以便为部件的正确性提供更高的置信度。 一个部件一般会在不同的环境中使用，而部件在 某种条件下能正常运转并不能保证它在未来也能 够成功运转，因为这个部件和其他部件或其他软 件之间可能存在着潜在的不良相互作用。因此， 我们希望部件的行为能够得到明确的规定和充分 的了解，并对部件的构成进行形式分析，以确保 风险最小化，并在最后得到高质量的软件。
（2）形式化定义


有限状态机FSM（Finite State Machine） 是一种基本的、简单的、重要的形式化技 术，它具有广泛的应用，可用于系统生命 期中从系统规格到系统设计的所有阶段。 直观地理解，有限状态机就是一个具有有 限状态的机器。 有限状态机是一个5元组M = (Q，∑，， q0，F)，其中：
（3）有限状态图的表示

有限状态机通常用图来表示，图中节点代 表状态，有向弧表示迁移关系，输入标注 在相应的关系弧旁边。图1显示了一个简单 的有限状态机，该状态机有4个状态q0、 q1、q2和q3，输入集合有3个元素a、b和 c。各个状态之间的转移关系可从图中清楚 地看出。
（3）有限状态图的表示
（5）经典案例及应用
（6）运输系统：巴黎地铁的自动火车保护 系统、英国铁路信号控制、以色列机 载航空电子软件。
软件开发中的形式化方法



1 2 3 4 5
形式化技术的产生和发展 软件开发中为什么使用形式化方法 形式化规格技术 形式化验证技术 总结
3 形式化规格技术



3.1 3.2 3.3 3.4 3.5
（2）形式化定义




① Q = {q0，q1，…，qn}是有限状态集合。在任一确 定的时刻，有限状态机只能处于一个确定的状态qi； ② ∑={1，2，…，m}是有限输入字符集合。在任一 确定的时刻，有限状态机只能接收一个确定的输入j； ③ ： Q Q是状态转移函数。在某一状态下，给定 输入后有限状态机将转入由状态迁移函数决定的一个新的 状态； ④ q0∈Q是初始状态，有限状态机由此状态开始接收输 入； ⑤ FQ是终结状态集合，有限状态机在达到终态后不再 接收输入。
3 形式化规格技术



3.1 3.2 3.3 3.4 3.5
形式化规格的定义 形式化规格的分类 操作类规格技术 描述类规格技术 双重类规格技术
3.3 操作类规格技术


操作类技术通过可执行模型描述系统，即 模型本身能够采用静态分析和执行模型得 到验证。 操作类技术侧重于系统行为的特性描述， 主要包括：有限状态机及其扩展技术和 Petri
形式化规格就是通过具有明确数学定义的 文法和语义的语言实现以上描述。
3 形式化规格技术



3.1 3.2 3.3 3.4 3.5
形式化规格的定义 形式化规格的分类 操作类规格技术 描述类规格技术 双重类规格技术
3.2 形式化规格的分类


形式化规格技术可分为：操作类、描述类和双重 类。 操作类技术基于状态和迁移，因其本质上可执行， 故具有直观和可视的特点；描述类技术基于数学 公理和概念，通过逻辑和代数给出系统的状态空 间，具有高度抽象、便于通过自动工具进行验证 的特点；双重类技术则兼有二者的特点，既能够 通过数学公理和概念高度抽象描述系统，又具有 状态和迁移的可执行特征。
（4）英国国防部的标准


这两个标准表明了英国国防部采用的安全 措施有多么严格，Brown在文献中提出： 在导弹系统表明其安全之前，我们必须假 设它处于危险状况中，没有危险错误存在 的证据并不等于没有危险。
（5）经典案例及应用

典型应用系统包括：IBM商用信息控制系统、 英国伦敦空中交通管理系统、空中交通防 碰撞系统TCAS等。

Praxis公司于1992年交付给英国民航局的信息显 示系统是伦敦机场新空中交通管理系统的一部分。 在该系统的需求分析阶段，形式化描述和非形式 结构化的需求概念相结合；在系统规格阶段，采 用了抽象的VDM模型；在设计阶段，抽象VDM细 化为更为具体的规格。项目开发的生产效率和采 用非形式化技术相当，甚至更好。同时，软件质 量得到了很大的提高，软件的故障率仅为0.75每 千行代码，大大低于采用非形式化技术所提供的 软件的故障率（约为2~20每千行代码）。
（5）经典案例及应用

除此之外还有：
（1）数据库：用于存储病人监护信息的HP 医用仪器实时数据库系统。 （2）核反应堆系统：核反应器安全系统、 核发电系统的切换装置。 （3）电信系统：AT&T的5ESS电话交换系 统、德国电信的电话业务系统。
（5）经典案例及应用
（4）保密系统：NATO控制指挥和控制系统 中的保密策略模型、Multinet网关系统 的数据安全传输、美国国家标准和技术 院的令牌访问控制系统。 （5）通信协议：协议规格、测试集的生成、 协议转换。
（5）经典案例及应用

牛津大学和Hursley实验室于20世纪80年 代合作将Z规格语言用于IBM商用信息控制 系统。IBM对整个开发进行的测试表明，Z 规格语言的应用明显地改善了产品质量、 大量减少了错误和早期诊断错误。IBM估计 使总体开发成本降低9％。这一成果获皇家 技术成就奖。
（5）经典案例及应用
形式化规格的定义 形式化规格的分类 操作类规格技术 描述类规格技术 双重类规格技术
3.1 形式化规格的定义

规格就是对系统或者对象及其期望的特性 或者行为进行的描述。规格所要描述的内 容包括：功能特性、行为特性、结构特性、 时间特性。功能特性侧重于系统的功能方 面，即做什么；行为特性侧重于系统的具 体行为演化，即如何做；结构特性侧重于 系统的组成，各个组成部分或者子系统间 的联系和复合；时间特性则是时间相关的 系统特性。
1 形式化技术的产生和发展

形式化技术成功的工业应用引起了人们的 普遍关注，可以预计，在未来的工业应用 系统开发中，形式化技术将会发挥越来越 重要的作用。
软件开发中的形式化方法



1 2 3 4 5
形式化技术的产生和发展 软件开发中为什么使用形式化方法 形式化规格技术 形式化验证技术 总结
1．有限状态机 2．Petri网
3.3.1有限状态机
（1）产生背景
（2）形式化定义 （3）有限状态图的表示 （4）“生产者与消费者”实例
（1）产生背景

有限状态机或者自动机的概念于20世纪50 年代提出，包括Moore机和Mealy机。由 于状态机本质上的可操作性，因而它成为 多种操作模型的基础。经典的有限状态机 （Moore机和Mealy机），可用来规格系 统的行为特性，并具有状态迁移图和状态 迁移矩阵两种表述方式。
1 形式化技术的产生和发展

尽管当前对大型复杂的系统进行完整的形 式化验证还不现实，但把形式化技术应用 于大型复杂系统的关键部分确实是一个有 效的实用策略。目前，有效的模型检验和 定理证明技术已成为硬件验证中传统仿真 技术的补充，而软件开发工程师们开始使 用更为严格的形式化规格及验证技术，成 功地完成了过程控制领域工业规模系统的 设计，通信系统中大量的安全可靠通信协 议得到了测试和检验。
（4）英国国防部的标准

在某些环境下，形式方法的使用是强制性 的。英国国防部在20世纪90年代初期发行 了两种与软件开发生命周期中使用形式方 法有关的安全至上标准。
（4）英国国防部的标准


第一个标准是防卫标准(Defense Standard)0055，即Def Stan00-55 另一个防卫标准是Def Stan 00-56
2 软件开发中为什么使用形式化方法



（1）保证质量的需要 （2）节约成本的需要 （3）形式方法和复用 （4）英国国防部的标准 （5）经典案例
（1）保证质量的需要

为了得到高质量的软件，我们强烈地希望 使用软件工程中最好的实践。软件中存在 的缺陷至少会引起客户的愤怒，而在更坏 的情况下可能会给客户的业务造成较大的 破坏或者造成生命损失。因此，企业要采 用最好的实践，使他们的软件过程变得成 熟起来。形式方法是一种前沿技术，研究 表明，这种技术非常有助于那些希望把软 件产品的缺陷出现率减到最小的公司。