-
公开(公告)号：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公式，为普通用户使用模型检测技术提供方便。
-
公开(公告)号：CN117494100A
公开(公告)日：2024-02-02
申请号：CN202311533394.2
申请日：2023-11-16
Applicant: 西安电子科技大学
Abstract: 本发明公开了一种基于偏序约束求解的中断驱动程序验证方法及装置，该方法包括：将包含多个不同中断服务例程的待验证的C程序转换为静态单赋值形式的程序；构建静态单赋值形式的程序的符号化事件结构；根据符号化事件结构和静态单赋值形式的程序生成符号表，并在符号表中添加符合中断驱动程序的语义的约束；记录静态单赋值形式的程序中的中断开启依赖关系；中断开启依赖关系是用于使中断事件发生在开启中断之后的依赖关系；根据中断开启依赖关系对符号表中添加的约束进行约简；对包含约简后的约束的符号表进行求解，得到求解结果，根据求解结果得到C程序的验证结果。本发明能够提高验证准确率和验证效率。
-
公开(公告)号：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节点，表明性质不成立；如果到达其他节点，说明当前获取到的信息无法判定性质是否成立，需要继续运行。本发明不需要对微信系统进行建模，从而避免传统模型检测方法的状态空间爆炸的问题，并且通过结合多种技术，完成了对微信群的在线监控。
-
公开(公告)号：CN104281480B
公开(公告)日：2017-06-06
申请号：CN201410531029.2
申请日：2014-10-10
Applicant: 西安电子科技大学
IPC: G06F9/45
Abstract: 本发明公开了一种基于时序逻辑语言MSVL的函数调用方法，首先判断被调用函数的类型是MSVL函数、有返回值的外部函数还是无返回值的外部函数，根据不同的函数类型对被调用函数进行定义或者修改其定义；然后判断函数调用的位置，根据不同的函数调用位置以及相应的被调用函数类型，以不同的方式进行调用。本发明可以在同一程序中以不同的方式对被调用函数进行解释；并且在MSVL程序中可以调用由C语言和Java语言编写的函数，有利于多种不同编程语言程序的集成，有效降低程序开发的难度，提高代码复用率。
-
公开(公告)号：CN106294780A
公开(公告)日：2017-01-04
申请号：CN201610663033.3
申请日：2016-08-12
Applicant: 西安电子科技大学
IPC: G06F17/30
CPC classification number: G06F17/30864 , G06F17/30908
Abstract: 本发明公开了一种从社交网络抽取MSVL模型的方法，所述从社交网络抽取MSVL模型的方法包括：通过网络爬虫或现有SNS数据包来获取感兴趣的SNS系统的数据信息；将获得的SNS系统信息进行分析，转化为统一的XML格式；将提取到的XML格式的SNS数据转化成MSVL程序，用形式化建模语言MSVL实现对SNS系统的建模。本发明对真实的SNS数据(网络爬虫获取或现有SNS数据包)进行分析，提取，转化为统一的XML格式，将XML文件当作中间层，屏蔽各种各样SNS数据格式对转化为形式化建模语言MSVL的影响。
-
公开(公告)号：CN104731582A
公开(公告)日：2015-06-24
申请号：CN201510079118.2
申请日：2015-02-13
Applicant: 西安电子科技大学
Abstract: 本发明公开了一种基于MSVL的社交网络系统建模及隐私策略性质验证方法，首先采用框架投影时序逻辑程序设计语言MSVL对社交网络系统进行建模，同时采用命题投影时序逻辑PPTL描述其中的隐私策略性质，最后通过MSV解释器加以验证，得出该社交网络的隐私策略性质是否正确。本发明中，系统建模用MSVL程序，隐私策略性质用PPTL描述，MSVL是PTL的可执行子集，PPTL是PTL的命题子集，两者同属PTL框架结构，使得两者可以统一在MSV解释器中执行，相比于其他方法，本发明不需要调用另外的工具，也不需要再定义另外的逻辑语言、简单方便，而且MSV解释器可以给出准确的结果示意图。
-
公开(公告)号：CN104281480A
公开(公告)日：2015-01-14
申请号：CN201410531029.2
申请日：2014-10-10
Applicant: 西安电子科技大学
IPC: G06F9/45
Abstract: 本发明公开了一种基于时序逻辑语言MSVL的函数调用方法，首先判断被调用函数的类型是MSVL函数、有返回值的外部函数还是无返回值的外部函数，根据不同的函数类型对被调用函数进行定义或者修改其定义；然后判断函数调用的位置，根据不同的函数调用位置以及相应的被调用函数类型，以不同的方式进行调用。本发明可以在同一程序中以不同的方式对被调用函数进行解释；并且在MSVL程序中可以调用由C语言和Java语言编写的函数，有利于多种不同编程语言程序的集成，有效降低程序开发的难度，提高代码复用率。
-
-
-
-
-
-
-
-
-
Search Results
48
records
(took 0.048 seconds)
