-
公开(公告)号：CN115346363A
公开(公告)日：2022-11-15
申请号：CN202210738974.4
申请日：2022-06-27
Applicant: 西安电子科技大学
Abstract: 本发明公开了一种基于神经网络的驾驶员违规预测方法，涉及违规预测技术领域，包括：获取原始数据；对原始数据进行处理，得到第一数据；采用第一数据对预设的第一模型进行训练，得到违规时间间隔预测模型，并对违规时间间隔预测模型进行评价；采用第一数据对预设的第二模型进行训练，对抗生成第二数据；将第一数据和第二数据进行综合，得到综合数据；采用综合数据对预设的第三模型进行训练，得到违规类型预测模型，并对违规类型预测模型进行评价；采用违规时间间隔预测模型和违规类型预测模型分别进行违规时间间隔和违规类型进行预测。本申请能够以较高的准确率对驾驶员违规进行预测。
-
公开(公告)号：CN113778381A
公开(公告)日：2021-12-10
申请号：CN202110933517.6
申请日：2021-08-14
Applicant: 西安电子科技大学
Abstract: 本发明属于计算机程序设计语言及应用技术领域，公开了一种PPTL规范挖掘系统和方法，所述PPTL规范挖掘系统，包括Trace生成模块、Trace解析模块、PPTL_LNFG转换模块、LNFG实例化模块、LNFG检测模块和挖掘结果返回模块。本发明利用完全正则的PPTL形式化待挖掘的性质，将PPTL一次性转为LNFG从而减少时间的浪费，再用类似广度优先遍历的方式将trace中的事件与LNFG边上的PPTL状态公式进行对比，从而挖掘出满足程序执行trace的规范，且减少出现内存崩溃的情况，很好地解决了现有技术挖掘规范时由于重复将相同或类似的PPTL转为NF而导致挖掘时间过长的问题。
-
公开(公告)号：CN113434132A
公开(公告)日：2021-09-24
申请号：CN202110498384.4
申请日：2021-05-08
Applicant: 西安电子科技大学
Abstract: 本发明属于系统形式化建模与验证领域和智能排课技术领域，公开了一种智能排课建模验证方法、系统，所述智能排课建模验证方法包括：使用MSVL语言对排课系统的功能需求分析进行系统建模，自定义业务实体的MSVL数据结构及算法，将核心模块编写为MSVL代码；使用命题投影时序逻辑PPTL公式描述系统期望性质，包括对课程、教师、教室、学生的约束在内的排课业务性质；使用PPTLCheck对系统MSVL代码与PPTL性质公式进行自动的模型检测验证。本发明能够在满足学校教学管理要求的前提下，较为合理地利用教学资源编排课表，且及时响应教学资源和约束条件的变化，是排课系统和基于MSVL的验证方法的成功结合。
-
公开(公告)号：CN109347651B
公开(公告)日：2021-06-01
申请号：CN201810981891.1
申请日：2018-08-27
Applicant: 西安电子科技大学
Abstract: 本发明属于形式化方法领域，公开了一种基于MSVL的区块链系统建模和安全性验证的方法及系统，在MC中用MSVL对区块链系统建模，用程序p表示；用PPTL描述区块链系统的性质，用公式φ表示；在MC中，加入MSVL的建模程序p和用PPTL描述的性质φ，验证区块链系统的安全性。本发明的区块链用MSVL程序进行建模，区块链的安全性性质用PPTL描述，而PPTL为PTL的命题子集，MSVL为PTL的可执行子集，因而MSVL和PPTL可以统一在MC中执行，相比于其他方法，本发明不需要使用另外的形式语言，也不需要调用另外的工具及大量的手工证明，只需要提供待验证性质的PPTL公式，证明过程由MC自动完成。
-
公开(公告)号：CN107844415B
公开(公告)日：2021-02-05
申请号：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中无用结点和边，缩小了遍历状态空间。
-
Patent Agency Ranking
公开(公告)号：CN110427179B
公开(公告)日：2020-10-16
申请号：CN201910563394.4
申请日：2019-06-26
Applicant: 西安电子科技大学
Abstract: 本发明属于计算机辅助设计技术领域，公开了一种面向智能合约语言的MSVL程序自动生成方法及系统，将Solidity的特殊变量抽取为MSVL程序，预生成的MSVL代码具有一次生成永久有效的特征，其不会因Solidity程序的改变而改变；使用JavaCC工具对Solidity的词法和语法做分析，在扫描Solidity代码的过程中识别出特定的单词和语句；通过细致地对比Solidity和MSVL的词法和语法，制定出MSVL等价描述Solidity语言的可行性规则，并在Solidity代码扫描的过程中动态的生成MSVL程序。本发明能够有效地检测出智能合约是否存在安全漏洞和逻辑漏洞。
-
公开(公告)号：CN106780055B
公开(公告)日：2020-05-22
申请号：CN201611068072.5
申请日：2016-11-28
Applicant: 西安电子科技大学
IPC: G06F16/9536 , G06Q50/00
Abstract: 本发明公开了一种基于MSVL社交网络用户关系强度的概率大小验证方法，包括：利用隐马尔可夫模型对社交网络中的用户关系强度和用户的交互行为进行建模，其中将用户关系强度作为隐状态，将用户之间的交互行为作为观测序列；在已知一个观测序列的基础上，利用时序逻辑语言MSVL对隐马尔可夫模型进行实现，得出最有可能产生这种观测序列的用户关系强度变化序列；采用命题投影时序逻辑PPTL公式描述用户关系强度状态的可能性大小，在MSV平台中进行建模和验证，验证用户关系强度概率大小是否符合期望值。本发明建模和验证可以在同一框架下进行；不需要调用另外的工具，简单方便，而且MSV平台可以给出详细的验证结果。
-
公开(公告)号：CN106371887B
公开(公告)日：2019-09-13
申请号：CN201610980621.X
申请日：2016-11-08
Applicant: 西安电子科技大学
IPC: G06F8/41
Abstract: 本发明公开了一种MSVL语言的编译系统及方法，包括：MSVL前端和底层虚拟机后端；MSVL前端包括词法语法分析模块，预处理模块和中间代码生成模块；LLVM后端包括目标代码生成模块；所述MSVL语言的编译方法对MSVL中的简单语句用正则形的方法进行预处理，对复杂语句，分别对每个并发分量进行预处理，并对每个并发分量创建一个线程。本发明很好地解决了现有技术执行MSVL程序效率低，影响了程序验证和执行的效率的问题，提高了MSVL程序的执行和验证效率；根据程序本身复杂程度的不同，其执行速度可提高几十倍乃至上百倍；并且一次编译成功后程序可以反复执行，无需再次编译。
-
公开(公告)号：CN106294780B
公开(公告)日：2019-04-30
申请号：CN201610663033.3
申请日：2016-08-12
Applicant: 西安电子科技大学
IPC: G06F16/951 , G06F16/80
Abstract: 本发明公开了一种从社交网络抽取MSVL模型的方法，所述从社交网络抽取MSVL模型的方法包括：通过网络爬虫或现有SNS数据包来获取感兴趣的SNS系统的数据信息；将获得的SNS系统信息进行分析，转化为统一的XML格式；将提取到的XML格式的SNS数据转化成MSVL程序，用形式化建模语言MSVL实现对SNS系统的建模。本发明对真实的SNS数据(网络爬虫获取或现有SNS数据包)进行分析，提取，转化为统一的XML格式，将XML文件当作中间层，屏蔽各种各样SNS数据格式对转化为形式化建模语言MSVL的影响。
-
公开(公告)号：CN109347651A
公开(公告)日：2019-02-15
申请号：CN201810981891.1
申请日：2018-08-27
Applicant: 西安电子科技大学
Abstract: 本发明属于形式化方法领域，公开了一种基于MSVL的区块链系统建模和安全性验证的方法及系统，在MC中用MSVL对区块链系统建模，用程序p表示；用PPTL描述区块链系统的性质，用公式φ表示；在MC中，加入MSVL的建模程序p和用PPTL描述的性质φ，验证区块链系统的安全性。本发明的区块链用MSVL程序进行建模，区块链的安全性性质用PPTL描述，而PPTL为PTL的命题子集，MSVL为PTL的可执行子集，因而MSVL和PPTL可以统一在MC中执行，相比于其他方法，本发明不需要使用另外的形式语言，也不需要调用另外的工具及大量的手工证明，只需要提供待验证性质的PPTL公式，证明过程由MC自动完成。
-
-
-
-
-
-
-
-
-
Search Results
132
records
(took 0.032 seconds)
