-
公开(公告)号：CN104111889B
公开(公告)日：2017-10-20
申请号：CN201410330453.0
申请日：2014-07-11
Applicant: 西安电子科技大学
IPC: G06F11/36
Abstract: 本发明公开了一种基于TMSVL的C语言实时系统运行形式化分析方法，所述方法使用TMSVL语言来描述C语言实时系统的性质，即描述待验证性质变量在特定时间的值，同时在C语言实时系统源代码中加入断言语句，通过执行加入断言语句后的C语言实时系统来获得待验证性质变量的信息，最终完成对C语言实时系统的运行形式化分析。本发明使得TMSVL验证C语言实时系统的性质更加容易，克服了人工建模工作量大、难度大以及容易出错的问题，同时相比于自动建模，本发明不需要建立复杂的转换器，提高了C语言实时系统形式化分析的效率。
-
公开(公告)号：CN104503816B
公开(公告)日：2017-09-19
申请号：CN201410841253.1
申请日：2014-12-30
Applicant: 西安电子科技大学
IPC: G06F9/45
Abstract: 一种硬件语言VHDL到MSVL的自动转换系统，其能够将VHDL语言程序文件转换成MSVL语言程序文件，所述转换系统包括，文件分析模块、词法分析模块、语法分析模块、信息存储模块、翻译模块、翻译结果字符串连接模块。VHDL程序转换为MSVL程序后，模型构造与性质描述使用同一种语言，使得验证在同一逻辑框架下进行，方便地实现对VHDL语言程序间接的模型检测。在转换的过程中，通过制定不同语法结构的转换规则，并通过一些额外的辅助手段将VHDL程序转换为了语义等价的MSVL程序，这样就可以通过对等价的MSVL程序进行仿真、建模和验证，来确保源VHDL程序的正确性。
-
公开(公告)号：CN104268023B
公开(公告)日：2017-08-25
申请号：CN201410531221.1
申请日：2014-10-10
Applicant: 西安电子科技大学
Abstract: 本发明公开了一种MSVL程序内存管理方法，包括框架变量存储区和非框架变量存储区；本发明基于MSVL语言中的框架技术，实现了一种MSVL语言的内存管理方法，使得在MSVL程序的执行过程中，能够动态地为变量分配和释放内存，节省了内存空间；针对MSVL程序中框架变量和非框架变量的特点，对两种变量的内存空间进行区分，使得程序从一个状态迁移到下一状态时，不需要在符号表中查找哪些变量是非框架变量，只需要直接删除非框架变量符号表中的符号，提高了程序的执行效率；针对框架变量的特点，用栈的方式对框架变量进行存储，当一个框架语句对应的区间结束时，该区间对应的框架变量将被删除，有效节省了内存空间。本发明可应用于MSV建模、仿真和验证工具中。
-
公开(公告)号：CN106682306A
公开(公告)日：2017-05-17
申请号：CN201611221318.8
申请日：2016-12-26
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明公开了一种快速FPGA布线方法，该方法采用新的重布线策略和波前扩展方法。该FPGA布线方法迭代地对所有线网进行布线直到找到一个合法的布线结果或者达到最大迭代次数。在每次布线迭代过程中，新的重布线策略只对非法的路径进行重布，保留合法的路径，从而减少每次布线迭代的时间。在对每一个线网漏端点进行布线时，布线树上距离目标漏端点t相对较远的节点出现在连接t的最优路径上的概率较低，因此在对波前进行初始化时只使用距离t相对较近的布线树节点，当布线树较大时，可以显著减少波前初始化的时间。本发明在保持关键路径延时和线长均有优化的前提下，明显减少了布线运行时间。
-
公开(公告)号：CN103916327B
公开(公告)日：2017-02-08
申请号：CN201410106285.7
申请日：2014-03-21
Applicant: 西安电子科技大学
IPC: H04L12/803 , H04L29/08
Abstract: 一种HP2P网络负载平衡的方法，其包括，HP2P网络群间负载平衡的方法，通过群分裂以及群在网络地址空间的移动来实现群之间的负载转移，并通过新节点加入负载较大的群诱导群发生分裂和合并从而使得负载较大的地址空间群数目较多，负载较小的地址空间群数目较少；HP2P网络群内负载平衡的方法，通过超级节点对群内负载有效的调度，使群内负载率较低的节点找到群内负载率较高的节点。
-
Patent Agency Ranking
公开(公告)号：CN103294596B
公开(公告)日：2016-11-16
申请号：CN201310196434.9
申请日：2013-05-23
Applicant: 西安电子科技大学
Abstract: 一种基于程序不变量的合约式软件故障预警方法，（1）使用Daikon工具为需要预警的程序生成程序不变量，根据测试用例集在Daikon工具上运行源程序产生不变量，输出程序不变量；（2）筛选不变量；（3）手动生成由布尔断言组成的数据合约；（4）将上述步骤2和3中两种方式得到的合约以规格化进行表示，并将规格化表示后的所述合约以注释的方式插桩到源程序的相应位置；（5）将步骤4中插桩到相应位置的注释转换为具有故障检测性质的代码，并插桩到源程序的相应目标位置；（6）运行经步骤1至5处理后的源程序，如果程序运行过程中违反了程序合约，则故障检测代码会自动把监测到的故障展示给用户。
-
公开(公告)号：CN105487873A
公开(公告)日：2016-04-13
申请号：CN201510884819.3
申请日：2015-12-04
Applicant: 西安电子科技大学
Abstract: 本发明公开了一种保证质量的快速软硬件划分方法，保留遗传算法的交叉运算和变异运算，并引入阴性选择算法的阴性选择过程和基于等位基因浓度来指导产生新个体的策略，采取一种新型的进化方法来加速进化的过程并保证个体的质量，从而克服传统遗传算法耗时长以及阴性选择算法结果随机性大、容易陷入局部最优的缺点。
-
公开(公告)号：CN104268023A
公开(公告)日：2015-01-07
申请号：CN201410531221.1
申请日：2014-10-10
Applicant: 西安电子科技大学
Abstract: 本发明公开了一种MSVL程序内存管理方法，包括框架变量存储区和非框架变量存储区；本发明基于MSVL语言中的框架技术，实现了一种MSVL语言的内存管理方法，使得在MSVL程序的执行过程中，能够动态地为变量分配和释放内存，节省了内存空间；针对MSVL程序中框架变量和非框架变量的特点，对两种变量的内存空间进行区分，使得程序从一个状态迁移到下一状态时，不需要在符号表中查找哪些变量是非框架变量，只需要直接删除非框架变量符号表中的符号，提高了程序的执行效率；针对框架变量的特点，用栈的方式对框架变量进行存储，当一个框架语句对应的区间结束时，该区间对应的框架变量将被删除，有效节省了内存空间。本发明可应用于MSV建模、仿真和验证工具中。
-
公开(公告)号：CN102307238B
公开(公告)日：2014-09-17
申请号：CN201110273600.1
申请日：2011-09-15
Applicant: 西安电子科技大学
Abstract: 本发明是一种HP2P网络中群的分裂与合并方法。本发明主要针对HP2P网络的上下层结点数量比例过大或过小会导致网络性能下降的问题，提出一种HP2P网络中群的分裂与合并的方法，通过计算结点间的亲和度将具有高亲和度的结点组织在一起，以使网络保持恰当的层间比例，从而维持HP2P网络的高效率、低负载和可扩展性。在群的分裂与合并方法中，将亲和度因子放在消息中进行传递，使得亲和度的计算简单，容易实现。在群分裂与合并后网络的拓扑结构还可以得到一次优化。本发明可应用于HP2P网络，还可应用于其它相似网络上的分裂与合并过程。
-
公开(公告)号：CN102663191B
公开(公告)日：2014-07-23
申请号：CN201210102064.3
申请日：2012-04-09
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明是一种基于SAT的命题投影时序逻辑限界模型检测方法，步骤是：用Kripke结构描述待验证系统模型M；用PPTL公式描述性质P；设定限界k；将PPTL限界模型检测转换为SAT问题；对SAT问题求解：有解，系统M不满足性质P，给出反例，无解，系统M有界满足性质P，增大k值，进入下一个检测周期，直到k值足够大且在每个限界模型检测周期内待验证系统M都有界满足性质P。本发明使用PPTL描述系统性质，解决了CTL和LTL表达能力有限的问题，并通过限制搜索长度减少搜索状态数，缓解了状态空间爆炸，融合了PPTL和BMC各自的优点，使系统复杂性质的验证更方便有效。本发明适用于软硬件系统以及通信协议的形式化验证。
-
-
-
-
-
-
-
-
-
Search Results
132
records
(took 0.033 seconds)
