B方法在PVS中的应用

Application of Integrating B Method into PVS

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

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.