B方法在PVS中的应用

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