B方法在PVS中的应用

刘 梅

（上海应用技术学院计算机科学与信息工程学院，上海 201418）

B方法在PVS中的应用

刘 梅

（上海应用技术学院计算机科学与信息工程学院，上海 201418）

针对B方法和原型验证系统（PVS）的特点，提出了将B方法引入到PVS中，即将一个用B方法描述的系统转换为由PVS描述，以此来实现形式化的检验证明.B方法中的抽象机在PVS中转换为一个方法，而B方法中的不变量不变式要转换为PVS中的一个类型，由B方法描述的性质则转换为PVS中的推测、猜想，并借助于PVS自带的证明器有效地完成相应证明工作.最后，通过1个电梯控制系统来阐述上述转换方法.

B方法；原形验证系统；形式化方法；电梯系统控制器

随着信息技术的不断发展，以及越来越多软硬件技术的结合，当今项目系统设计的要求越来越高.伴随着复杂的系统设计和高质量安全需求，这一趋势将在今后数年愈发明显.然而，如果仅通过软硬件测试，常常会因时间或财力等因素不能完全达到具体产品安全覆盖的要求.长期以来，人们认识到形式化方法［1］可以帮助设计人员发现和弥补一些疏漏，或者发现一些设计中有歧义的地方，以此来不断提高项目设计质量.本文集中关注B方法［2］和原型验证系统（PVS）［3］这2个形式化方法，建立一个可以将B方法引入的PVS系统，通过该方法，不仅能提高建模的质量，而且能利用一个强有力的定理证明器执行全类型检测.

1 E方法和PVS的概要介绍

1.1 E方法

一般而言，B方法是由一些抽象机组成，并在此基础上不断做出精化的过程，最后一步的精化相当于实现.在B方法中，一个模块称之为一个抽象机［4］，每一个抽象机都有其各自的业务，允许外部使用者调用或切换其当前状态.根据B方法的句法规则，一个抽象机由决定其状态和描述状态性质的一些子句所组成.子句包括集合、变量、不变量、初始化和操作等.在B方法中，变量描述的是内部变化；不变量约束的是变量的变化范围；初始化描述的是抽象机初始时所必需满足的不变量以及初始状态；由抽象机提供的方法称之为操作.抽象机的描述可以通过不断地精化直至最后的实现，且上述子句都将在精化中得以保留.

1.2 PVS

PVS的语言建立在高阶逻辑上，而高阶逻辑可以提供给模块更多的参数理论和更为丰富多样的类型系统，包括子类型的注释和类型依赖.PVS描述［5］由许多理论部分组成，每一个理论都由一些必要的声明组成：声明包含类型、常量、变量、公理和公式，也可以通过引用其他理论获得该理论中所用到的声明.

当一个模块被描述成一个理论后，在PVS中的类型检查必须执行，以此来发现理论中不一致的类型声明.当对一个理论进行过类型检查以及完成其所有猜测后，可认为这一理论的所有工作就完成了.当然，在PVS证明器中提供了许多不同概念的证明命令，如（induct“n“）是对于所证明公式中出现“n“时，运用数学归纳法进行自动推理证明；而（skolem！）是用来消除FORALL这一量词的，等等.这些证明都是一步步通过人机交互式完成的，在证明过程中，证明器保留着所有证明的步骤，当猜测证明完成后，会生成一棵类似树一样的证明过程图，所有用到的命令都是其节点，所有的叶子部门，都认为是正确的.

2 将E方法引入至PVS中

2.1 从E方法到PVS中的结构转换规则

为证明在B方法中所描述的性质，由B方法所描述的系统必须转换成PVS中的语言.转换之间一一对应的关系如表1所示.在这一转换中，B方法中的MACHINE（抽象机）对应PVS中的THEORY（理论）；INVARIANT（不变量）对应TYPE（类型）；OPERATIONS（操作）转换为PVS中的FUNCTIONS（函数）.B方法中的语义转换为PVS中的语言.

2.2 转换描述和实例

E方法

表1 E方法与PVS之间的转换Tab.1 Conversion between E method and PVS

在PVS中，类型为t的元素所组成的集合以谓词的方式出现，如一个由类型t至Boolean的函数.集合给出的形式可以为［t！bool］，pred［t］，或setof［t］，给出的类型均是等价的.

举例说明：

E方法 SETS BUS

E方法

此处将B方法中的性质转换成PVS中公理的形式.在使用公理前，必须进行证明，完成证明后，方可使用.

举例说明：

E方法 PROPERTIES

此处可认为1辆公共汽车中有乘客和司机.显然，这两类人都是自然数，且开在路上的公共汽车必须有司机.

此即为PVS所描述B方法中的性质.

E方法

在B方法中，不变量的使用是用来限制变量的.PVS中的类型声明是引入一个新的类型［6］，且这一新类型将被后面的变量所用到.

举例说明：

E方法

每一张票都有所对应的价格，并且当知道站数多少时，能够得到相应的PRICE（票价）即（ticket

在PVS中，首先定义TICKET这一类型，然后通过ticket这一变量使用它.

E方法

从某种意义上来讲，OPERATIONS是一个抽象的概念，由使用者自己定义［7］，类似于在PVS中的函数，故决定在PVS中直接用函数去描述OPERATIONS.

上述为FUNCTIONS（函数）的3种基本形式，每一个ti都是一种类型描述［8］.但有时也用predicate（谓词）定义FUNCTION（函数）.

举例说明：

E方法

此处操作可以认为，如果某一人上车后没有买票，那么他必须买相应的车票，之后集合has_ticket（记录乘客与票价之间的集合）会记录其行为.

在PVS中，has_ticket也是一个集合记录乘客有没有买票.而buy_ticket函数是判断该乘客是否有买票的操作，如果乘客已经买过票了，则has_ ticket集合保持不变，否则要求该乘客先行买票，之后将其加入已经买过票的has_ticket集合中.

3 实例分析

以一个简单的电梯控制系统为例，使用上述所提到的方法和理论.如在一栋有N部电梯的M层高的大楼里，每一部电梯都有一组按钮来控制，按钮与大楼的楼层相对应.电梯根据按钮的操作执行，只要对应楼层的按钮灯亮，电梯就往该层运行，当运行至相应楼层停靠后，按钮灯灭.在大楼的楼道里，除底楼和最高楼层外，都有2个按钮，对应电梯往上和往下运行执行请求.

3.1 E方法中的电梯控制系统描述

在电梯控制系统中有2个集合，分别用LIFT和DIERCTION（1个枚举类型）描述电梯的集合以及表明电梯运行的方向.电梯控制系统中还包括2个常量，分别是top和ground表示顶层以及底楼.

VARIABLES和INVARIANT：

（1）变量moving表示运行中的电梯；

（2）对于每一部电梯l而言，如果l没有在moving中，即l未处于运行状态，都可以通过floor（l）得到其所处停靠的相应楼层；

（3）dir（l）表明的是电梯运行的方向，当电梯运行时，dir（l）就是该电梯运行的方向，如果该电梯未运行，处于停靠状态，则dir（l）就是目标方向或保留其最后状态的方向；

（4）变量in是一个二元关系，对应的是FLOOR（楼层）至DIRECTION（方向）的概念，当（f，d）∈in，表明有人想从楼层f出发出往方向d执行的请求；

（5）变量out也是一个二元关系，对应的是LIFT（电梯）至FLOOR（楼层）的概念，当（l，f）∈out时，表明有人想从LIFT（电梯）中到具体的FLOOR（楼层）的请求；

（6）不变量moving△（out∩floor）=，表明moving不会出现的情况是当电梯l已经停靠在具体楼层f时，还有人在电梯中，想要电梯l发出执行至楼层f的请求，换言之，对于这样的请求不予执行；

（7）还要满足一类情况是，虽然电梯已经停靠在楼层f上了，但假使该电梯往上继续执行操作，这时楼道中的人按了往下执行的请求，电梯不予理睬，而楼道中往下方向的按钮灯不灭；对应的B方法描述为：

OPERATIONS（操作）：电梯应该有自己的操作方式，如有人在电梯l中按了去往f楼层的按钮，定义为Request Floor（l，f）；当然B方法中也有这样的描述Request Lift（f，d），表明有人在楼层f，想要得到去往d方向的请求.

3.2 在PVS中抽象机的实现

在提到的转换方法中，B方法中的电梯抽象机可以这样被转换引入到PVS的理论中，B方法中的SETS（集合）LIFT转换成PVS中的SET（集合）.为了验证某些性质，稍对B方法进行一些精化.想证明以下2个重要的性质概念：（Buttons）按钮的实现和如何控制这些按钮的状态变化.故在PVS中，用到了recordtype（记录类）这一概念，用来包含Buttons（按钮）和Control（如何控制）之间的关系.具体地说，Buttons（按钮）是所有的按钮，包括电梯中所有楼层的按钮，以及在楼道中，每一层的上、下请求的按钮；而Control（控制）包含的是所有楼层的信息，电梯的移动以及电梯执行的方向.使用记录类型：Lift=［＃btns：Buttons，ctr：Control＃］.

在B方法中，不变量INVARIANT（ground｜→dn）εin并且（top｜→up）εin是为了限制这样的需求：在底层没有往下执行的按钮，同样在顶层没有往上执行的按钮.在PVS中，增加了2个新的类型：Up_floor和Down_floor，用来描述每一楼层确切的方向执行请求.类型Up_floor定义了除了顶层外的每一层都有1个要求电梯往上执行的请求，而类型Down_floor定义了除了底层外的每一层都有1个要求电梯往下执行的请求.在B方法中变量moving转换成了PVS中的枚举类型Movement，表示电梯所处状态，running（运行）或者halted（悬停）.

在B方法中，不变量out∈LIFT FLOOR表明的是在电梯内部每一楼层的需求.而在PVS中，用［floor→boolean］描述在电梯中相应楼层是否应该停靠的请求.B方法中抽象机OPERATIONS（操作）可以转换成PVS的FUNCTIONS（函数），故Request_floor也相应地转换为PVS中的函数.如有人在电梯中按下了任一楼层的按钮，那么这一楼层的按钮灯必须亮起，并且该电梯将立即或者不久将运行至该层停靠，以响应该请求命令.

3.3 验证性质

由于篇幅所限，仅列出以下性质的验证：电梯一定会运行至相应请求过的楼层.在PVS中，可以给出如下猜测：首先，对于任一楼层按钮，发出请求后，都会有灯亮起；其次，电梯一定会在相应楼层停靠. response_push_floor：conjecture

使用命令（induct“f“）进行证明，会生成6个子目标.每个子目标使用grind或ground都很容易证明，不做赘述.

4 结 语

本文根据2种形式化方法，B方法和PVS的特点，提出将B方法子集的一部分引入PVS中，给出了B方法语义到PVS语言的转换规则.最后，对一个简单的电梯控制系统，分别进行B方法和PVS语言描述，并根据上述转换规则完成了验证工作.由此表明，文中提出的转换规则和方法的可操作性.B方法和PVS在形式化方法研究、系统检测、检验证明等方面具有更加深入的研究价值，如何将B方法中更多部分引入到PVS中，将是后续工作的重点.

［1］ Owr S，Shankar N.Abstract datatypes in PVS［J］. Computer Science Laboratory，SRI International，1999，1（3）：308-309.

［2］ Pratten C H.An introduction to proving AMN specifications with PVS and the AMN-PROOF tool［J］. IRIN-IUT de Nantes，2002，5（2）：149-165.

［3］ Pilotto C，White J.Towards a verification framework for faulty message passing systems in PVS［J］.Innovations in Systems and Software Engineering，2011，7（2）：109-118.

［4］ 许庆国，缪淮扣.实时系统形式规格说明在PVS中的建立［J］.计算机科学，2006，33（12）：239-240.

［5］ Moscato M M，Pombo C G L，Frias M F.Dynamite：a tool for the verification of alloy models based on PVS［J］.ACM Transactions on Software Engineering and Methodology，2014，23（2）：100.

［6］ 李昊，张敏，王榕.基于PVS的数据库安全策略形式化分析方法［J］.中国科学技术大学学报，2013，43（7）：591-598.

［7］ 唐宇.一种基于形式化B方法的软件构件模型［J］.天水师范学院学报，2009，29（2）：87-89.

［8］ 孙国栋，牛晋刚.超长整数运算的PVS规范与验证［J］.计算机工程与应用，2015，51（3）：93-94.

（编辑 吕丹）

Application of lntegrating B Method into PVS

LIU Mei
（School of Computer Science and Information Engineering，Shanghai Institute of Technology，Shanghai 201418，China）

A method to integrate the B method into prototype verification system（PVS）according to their characteristics was presented，which could convert a system described by B method into formal specification language of PVS.In this method，a machine in B method was expressed to be a theory in PVS，while an invariant to be a type in PVS.Some properties described by B method were transformed into conjectures of PVS language，then，these conjectures could be proved effectively by PVS prover.In the end，an example，a lift system controller，was given to illustrate the application of this method.

B method；prototype verification system（PVS）；formal method；lift system controller

TP 301.2

A

1671-7333（2015）04-0380-04

10.3969／j.issn.1671-7333.2015.04.014

2014-11-03

刘 梅（1968-），女，副教授，主要研究方向为数据库理论及应用，计算机课程教学方法.E-mail：liumei＠sit.edu.cn