公开(公告)号：CN115829018A

公开(公告)日：2023-03-21

申请号：CN202211422138.1

申请日：2022-11-14

Applicant: 西安电子科技大学

Inventor： 田聪 ,  董彦松 ,  段鑫民 ,  刘月浩 ,  赵亮 ,  于斌 ,  段振华

IPC: G06N3/08 ,  G06N3/048

Abstract: 本发明涉及一种基于误差分治的神经网络验证方法，采用改进的符号线性松弛计算给定输入范围内网络节点的严格近似函数，并使用过近似节点的误差约束分割策略将原验证问题划分为等价的一系列子问题，对一系列子问题进行完备验证从而验证整个神经网络的安全属性。通过本发明的方法，有效地缩减了神经网络验证过程中的状态空间，能够高效地对神经网络进行安全属性验证和评估并且能够提高神经网络可信验证方法的可扩展性。

公开(公告)号：CN115080112A

公开(公告)日：2022-09-20

申请号：CN202210575903.7

申请日：2022-05-25

Applicant: 西安电子科技大学

Inventor： 赵亮 ,  王祥坤 ,  段振华 ,  王小兵 ,  田聪 ,  张南

IPC: G06F8/75 ,  G06F11/36

Abstract: 本发明涉及一种基于PVS的PPTLI定理证明的形式化验证方法，包括：S101：通过PVS构建得到PPTLI的基本时序类型和PPTLI的索引表达式类型，并根据PPTLI的索引表达式类型等价表示线性时序逻辑；S102：根据PPTLI的基本时序类型和PPTLI的索引表达式类型，通过PVS构建得到PPTLI定理证明系统；S103：将待证明的PPTLI时序性质表示为定理，利用PVS交互式证明命令使用PPTLI定理证明系统对待证明的PPTLI时序性质进行证明。本发明的方法借助于PPTLI这种表达能力强且综合统一的时序逻辑来描述和证明计算机系统预期的性质，能够弥补现有定理证明技术的不足，以保障系统的安全性和可靠性。

公开(公告)号：CN113255295A

公开(公告)日：2021-08-13

申请号：CN202110457578.X

申请日：2021-04-27

Applicant: 西安电子科技大学

Inventor： 王小兵 ,  李戈 ,  李春奕 ,  段振华 ,  赵亮 ,  田聪 ,  张南

IPC: G06F40/151 ,  G06F40/211 ,  G06F40/30

Abstract: 本发明属于计算机辅助设计技术领域，公开了一种自然语言到PPTL形式化规约自动生成方法及系统，所述自然语言到PPTL形式化规约自动生成方法包括：利用自然语言处理技术解析自然语言性质文本并生成语法树，遍历该树进行句子成分的提取、重排和标记等预处理操作，并生成标记文本；使用JavaCC工具对标记文本进行语法语义分析，生成含有子句、连接词和时序信息的句法树，遍历句法树生成原子命题及组合PPTL公式；使用PPTLSAT工具判定生成公式的可满足性。本发明能够帮助用户从自然语言描述的性质中提取形式化规约用于模型检测，将用户描述的自然语言文本性质转化为PPTL公式，为普通用户使用模型检测技术提供方便。

公开(公告)号：CN113238759A

公开(公告)日：2021-08-10

申请号：CN202110399134.5

申请日：2021-04-14

Applicant: 西安电子科技大学

Inventor： 段振华 ,  谷宇天 ,  张南 ,  田聪 ,  王小兵 ,  赵亮 ,  陆旭 ,  于斌 ,  张捷

IPC: G06F8/41 ,  G06F8/76

Abstract: 本发明属于计算机程序设计语言及应用技术领域，公开了一种类Python程序设计语言XD‑M的解释系统及方法，所述类Python程序设计语言XD‑M的解释方法包括：对于XD‑M语言中的基本语句和源自建模仿真验证语言MSVL的语句，通过调用MSVL解释器底层接口的方法进行解释；对于具有XD‑M语言特性的语句，为语句建立等价的MSVL语法树，扩展底层接口，编写底层对该语句的解释方法。本发明使用XD‑M语言编写的XD‑M程序可以进行建模、仿真和验证，提高了XD‑M语言的正确性、可靠性和安全性，实现类Python的使用简单变量而无需类型声明的编程风格，提高XD‑M程序的灵活性；依托MinGW开发环境。

公开(公告)号：CN110427179A

公开(公告)日：2019-11-08

申请号：CN201910563394.4

申请日：2019-06-26

Applicant: 西安电子科技大学

Inventor： 王小兵 ,  朱云凯 ,  段振华 ,  赵亮 ,  田聪 ,  张南

IPC: G06F8/30 ,  G06F8/41

Abstract: 本发明属于计算机辅助设计技术领域，公开了一种面向智能合约语言的MSVL程序自动生成方法及系统，将Solidity的特殊变量抽取为MSVL程序，预生成的MSVL代码具有一次生成永久有效的特征，其不会因Solidity程序的改变而改变；使用JavaCC工具对Solidity的词法和语法做分析，在扫描Solidity代码的过程中识别出特定的单词和语句；通过细致地对比Solidity和MSVL的词法和语法，制定出MSVL等价描述Solidity语言的可行性规则，并在Solidity代码扫描的过程中动态的生成MSVL程序。本发明能够有效地检测出智能合约是否存在安全漏洞和逻辑漏洞。

公开(公告)号：CN105653935B

公开(公告)日：2018-12-18

申请号：CN201610012054.9

申请日：2016-01-08

Applicant: 西安电子科技大学

Inventor： 王小兵 ,  刘东淼 ,  段振华 ,  赵亮 ,  田聪 ,  张南

IPC: G06F21/52

Abstract: 本发明公开了一种基于PPTL3的社交网络系统隐私安全运行时验证方法，对于待验证的性质P，用PPTL3公式来描述，然后分别将P与非P所对应的逻辑公式转化为范式，并进一步转化为范式图及带标记的范式图，根据后者可求得相应的Buchi自动机，通过改变接受集来定义一个有穷自动机并对其确定化，最终对有穷自动机求积以构造监控器；在此基础上，还公开了运行时验证在社交网络系统中的应用，通过PPTL3公式来描述社交网络应满足的性质，并建立相应的监控器，在系统运行的时候，对其进行监控以判断当前的运行是否满足该性质。

公开(公告)号：CN107679400A

公开(公告)日：2018-02-09

申请号：CN201710772215.9

申请日：2017-08-31

Applicant: 西安电子科技大学

Inventor： 王小兵 ,  郭文轩 ,  段振华 ,  赵亮 ,  田聪 ,  张南

IPC: G06F21/54 ,  G06Q50/00

Abstract: 本发明属于计算机应用技术领域，公开了一种基于源代码插桩的社交网络安全运行时验证方法及系统，通过对开源社交网络进行代码插桩来捕获事件，用PPTL3来描述性质并生成相应的性质监控模块，然后将事件和性质监控模块输入运行时监控器，运行时监控器自动的监控开源社交网络的运行是否符合给定的性质，并可以在社交网络不满足性质时给出监控信息，避免了模型检测状态空间爆炸的问题，也不需要复杂的定理证明，而且具有良好的实时性。本发明在不影响社交网络正常运行的前提下进行代码的插桩，以此实时的捕获关注的事件并验证性质，解决在大型开源社交网络中，传统模型检测方法的状态爆炸和不具备实时性的问题。

公开(公告)号：CN104111889B

公开(公告)日：2017-10-20

申请号：CN201410330453.0

申请日：2014-07-11

Applicant: 西安电子科技大学

Inventor： 王小兵 ,  苏多铎 ,  段振华 ,  赵亮 ,  田聪 ,  张南

IPC: G06F11/36

Abstract: 本发明公开了一种基于TMSVL的C语言实时系统运行形式化分析方法，所述方法使用TMSVL语言来描述C语言实时系统的性质，即描述待验证性质变量在特定时间的值，同时在C语言实时系统源代码中加入断言语句，通过执行加入断言语句后的C语言实时系统来获得待验证性质变量的信息，最终完成对C语言实时系统的运行形式化分析。本发明使得TMSVL验证C语言实时系统的性质更加容易，克服了人工建模工作量大、难度大以及容易出错的问题，同时相比于自动建模，本发明不需要建立复杂的转换器，提高了C语言实时系统形式化分析的效率。