[科普中国]-抽象机符号

抽象机符号是B方法中一个模块称为一个抽象机。这是一个概念，非常接近于在程序设计上人们所熟知的一些概念，如模块、类、包或抽象数据类型。每个抽象机包含一些数据并提供了一些操作。抽象机中的数据不能直接触及，总是通过机器的操作去使用。

UML建模的形式化方法研究和应用形式化方法是建立在严格数学基础上的软件开发方法，能够精确地、无二义地描述系统，并且有严格的证明。B方法是一种较为实用的形式化软件开发方法，覆盖了从抽象规约到可执行代码生成的过程，拥有强有力的支持工具。B方法使用抽象机符号（A\1N）来构造模型，并支持规范说明的类型检测和动态验证。B方法的支持工具可用动画等方式模拟运行规范说明，根据需求和测试场景检查获得的规范说明是否符合需求，对提高软件的可靠性有着非常显著的作用。1

B方法简介B方法属于基于模型的规格说明符号语言范畴，是一种基于对象的形式化语言。J一RAbrial是对软件形式化方法及其应用做出了最重要贡献的人物之一。从20世纪70年代开始研究数据结构的程序的形式化规范问题，20世纪70年代后期在牛津大学程序设计研究组（PRG）访问期间完成了有关形式化规范语言z的开创性工作。为了将形式化方法与软件更好地平滑衔接，J一RAbrial从20世纪80年代前期开始了B语言和B方法的研究和开发。1985年至1988年，PRG在一项为期三年的R&D项目中研制开发了B语台‘方法和抽象机符号表示法。

B方法的口的是希望为整个软件开发过程提供坚实的数学基础。随着B方法的发展和成熟，B方法是国际上最受重视的实用性软件形式化方法之一，用它编写软件系统规范，进行系统设计和编程。它已经被成功地应用到许多关键性的工业开发项目中。一个早期的重要实例是巴黎地铁列车的信号系统，这一系统为减少列车的阳J距、提高整个地铁系统的安全性做出了显著贡献。

B方法是一种用于描述、设计计一算机软件的严格方法，其作用一直延伸到代码生成。B方法的中心思想是C.A.R.Hoare和E.W.Dijkstra的程序作为一个数学对象、前一后谓词、不确定性最弱前置谓词的概念。B方法使得软件系统的需求定义、规格说明、可执行软件组件实现处于一个统一的数学框架之下，以基于集合理论和符号表示法来书写。

通常最初的需求是以自然语言表示，或者使用图表，逻辑表格，B方法是借助数学的符号表示方法和谓词逻辑、集合、序列、函数及其他的抽象数据类型，以一种精确的方法来描述软件需求与设计。抽象机符号表示法（AbstractMaChineNotation:AMN）是B方法的规格说明与设计语言。广义代换语言（GeneraliZedSubstitUtionLanguage）提供了A训的形式语义，标识抽象机的操作。使用B方法开发时，首先要在用自然语言描述系统需求的基础上，描述系统的主要状态，构造反映需求的B方法形式规约，不变式给出这些状态需要满足的属性，操作给出这些状态的变化。由此得到的模型反映了软件系统实现的功能。然后对所得到的形式规约进行验证和产生证明义务（由B方法上具完成），确认该规约实现了系统的功能。1

抽象机在接受了形式化地描述一个软件系统的任务之后，需要一种能用于说明软件系统是什么、处理起来比较简单的通用模型，这一模型能更容易地阅读一个给定系统的描述，抽象机就是这样的一个模型。抽象机 （AbstractMachine:AM）是B方法的一个基本机制，其概念非常接近模块、类或抽象类型。

按照抽象机模型的方式去理解软件系统，就是说，总用一个状态以及各种各样能够改变这一状态的操作方式去理解它们。对这些系统的分析就构成了抽象机对应于状态定义的静态行为和对应于有关操作的动态行为。

静态行为即状态的描述:首先是构成了状态的组成成分所需要的变量;其次是描述了系统的静态规则有关的不变式。不变式是一个逻辑语句，基于有关变量并利用谓词演算和集合论的形式语言进行描述。

动态行为即操作的描述:操作就是在不变式的限制范围之内修改抽象机器中的状态。

抽象机的各个子句如下：

MACHINE子句；CONSTRAINTS子句；SET子句；CONSTANTS子句；PROPERITIES子句；VARIABLES子句；DEFINITIONS子句；INVARIANTS子句；INITIALISATION子句；ASSERTION子句；OPERATI0N子句。1

UML用例模型的B形式化描述方法以UML用例模型为主要研究对象，在分析UML用例模型概念和B抽象机符号的基础上，对用例模型建模元素的抽象语法进行描述，建立两者之间的映射，实现UML用例模型图到B形式规约的转换。首先用半形式化的UML用例模型为目标系统建立需求模型，然后根据给出方法构建目标系统的B形式化规约，再利用B方法支持工具对规约进行动态分析和模型验证，得出可靠的形式规约，为在此基础上进行的形式推导和精化提供了正确的起点。最后，通过对电梯控制系统的实例分析，进一步详述了UML用例模型到B方法形式规约的转换方法及过程，并利用B方法的支持工具ProB对所得到的形式化模型进行了动态分析和模型检测。2

B方法概述B方法当前正为产业界和学术界越来越多的人们所关注，研究工作是在20世纪80年代的初期和中期由J.R Abrial以及BP研究中心的MATRA和GEC Alsthom研究小组进行的，目的是希望为实际软件开发过程提供一个坚实的数学基础。B方法以Z语言的研究为背景，在引入一些面向对象机制等特点的同时，保留了Z语言的优点，即基于所熟悉且便于理解的数学基础。在B方法的形成过程中，吸收了将程序作为一个数学对象、前-后谓词、不确定性最弱前置谓词的概念以及‘’Programming fromSpecification‘’的重要思想。

B方法是一广谱方法，包含了高度抽象的数学描述和可执行的描述。它借助数学符号表示方法，如谓词逻辑、集合、序列、函数及其他的抽象数据类型，在软件开发的各个阶段采用统一的AMN（Abstract Machine Notation），以一种精确的方法描述系统规约和系统设计，使程序和程序的规约说明处于统一的数学框架下，支持规约说明特性推理（包括内部一致性验证和精化验证），减少出现语义错误的可能性。

在B方法中，软件系统模型由一个或多个相互依存地抽象机构成，称为B模型。B模型由三种类型的B组件共同表达：机器（MACHINE）、精化（REFINEMENT）、实现（IMPLEMENTATION）。通常，B模型有一个MACHINE 组件来描述目标系统的规约，有多个精化来描述系统的开发过程，有一个实现表达系统的最终实现细节，其中实现是一种特殊的精化，是系统精化的最后阶段，可借助工具直接转化为可执行代码（如C语言代码）。为了确保规约本身及精化过程的一致性，B方法提供了正确性验证机制，自动产生证明义务，并且两个商业支持工具（B-Toolkit和Atelier-B）都能自动证明大部分的证明义务。从本质上看，B方法处理的是软件生存周期的核心方面，即技术性的规范，通过一系列精化步骤进行设计，产生层次性体系结构，以及可执行代码的生成。2

抽象机的精化精化是一种技术，用于将软件系统的‘’抽象模型‘’（其规范）变换为另一种更加具体的模型表示（即精化结果）。后一种模型可能在两个方面更具体：首先，它可能包含了与原来非形式规范有关的更多细节；其次，它可能更接近于实现。

B方法通过分层模块方式构造大型的软件系统的基本思想是：抽象机的数学模型要经过多次精化，直到最后的精化结果能够直接在计算机上执行。这样的一个精化结果可能引入另外一些抽象机（其他模块）作为最终实现的基础。由于这种原因，最终精化的结果被称为实现。

一次精化可以从MACHINE到一个REFINEMENT组件，或从一个REFINEMENT组件到另一个REFINEMENT组件，或者从REFINEMENT组件到IMPLEMENTATION组件。精化过程向规约中引入了所有非形式规约中表达的性质，在每一步精化过程中都必须证明精化关于其抽象的正确性，且都需要通过广义代换整体性地重新构造初始的抽象机。在B方法中，软件开发过程就是一个对规约（抽象机集合）逐步精化直至实现的过程。2

本词条内容贡献者为:

王沛 - 副教授、副研究员 - 中国科学院工程热物理研究所