形式化验证方法

授权

摘要

本发明公开了一种形式化验证方法，包括SEDS建模步骤，用于依据电子数据表单规范文件建立SEDS模型；模型转换步骤用于将SEDS模型转换为适合模型检查的形式化模型；性质规约步骤用于对SEDS模型的功能逻辑的性质进行形式化描述；形式化验证步骤用于对形式化模型和所描述的功能逻辑性质进行形式化验证，得到验证结果。本发明通过将SEDS模型转换为形式化模型，对SEDS模型的功能逻辑的性质进行形式化描述，对形式化模型和性质描述进行形式化验证，以从数学推理角度对SEDS的功能逻辑实现检查，进而保障软件的正确性和可靠性，同时用户还可以根据验证结果发现功能逻辑中存在的冲突或缺陷，并对SEDS模型中的错误进行修正。

基本信息

专利标题：

形式化验证方法

专利标题（英）：

暂无

公开（公告）号：

CN111427565A

申请号：

CN202010113863.5

公开（公告）日：

2020-07-17

申请日：

2020-02-24

授权号：

CN111427565B

授权日：

2022-04-05

发明人：

黄滟鸿杨秀丽史建琦曹桂涛郭欣

申请人：

华东师范大学

申请人地址：

上海市普陀区中山北路3663号

代理机构：

北京辰权知识产权代理有限公司

代理人：

付婧

优先权：

CN202010113863.5

主分类号：

G06F8/35

IPC分类号：

G06F8/35 G06F11/36