-
公开(公告)号：CN115099414A
公开(公告)日：2022-09-23
申请号：CN202210608393.9
申请日：2022-05-31
Applicant: 西安电子科技大学
IPC: G06N20/00
Abstract: 本发明公开了一种基于索引表达式的梯度下降算法的建模方法，包括：基于预设的索引表达式，构建梯度下降谓词；根据梯度下降算法的预设精度，利用MSVL中的字符串对输入数据进行不同类型的运算，得到第一结果；读取数据集，并根据梯度下降谓词对多元线性回归模型进行训练，得到梯度下降的形式化模型；利用第一结果，对梯度下降的形式化模型的性质进行验证。本发明通过基于预设的索引表达式来构建梯度下降谓词，从而针对泰勒展开应用的形式化模型，可以对机器学习系统底层的安全性和可靠性进行验证分析。
-
公开(公告)号：CN113626813A
公开(公告)日：2021-11-09
申请号：CN202110876832.X
申请日：2021-07-31
Applicant: 西安电子科技大学
Abstract: 本发明属于程序运行验证技术领域，公开了一种基于运行时验证的边缘服务器DoS攻击检测方法，所述基于运行时验证的边缘服务器DoS攻击检测方法包括：采用PPTL公式形式化描述边缘服务器预期行为；采用PPTL公式形式化描述边缘服务器DoS攻击特征；针对PPTL公式中涉及的程序变量与程序函数，对边缘服务器运行程序进行插桩；针对边缘服务器程序的动态执行轨迹，采用并行运行时验证框架检测程序运行状态，根据检测结果判断边缘服务器是否正在被DoS攻击。本发明提供的基于并行运行时验证框架能够充分利用边缘服务器的空闲计算与存储资源，提高验证效率，及时发现攻击，还能够使得程序执行的每一个状态均能够得到可靠的验证，有效保障了边缘服务器安全性。
-
公开(公告)号：CN107679400B
公开(公告)日：2020-09-25
申请号：CN201710772215.9
申请日：2017-08-31
Applicant: 西安电子科技大学
Abstract: 本发明属于计算机应用技术领域，公开了一种基于源代码插桩的社交网络安全运行时验证方法及系统，通过对开源社交网络进行代码插桩来捕获事件，用PPTL3来描述性质并生成相应的性质监控模块，然后将事件和性质监控模块输入运行时监控器，运行时监控器自动的监控开源社交网络的运行是否符合给定的性质，并可以在社交网络不满足性质时给出监控信息，避免了模型检测状态空间爆炸的问题，也不需要复杂的定理证明，而且具有良好的实时性。本发明在不影响社交网络正常运行的前提下进行代码的插桩，以此实时的捕获关注的事件并验证性质，解决在大型开源社交网络中，传统模型检测方法的状态爆炸和不具备实时性的问题。
-
公开(公告)号：CN110443348A
公开(公告)日：2019-11-12
申请号：CN201910563393.X
申请日：2019-06-26
Applicant: 西安电子科技大学
Abstract: 本发明属于系统形式化建模与验证技术领域，公开了一种基于MSVL的神经网络系统的建模和验证方法。采用MSVL对需要进行验证的神经网络(包括DNN、CNN、RNN等)系统进行建模，用多维数组表示系统中所涉节点和边的信息，在建模中，用函数表示神经网路系统中的基本操作；确定需要验证的神经网络系统的共有性质特征，主要包括正确性和健壮性，并采用PPTL公式描述神经网络系统的这些性质；将建模的MSVL程序和描述共有性质的PPTL公式统一在UMC4MSVL平台中验证，根据验证结果判断性质是否能够得到满足。本发明将形式化的程序设计过程应用于神经网络系统的建模和验证，程序执行的每一个状态均能够得到可靠的验证，有效地保障了系统本身的安全性。
-
公开(公告)号：CN105487873B
公开(公告)日：2019-01-01
申请号：CN201510884819.3
申请日：2015-12-04
Applicant: 西安电子科技大学
Abstract: 本发明公开了一种保证质量的快速软硬件划分方法，保留遗传算法的交叉运算和变异运算，并引入阴性选择算法的阴性选择过程和基于等位基因浓度来指导产生新个体的策略，采取一种新型的进化方法来加速进化的过程并保证个体的质量，从而克服传统遗传算法耗时长以及阴性选择算法结果随机性大、容易陷入局部最优的缺点。
-
Patent Agency Ranking
公开(公告)号：CN106708525A
公开(公告)日：2017-05-24
申请号：CN201611223495.X
申请日：2016-12-27
Applicant: 西安电子科技大学
IPC: G06F9/44
CPC classification number: G06F8/31
Abstract: 本发明公开了一种基于Coq的MSVL程序验证方法，所述基于Coq的MSVL程序验证方法使用Coq规范语言Gallina描述MSVL的语法和语义；使用Coq规范语言描述MSVL的公理系统。本发明利用Coq强大的数学模型基础和完整的工具集来形式化MSVL公理系统，从而使得Coq能够识别MSVL程序；对使用MSVL建模的程序或系统，通过定理证明技术验证系统性质；可以将程序建模和抽取出的相关性质在Coq中转化成待证定理，通过人工选择合适的Coq策略链来指导证明的进行，从而完成性质的验证；琐碎的细节可以利用Coq策略自动的证明，人工仅在复杂的步骤上指导控制，有效地简化了MSVL程序的定理证明过程。
-
公开(公告)号：CN103258081B
公开(公告)日：2016-06-22
申请号：CN201310129977.9
申请日：2013-04-15
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明公开了一种抽象模型中虚假路径的高效检测方法，所述方法具体是，在反例路径中，每个状态是不是失败状态，只与它的前驱状态和后继状态有关。所以，判断时，采用并发执行，通过集合In和集合Out的交集来判断状态是否为失败状态。本发明在检测无穷反例路径时，采用有限前缀分析的多项式比已有的算法短。同时，采用并发技术，能更快的找出失败状态；而且，本发明能更早找到隐藏在反例路径中的失败状态，实验结果显示，系统的规模越大，本发明提出的方法执行的效果越好。
-
公开(公告)号：CN105488285A
公开(公告)日：2016-04-13
申请号：CN201510883669.4
申请日：2015-12-04
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明公开了一种高效FPGA技术映射算法，将技术映射划分为逻辑优化与结构优化，逻辑优化部分采用AIG模型以及balance、rewrite以及refactor等技术对电路进行优化；结构优化部分采用DAG模型，分为划分产生、划分选择以及LUT映射三步，划分产生采用了动态规划的思想，快速为每一个节点产生所有k-可行划分；划分选择基于一种迭代次数可以自适应改变的迭代启发式思想，通过多次向前遍历与向后遍历的迭代，最终选择出延时和面积同时被优化的划分集合，与此同时，本发明修正了节点面积流计算公式，提高了划分选择的随机性；LUT映射将划分选择产生的划分结合映射成为LUT网络。
-
公开(公告)号：CN104503816A
公开(公告)日：2015-04-08
申请号：CN201410841253.1
申请日：2014-12-30
Applicant: 西安电子科技大学
IPC: G06F9/45
Abstract: 一种硬件语言VHDL到MSVL的自动转换系统，其能够将VHDL语言程序文件转换成MSVL语言程序文件，所述转换系统包括，文件分析模块、词法分析模块、语法分析模块、信息存储模块、翻译模块、翻译结果字符串连接模块。VHDL程序转换为MSVL程序后，模型构造与性质描述使用同一种语言，使得验证在同一逻辑框架下进行，方便地实现对VHDL语言程序间接的模型检测。在转换的过程中，通过制定不同语法结构的转换规则，并通过一些额外的辅助手段将VHDL程序转换为了语义等价的MSVL程序，这样就可以通过对等价的MSVL程序进行仿真、建模和验证，来确保源VHDL程序的正确性。
-
公开(公告)号：CN102708228B
公开(公告)日：2015-02-18
申请号：CN201210118810.8
申请日：2012-04-20
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明公开了一种TMSVL实时系统建模方法，属形式化建模与验证领域，本发明通过扩展MSVL，得到的TMSVL可在同一逻辑框架下对实时系统进行建模和验证。TMSVL实时系统建模方法的步骤包括初始化系统时钟、建立系统的TMSVL模型和对TMSVL模型的化简。本发明用时间变量显式定义系统时钟，并依此定义了TMSVL基本语句和实时系统中常用的延时、超时和中断的概念，给出了TMSVL操作语义。用TMSVL语句描述实时系统后，操作语义通过对TMSVL语句的化简构造出系统的实际模型。本发明由MSVL扩展而来，具有MSVL的全部优点且能够表示相对和绝对时间约束，适应于实时系统的建模、仿真与验证。
-
-
-
-
-
-
-
-
-
Search Results
132
records
(took 0.032 seconds)
