B方法在PVS中的应用

来源 :上海应用技术学院学报(自然科学版) | 被引量 : 0次 | 上传用户：laiyq

【摘要】

：

针对B方法和原型验证系统（PVS）的特点,提出了将B方法引入到PVS中,即将一个用B方法描述的系统转换为由PVS描述,以此来实现形式化的检验证明.B方法中的抽象机在PVS中转换为一个方

【作者】

：

刘梅

【机构】

：

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

【出处】

：

上海应用技术学院学报(自然科学版)

【发表日期】

：

2015年4期

【关键词】

：

B方法原形验证系统形式化方法电梯系统控制器 B method prototype verification system（PVS） formal me

下载到本地 , 更方便阅读

下载此文赞助VIP

声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架

论文部分内容阅读

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

其他文献

多边矩阵的剖分和数据挖掘——处理复杂系统的新思维系列之二十八

介绍了多边矩阵的剖分概念,给出了多边矩阵剖分的基本性质,证明了多边矩阵剖分是矩阵理论中矩阵分块方法的直接推广.作为应用,研究了多边矩阵剖分和矩阵左半张量积、数量挖掘

期刊

多边矩阵基阵多边矩阵的剖分矩阵半张量积数据挖掘multilateral matricesbasic multilateral matrices

基于FPGA高精度信号相位差设计

在导航定位、精确制导中,脉冲参数测量是至关重要的信息.针对高精度、实时脉冲参数测量要求,采用现场可编程门阵列(FPGA)对脉冲参数信号相位差进行测量.相比较于离散傅里叶变

期刊

现场可编程门阵列离散傅里叶变换相位测量field programmable gate array(FPGA)discrete Fourier tran

磷酸锰锂正极材料的可控合成与电化学性能研究

研究了磷酸锰锂（LiMnPO4）微纳米材料的水热合成过程及其电化学特性。在水热合成过程中，改变各种参数，如反应温度、反应物LiOH浓度、铁元素掺杂等，制备一系列LiMn-PO4粉体。使用X射

期刊