-
公开(公告)号：CN116911355A
公开(公告)日：2023-10-20
申请号：CN202310685300.7
申请日：2023-06-09
Applicant: 西安电子科技大学
IPC: G06N3/0464 , G06N3/08 , G06N3/084
Abstract: 本发明公开了一种基于统一模型检测的神经网络训练性质验证方法，包括：按照层次化和模块化的原则，构建待验证的神经网络的MSVL形式化模型，MSVL形式化模型包括结构构建和基础行为构建；挖掘神经网络的训练相关性质并将训练相关性质构建为PPTL公式，训练相关性质包括梯度消失现象、梯度爆炸现象、大量神经元失活现象以及网络训练收敛；结合MSVL形式化模型和PPTL公式对神经网络进行验证，以判断神经网络中是否存在训练相关性质问题。本发明以神经网络的MSVL模型和PPTL公式为输入执行统一模型检测方法完成验证，可以有助于有效发现神经网络结构中存在的问题，改善神经网络的训练效果，为神经网络的训练和应用提供更加可靠和安全的保障。
-
公开(公告)号：CN113240075B
公开(公告)日：2023-08-22
申请号：CN202110439442.6
申请日：2021-04-23
Applicant: 西安电子科技大学
IPC: G06N3/0499 , G06N3/08 , G06N3/084
Abstract: 本发明属于BP神经网络技术领域，公开了一种基于MSVL的BP神经网络的构建和训练方法及系统，所述基于MSVL的BP神经网络的构建和训练方法包括：根据BP神经网络基本的层次化结构和属性行为特征，构建基于MSVL的BP神经网络的底层结构方法库；根据用户的定制需求，利用结构方法库中的MSVL结构体，构建BP神经网络的初始架构；读取样本数据，利用结构方法库中MSVL方法，对初始架构进行训练，得到BP神经网络的形式化架构。本发明涵盖了矩阵运算、反向传播、权值更新等多种神经网络系统的基本行为，可直接用于模型检测、插桩验证等形式化验证技术，并支持与这些行为相关的多方面性质的验证，从而系统的安全可信性能够得到有效的保障。
-
公开(公告)号：CN115829018A
公开(公告)日：2023-03-21
申请号：CN202211422138.1
申请日：2022-11-14
Applicant: 西安电子科技大学
Abstract: 本发明涉及一种基于误差分治的神经网络验证方法，采用改进的符号线性松弛计算给定输入范围内网络节点的严格近似函数，并使用过近似节点的误差约束分割策略将原验证问题划分为等价的一系列子问题，对一系列子问题进行完备验证从而验证整个神经网络的安全属性。通过本发明的方法，有效地缩减了神经网络验证过程中的状态空间，能够高效地对神经网络进行安全属性验证和评估并且能够提高神经网络可信验证方法的可扩展性。
-
公开(公告)号：CN115080112A
公开(公告)日：2022-09-20
申请号：CN202210575903.7
申请日：2022-05-25
Applicant: 西安电子科技大学
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: 西安电子科技大学
IPC: G06F40/151 , G06F40/211 , G06F40/30
Abstract: 本发明属于计算机辅助设计技术领域，公开了一种自然语言到PPTL形式化规约自动生成方法及系统，所述自然语言到PPTL形式化规约自动生成方法包括：利用自然语言处理技术解析自然语言性质文本并生成语法树，遍历该树进行句子成分的提取、重排和标记等预处理操作，并生成标记文本；使用JavaCC工具对标记文本进行语法语义分析，生成含有子句、连接词和时序信息的句法树，遍历句法树生成原子命题及组合PPTL公式；使用PPTLSAT工具判定生成公式的可满足性。本发明能够帮助用户从自然语言描述的性质中提取形式化规约用于模型检测，将用户描述的自然语言文本性质转化为PPTL公式，为普通用户使用模型检测技术提供方便。
-
Patent Agency Ranking
公开(公告)号：CN113238759A
公开(公告)日：2021-08-10
申请号：CN202110399134.5
申请日：2021-04-14
Applicant: 西安电子科技大学
Abstract: 本发明属于计算机程序设计语言及应用技术领域，公开了一种类Python程序设计语言XD‑M的解释系统及方法，所述类Python程序设计语言XD‑M的解释方法包括：对于XD‑M语言中的基本语句和源自建模仿真验证语言MSVL的语句，通过调用MSVL解释器底层接口的方法进行解释；对于具有XD‑M语言特性的语句，为语句建立等价的MSVL语法树，扩展底层接口，编写底层对该语句的解释方法。本发明使用XD‑M语言编写的XD‑M程序可以进行建模、仿真和验证，提高了XD‑M语言的正确性、可靠性和安全性，实现类Python的使用简单变量而无需类型声明的编程风格，提高XD‑M程序的灵活性；依托MinGW开发环境。
-
公开(公告)号：CN108595318B
公开(公告)日：2021-05-14
申请号：CN201810278731.0
申请日：2018-03-31
Applicant: 西安电子科技大学
Abstract: 本发明属于计算机软件分析技术领域，公开了一种RFC制导的SSL/TLS实现中数字证书验证模块的差异测试方法，从RFC中提取并更新规则；对规则进行分类，进一步对消费者规则和共享规则分为可打破规则和不可打破规则，规则转换为规则变量并生成动态符号执行技术中的输入即符号化程序；对符号化程序使用动态符号执行技术生成低级测试用例；根据低级测试用例组装高级测试用例即数字证书；使用组装的数字证书对SSL/TLS实现中的数字证书验证模块进行差异测试。本发明对被测试程序进行高效的差异测试；应用于SSL/TLS实现中数字证书验证模块的测试，发现潜在的软件缺陷或安全漏洞，提高SSL/TLS实现的正确性和安全性。
-
公开(公告)号：CN110427179A
公开(公告)日：2019-11-08
申请号：CN201910563394.4
申请日：2019-06-26
Applicant: 西安电子科技大学
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: 西安电子科技大学
IPC: G06F21/52
Abstract: 本发明公开了一种基于PPTL3的社交网络系统隐私安全运行时验证方法，对于待验证的性质P，用PPTL3公式来描述，然后分别将P与非P所对应的逻辑公式转化为范式，并进一步转化为范式图及带标记的范式图，根据后者可求得相应的Buchi自动机，通过改变接受集来定义一个有穷自动机并对其确定化，最终对有穷自动机求积以构造监控器；在此基础上，还公开了运行时验证在社交网络系统中的应用，通过PPTL3公式来描述社交网络应满足的性质，并建立相应的监控器，在系统运行的时候，对其进行监控以判断当前的运行是否满足该性质。
-
公开(公告)号：CN107679400A
公开(公告)日：2018-02-09
申请号：CN201710772215.9
申请日：2017-08-31
Applicant: 西安电子科技大学
Abstract: 本发明属于计算机应用技术领域，公开了一种基于源代码插桩的社交网络安全运行时验证方法及系统，通过对开源社交网络进行代码插桩来捕获事件，用PPTL3来描述性质并生成相应的性质监控模块，然后将事件和性质监控模块输入运行时监控器，运行时监控器自动的监控开源社交网络的运行是否符合给定的性质，并可以在社交网络不满足性质时给出监控信息，避免了模型检测状态空间爆炸的问题，也不需要复杂的定理证明，而且具有良好的实时性。本发明在不影响社交网络正常运行的前提下进行代码的插桩，以此实时的捕获关注的事件并验证性质，解决在大型开源社交网络中，传统模型检测方法的状态爆炸和不具备实时性的问题。
-
-
-
-
-
-
-
-
-
Search Results
132
records
(took 0.033 seconds)
