-
公开(公告)号：CN115080112B
公开(公告)日：2025-05-13
申请号：CN202210575903.7
申请日：2022-05-25
Applicant: 西安电子科技大学
IPC: G06F8/75 , G06F11/3668
Abstract: 本发明涉及一种基于PVS的PPTLI定理证明的形式化验证方法，包括：S101：通过PVS构建得到PPTLI的基本时序类型和PPTLI的索引表达式类型，并根据PPTLI的索引表达式类型等价表示线性时序逻辑；S102：根据PPTLI的基本时序类型和PPTLI的索引表达式类型，通过PVS构建得到PPTLI定理证明系统；S103：将待证明的PPTLI时序性质表示为定理，利用PVS交互式证明命令使用PPTLI定理证明系统对待证明的PPTLI时序性质进行证明。本发明的方法借助于PPTLI这种表达能力强且综合统一的时序逻辑来描述和证明计算机系统预期的性质，能够弥补现有定理证明技术的不足，以保障系统的安全性和可靠性。
-
公开(公告)号：CN113778381B
公开(公告)日：2024-07-19
申请号：CN202110933517.6
申请日：2021-08-14
Applicant: 西安电子科技大学
Abstract: 本发明属于计算机程序设计语言及应用技术领域，公开了一种PPTL规范挖掘系统和方法，所述PPTL规范挖掘系统，包括Trace生成模块、Trace解析模块、PPTL_LNFG转换模块、LNFG实例化模块、LNFG检测模块和挖掘结果返回模块。本发明利用完全正则的PPTL形式化待挖掘的性质，将PPTL一次性转为LNFG从而减少时间的浪费，再用类似广度优先遍历的方式将trace中的事件与LNFG边上的PPTL状态公式进行对比，从而挖掘出满足程序执行trace的规范，且减少出现内存崩溃的情况，很好地解决了现有技术挖掘规范时由于重复将相同或类似的PPTL转为NF而导致挖掘时间过长的问题。
-
公开(公告)号：CN113255295B
公开(公告)日：2024-04-09
申请号：CN202110457578.X
申请日：2021-04-27
Applicant: 西安电子科技大学
IPC: G06F40/151 , G06F40/211 , G06F40/30
Abstract: 本发明属于计算机辅助设计技术领域，公开了一种自然语言到PPTL形式化规约自动生成方法及系统，所述自然语言到PPTL形式化规约自动生成方法包括：利用自然语言处理技术解析自然语言性质文本并生成语法树，遍历该树进行句子成分的提取、重排和标记等预处理操作，并生成标记文本；使用JavaCC工具对标记文本进行语法语义分析，生成含有子句、连接词和时序信息的句法树，遍历句法树生成原子命题及组合PPTL公式；使用PPTLSAT工具判定生成公式的可满足性。本发明能够帮助用户从自然语言描述的性质中提取形式化规约用于模型检测，将用户描述的自然语言文本性质转化为PPTL公式，为普通用户使用模型检测技术提供方便。
-
公开(公告)号：CN117113889A
公开(公告)日：2023-11-24
申请号：CN202210529119.2
申请日：2022-05-16
Applicant: 西安电子科技大学
IPC: G06F30/31 , G06F30/343 , G06F115/02
Abstract: 本发明涉及一种FPGA设计开发方法，包括以下步骤：在集成开发环境中，打开或创建工程，工程用于管理FPGA设计开发过程中涉及到的文件；根据开启工程指令打开或创建工程；在工程中添加资源文件，以调用集成开发环境对资源文件进行管理和编译转换；资源文件包括：设计文件和约束文件，或者，资源文件包括：设计文件、约束文件和仿真文件；调用集成开发环境的执行功能对工程中对应的资源文件进行编译和转换，并根据转换结果得到可载入FPGA芯片的比特流，执行功能包括：综合功能、实现功能和比特流生成功能，或者，还可以包括仿真功能。本发明为FPGA设计开发提供全流程调用以及简单友好的交互界面，可以提高FPGA设计开发的效率。
-
公开(公告)号：CN116107862A
公开(公告)日：2023-05-12
申请号：CN202210974710.9
申请日：2022-08-15
Applicant: 西安电子科技大学
IPC: G06F11/36
Abstract: 本发明公开了一种面向完全正则时序逻辑性质的高效运行时监控方法，包括：采用MSVL语言编写待监控程序，得到MSVL程序；采用PPTL公式形式化描述待验证的时序逻辑性质；针对PPTL公式中涉及的与MSVL程序有关的程序变量，对MSVL程序进行插桩；根据MSVL程序在动态执行过程中生成的状态序列，检测MSVL程序的实时运行状态，并根据检测结果判断MSVL程序的运行状态是否满足待验证的时序逻辑性质。本发明提供的利用分布式架构的运行时监控方法可用于对MSVL程序的完全正则时序逻辑性质的正确性检测，使得MSVL程序的动态执行状态能够得到及时检测，有效地保障了MSVL程序的可靠性和安全性。
-
Patent Agency Ranking
公开(公告)号：CN111767739A
公开(公告)日：2020-10-13
申请号：CN202010457574.7
申请日：2020-05-26
Applicant: 西安电子科技大学
IPC: G06F40/30 , G06F16/335 , G06F16/35 , G06F16/951 , G06K9/62
Abstract: 本发明属于网络监控技术领域，公开了一种基于PPTL3的微信群在线监控方法及系统，首先使用网络爬虫获取微信群的文本，然后使用PPTL3来描述特定的性质并生成对应的监控器，之后使用文本分类技术和关键词过滤获取性质相关的文本，进而判定性质对应的原子命题的真假，最后将原子命题组合成状态子公式输入到监控器中，如果到达TRUE节点，表明性质成立；如果到达FALSE节点，表明性质不成立；如果到达其他节点，说明当前获取到的信息无法判定性质是否成立，需要继续运行。本发明不需要对微信系统进行建模，从而避免传统模型检测方法的状态空间爆炸的问题，并且通过结合多种技术，完成了对微信群的在线监控。
-
公开(公告)号：CN106682306B
公开(公告)日：2020-07-07
申请号：CN201611221318.8
申请日：2016-12-26
Applicant: 西安电子科技大学
IPC: G06F30/347
Abstract: 本发明公开了一种快速FPGA布线方法，该方法采用新的重布线策略和波前扩展方法。该FPGA布线方法迭代地对所有线网进行布线直到找到一个合法的布线结果或者达到最大迭代次数。在每次布线迭代过程中，新的重布线策略只对非法的路径进行重布，保留合法的路径，从而减少每次布线迭代的时间。在对每一个线网漏端点进行布线时，布线树上距离目标漏端点t相对较远的节点出现在连接t的最优路径上的概率较低，因此在对波前进行初始化时只使用距离t相对较近的布线树节点，当布线树较大时，可以显著减少波前初始化的时间。本发明在保持关键路径延时和线长均有优化的前提下，明显减少了布线运行时间。
-
公开(公告)号：CN107844415A
公开(公告)日：2018-03-27
申请号：CN201710896756.2
申请日：2017-09-28
Applicant: 西安电子科技大学
IPC: G06F11/36
Abstract: 本发明属于计算机应用技术领域，公开了一种基于插值的模型检测路径缩减方法、计算机，读入C程序，对C程序进行语法语义分析，并从抽象语法树中提取出控制流自动机CFG；给CFG添加safety(S)插值和error(E)插值，扩展CFG；在根据CFG生成ARG的过程中，在每一个状态，判断safety插值和error插值是否被当前路径公式蕴含。本发明通过计算S插值和E插值，提高了检测的效率，使得模型检测算法可以更好地应用于大规模的程序；S插值避免不必要的探索，大大地减少ARG的状态数；E插值可以运用于快速地判断程序中是否存在真反例路径，加快了程序的验证，提高了效率；裁剪CFG中无用结点和边，缩小了遍历状态空间。
-
公开(公告)号：CN104657542B
公开(公告)日：2017-12-19
申请号：CN201510040674.9
申请日：2015-01-27
Applicant: 西安电子科技大学
IPC: G06F17/50
Abstract: 本发明公开了一种基于MSVL的Petri网模型检测方法，首先利用现有的建模工具Workcraft建立Petri网系统模型，然后将该模型转换成等价的MSVL程序，为此本发明给出了分别由Petri网系统的顺序语意、并行语意和最大并行语意指导的三种转换方法；最后使用现有的MSVL支持工具MSV对生成的MSVL程序进行仿真、建模和验证。针对上述转换方法，本发明开发了转换工具PN3MSVL和PN4MSVL，使得工具MSV能够对Petri网系统的各种语意进行分析和验证。本发明解决了现有的Petri网模型检测方法难以充分验证各种语意的完全正则性质的问题。
-
公开(公告)号：CN104281480B
公开(公告)日：2017-06-06
申请号：CN201410531029.2
申请日：2014-10-10
Applicant: 西安电子科技大学
IPC: G06F9/45
Abstract: 本发明公开了一种基于时序逻辑语言MSVL的函数调用方法，首先判断被调用函数的类型是MSVL函数、有返回值的外部函数还是无返回值的外部函数，根据不同的函数类型对被调用函数进行定义或者修改其定义；然后判断函数调用的位置，根据不同的函数调用位置以及相应的被调用函数类型，以不同的方式进行调用。本发明可以在同一程序中以不同的方式对被调用函数进行解释；并且在MSVL程序中可以调用由C语言和Java语言编写的函数，有利于多种不同编程语言程序的集成，有效降低程序开发的难度，提高代码复用率。
-
-
-
-
-
-
-
-
-
Search Results
132
records
(took 0.033 seconds)
