-
公开(公告)号：CN118734013A
公开(公告)日：2024-10-01
申请号：CN202410769334.9
申请日：2024-06-14
Applicant: 华东师范大学
Abstract: 本发明公开了一种面向概率深度强化学习系统的形式化验证方法，主要用于验证由非确定性深度强化学习算法训练获得的系统的安全问题，具体步骤包括：(1)抽象训练：基于现有的抽象训练技术离散化抽象并进行抽象训练；(2)概率模型建模：依据原系统动力学设计抽象状态空间上的状态迁移规则，构建离散马尔科夫链模型；(3)验证分析：给出描述系统安全性质的PCTL时序逻辑规范，利用STORM概率模型检查器验证系统安全。本发明能够自动完成对概率深度强化学习系统的概率安全性质的检查，提供深度强化学习应用中的安全性。本发明还公开了一种实现所属概率系统形式化验证方法的工具。
-
公开(公告)号：CN112564972A
公开(公告)日：2021-03-26
申请号：CN202011424640.7
申请日：2020-12-09
Applicant: 华东师范大学
Abstract: 本发明提供一种基于Event‑B方法的区块链PBFT共识算法的形式化建模和安全性验证方法，根据PBFT共识算法在区块链上的运行机制，用Event‑B建模平台Rodin实现区块链上的PBFT共识算法，对PBFT共识算法的功能安全性进行形式化验证，包括确定模型的核心元素，根据不同元素的结构及性质转换成Event‑B模型的常量和变量，对常量定义相应公理，对变量定义相应不变式保证结构和性质成立；建立抽象模型，将算法执行过程映射为具体事件；按模块进行分层精化，增加不变式对区块链的安全性质进行表示，生成证明义务，验证算法的功能安全性。本发明实现了基于模型精化技术的区块链PBFT共识算法的形式化建模，利用形式化方法对算法的功能安全性进行了验证，并支持不同区块链共识算法的精化验证。
-
公开(公告)号：CN110968436A
公开(公告)日：2020-04-07
申请号：CN201911051831.0
申请日：2019-10-31
Applicant: 华东师范大学
Abstract: 本发明公开了一种基于Event-B方法的微内核操作系统进程间通信机制的形式化建模和验证方法，包括：需求设计分析，根据基于Event-B方法的微内核操作系统进程间通信机制，结合订阅者发布者模式，设计分析符合Event-B建模的原始需求。根据基于Event-B方法的微内核操作系统进程间通信机制以及原始需求的结果，设计分析符合Event-B建模的重写需求；建模精化验证，根据重写需求，设计建立验证基于Event-B方法的微内核操作系统进程间通信机制的模型。该模型需要验证的证明义务包括模型功能性不变式以及模型性质不变式和安全性质相关不变式。
-
公开(公告)号：CN104486659A
公开(公告)日：2015-04-01
申请号：CN201410738188.X
申请日：2014-12-05
Applicant: 华东师范大学
IPC: H04N21/431 , H04N21/485 , H04N5/91
CPC classification number: H04N21/4312 , H04N5/91 , H04N21/4854
Abstract: 本发明公开了一种用于播放视频的边缘融合处理与控制系统，包括：预融合配置管理器和融合配置播放终端；其中，至少两台融合配置播放终端分别与预融合配置管理器连接；预融合配置管理器用于控制融合配置播放终端调整融合配置参数，从融合配置播放终端收集融合配置参数，并根据融合配置参数对待播放视频进行边缘融合处理，形成视频影像信息，将视频影像信息进行分割，分别发送至对应的融合配置播放终端；融合配置播放终端对接收到的视频影像信息进行同步解码，并进行播放。本发明对投影屏幕大小及形状等无特别要求，成本低廉，可实现多通道视频同步播放，特别适用于播放视频的边缘融合应用场景。
-
公开(公告)号：CN113553581A
公开(公告)日：2021-10-26
申请号：CN202110785175.8
申请日：2021-07-12
Applicant: 华东师范大学
Abstract: 本发明公开了一种针对非平衡数据的入侵检测系统，包括获取模块，代码读取模块，分类模块，上采样模块，以及入侵检测模块，上述系统，在数据集构建中，通过对数据进行重采样，消除部分类别的不平衡，另外在入侵检测模型上进一步削减不平衡数据分类的难度，可以有效解决入侵检测系统中针对不平衡数据检测的问题，并能进一步提高保障系统安全的能力，做到高效智能。
-
Patent Agency Ranking
公开(公告)号：CN114741278B
公开(公告)日：2024-10-22
申请号：CN202210283082.X
申请日：2022-03-22
Applicant: 华东师范大学
IPC: G06F11/36
Abstract: 本申请提供了一种机载软件中目标代码到源代码的验证分析系统，具体的，第一代码模块根据第一目标代码通过反汇编得到第一汇编代码，根据第一汇编代码进行反编译得到第一C代码；关系映射模块将第一C代码与源代码进行对比，得到源代码变量名之间的对应关系；根据对应关系，结合第一汇编代码，得到源代码变量名与汇编代码的指令中逻辑地址的关系映射表；第二代码模块根据第二目标代码通过反汇编得到第二汇编代码；根据关系映射表对汇编代码进行反编译，得到第二C代码；第一验证分析模块将第二C代码与源代码进行对比，得到第一验证结果。本申请解决了IDA Pro不能对COFF格式文件进行反编译的缺陷，提供了新的可执行目标代码到源代码可追溯性验证思路。
-
公开(公告)号：CN110968436B
公开(公告)日：2023-07-14
申请号：CN201911051831.0
申请日：2019-10-31
Applicant: 华东师范大学
Abstract: 本发明公开了一种基于Event‑B方法的微内核操作系统进程间通信机制的形式化建模和验证方法，包括：需求设计分析，根据基于Event‑B方法的微内核操作系统进程间通信机制，结合订阅者发布者模式，设计分析符合Event‑B建模的原始需求。根据基于Event‑B方法的微内核操作系统进程间通信机制以及原始需求的结果，设计分析符合Event‑B建模的重写需求；建模精化验证，根据重写需求，设计建立验证基于Event‑B方法的微内核操作系统进程间通信机制的模型。该模型需要验证的证明义务包括模型功能性不变式以及模型性质不变式和安全性质相关不变式。
-
公开(公告)号：CN116401809A
公开(公告)日：2023-07-07
申请号：CN202310058021.8
申请日：2023-01-20
Applicant: 华东师范大学
IPC: G06F30/20 , G06F119/12
Abstract: 本发明公开了一种面向OpenSCENARIO的智能驾驶场景建模及其形式化验证方法，主要用于验证智能驾驶场景的安全问题，具体步骤包括：(1)设计模型转换规则将OpenSCENARIO描述场景模型转换为时间自动机网络；(2)构建计算模块处理车辆运动状态等复杂计算，提取驾驶场景信息；(3)给出描述智能驾驶场景安全等性质的TCTL时序逻辑规范，利用UPPAAL模型检测工具验证该场景的安全性。本发明能够自动发现智能驾驶场景中存在的安全问题，提高智能驾驶的安全性。本发明还公开了一种实现上述模型转换的自动化工具。
-
公开(公告)号：CN115527058A
公开(公告)日：2022-12-27
申请号：CN202210961813.1
申请日：2022-08-11
IPC: G06V10/764 , G06V10/774 , G06V10/25 , G06V10/26 , G06V10/44 , G06N20/00 , G06N3/08 , G06N3/04
Abstract: 本发明公开了一种基于模块协同的机器学习系统概率正确性建模与评估方法，所述方法包括：根据系统构建的SysML活动图，将活动图中的活动节点分类为智能模块与非智能模块，并使用构型的概念，来描述活动图中活动模块之间的组合以及数据交互，以此建立整个系统的模型；测定模型中每个智能模块的概率正确性，并通过模块协同算子所定义的相应公式，计算系统模型中复合构型的概率正确性，最后从系统起始点出发，依次计算每个流程中数据概率正确性的传递，最终评估获得系统整体的概率正确性。本发明还公开了实现上述建模与评估方法的系统。
-
公开(公告)号：CN112564972B
公开(公告)日：2022-04-05
申请号：CN202011424640.7
申请日：2020-12-09
Applicant: 华东师范大学
Abstract: 本发明提供一种基于Event‑B方法的区块链PBFT共识算法的形式化建模和安全性验证方法，根据PBFT共识算法在区块链上的运行机制，用Event‑B建模平台Rodin实现区块链上的PBFT共识算法，对PBFT共识算法的功能安全性进行形式化验证，包括确定模型的核心元素，根据不同元素的结构及性质转换成Event‑B模型的常量和变量，对常量定义相应公理，对变量定义相应不变式保证结构和性质成立；建立抽象模型，将算法执行过程映射为具体事件；按模块进行分层精化，增加不变式对区块链的安全性质进行表示，生成证明义务，验证算法的功能安全性。本发明实现了基于模型精化技术的区块链PBFT共识算法的形式化建模，利用形式化方法对算法的功能安全性进行了验证，并支持不同区块链共识算法的精化验证。
-
-
-
-
-
-
-
-
-
Search Results
18
records
(took 0.043 seconds)
