-
公开(公告)号：CN114356294A
公开(公告)日：2022-04-15
申请号：CN202111570950.4
申请日：2021-12-21
Applicant: 华东师范大学 , 卡斯柯信号有限公司 , 上海工业控制安全创新科技有限公司
IPC: G06F8/30
Abstract: 本发明公开了一种基于FQLTL的实例生成方法，本方法获取系统设备集合、设备性质以及设备间关系等配置信息，通过遍历公式的语法树进行逻辑计算，判断每个对象/对象集合是否满足公式中所限定的范围，由最终得到的逻辑运算结果可以滤去恒真/恒假的集合,这些集合都无需进行下一步验证，留下真正需要验证的设备集合，也就是状态不确定的设备集合。包括如下步骤：对公式进行语法解析；预处理；遍历语法树，进行可满足性检查；输出可满足性检查结果。由于验证器无法进行包含范围的性质验证，而这种新的形式化语言中规定了需要验证集合的范围。故本发明解决了在验证项目中，从系统全部的设备集合缩减到真正待验证实例的问题。
-
公开(公告)号：CN114356294B
公开(公告)日：2023-07-14
申请号：CN202111570950.4
申请日：2021-12-21
Applicant: 华东师范大学 , 卡斯柯信号有限公司 , 上海工业控制安全创新科技有限公司
IPC: G06F8/30
Abstract: 本发明公开了一种基于FQLTL的实例生成方法，本方法获取系统设备集合、设备性质以及设备间关系等配置信息，通过遍历公式的语法树进行逻辑计算，判断每个对象/对象集合是否满足公式中所限定的范围，由最终得到的逻辑运算结果可以滤去恒真/恒假的集合,这些集合都无需进行下一步验证，留下真正需要验证的设备集合，也就是状态不确定的设备集合。包括如下步骤：对公式进行语法解析；预处理；遍历语法树，进行可满足性检查；输出可满足性检查结果。由于验证器无法进行包含范围的性质验证，而这种新的形式化语言中规定了需要验证集合的范围。故本发明解决了在验证项目中，从系统全部的设备集合缩减到真正待验证实例的问题。
-
公开(公告)号：CN114564202B
公开(公告)日：2023-02-17
申请号：CN202210038442.X
申请日：2022-01-13
Applicant: 华东师范大学 , 上海工业控制安全创新科技有限公司
IPC: G06F8/41
Abstract: 本发明公开了一种基于SAT求解器的符号模型检测方法：读取待检测文件，将待检测文件解析为C++程序中对应的数据结构存储用于后续步骤，得到待检测模型M和待检测安全性性质P，将待检测安全性质P取反得到不安全性性质bad；待检测安全性性质P由线性时态逻辑编写；将待检测模型M蕴含的状态以及状态间的迁移关系构造为文字和等价的子句，存入SAT求解器供后续步骤使用；将当前状态si以及不安全性性质bad作为假设，在待检测模型M的子句集合约束下进行求解，若公式可满足，则从当前状态si可以一步到达违反安全性质的坏状态；从初始状态到坏状态的路径，即为目击者或反例，作为证明系统不安全的证据。
-
公开(公告)号：CN114564202A
公开(公告)日：2022-05-31
申请号：CN202210038442.X
申请日：2022-01-13
Applicant: 华东师范大学 , 上海工业控制安全创新科技有限公司
IPC: G06F8/41
Abstract: 本发明公开了一种基于SAT求解器的符号模型检测方法：读取待检测文件，将待检测文件解析为C++程序中对应的数据结构存储用于后续步骤，得到待检测模型M和待检测安全性性质P，将待检测安全性质P取反得到不安全性性质bad；待检测安全性性质P由线性时态逻辑编写；将待检测模型M蕴含的状态以及状态间的迁移关系构造为文字和等价的子句，存入SAT求解器供后续步骤使用；将当前状态si以及不安全性性质bad作为假设，在待检测模型M的子句集合约束下进行求解，若公式可满足，则从当前状态si可以一步到达违反安全性质的坏状态；从初始状态到坏状态的路径，即为目击者或反例，作为证明系统不安全的证据。
-
公开(公告)号：CN115906482A
公开(公告)日：2023-04-04
申请号：CN202211464467.2
申请日：2022-11-22
Applicant: 上海工业控制安全创新科技有限公司
IPC: G06F30/20 , G06F111/04
Abstract: 本发明涉及一种铁路站场图自动生成方法及装置。该方法包括：步骤S1，获取站场拓扑数据；步骤S2，建立对站场拓扑数据进行解析得到的站场二叉树数据结构；步骤S3，根据站场二叉树数据结构生成站场图，其中，站场拓扑数据包括多个站场元素的站场元素数据，站场元素包括区段、道岔、信号机、绝缘节以及端点，步骤S3包括：步骤S3‑1，通过对站场二叉树数据结构进行前序遍历，将站场拓扑数据按照行进行划分，并基于预设道岔对行约束规则进行预排序；步骤S3‑2，进行断行拼接；步骤S3‑3，根据每一行中所有道岔的方向对所有行的顺序进行优化调整；步骤S3‑4，删除每一行中多余的站场元素；步骤S3‑5，对每一行中的每一个站场元素的横坐标进行赋值；步骤S3‑6绘制站场图。
-
Patent Agency Ranking
公开(公告)号：CN118862765A
公开(公告)日：2024-10-29
申请号：CN202410836706.5
申请日：2024-06-26
Applicant: 华东师范大学
IPC: G06F30/33 , G06F119/06
Abstract: 本发明公开了一种多线程的VCD文件数据统计工具及其应用方法，属于电子数字技术领域。其结构包括读取VCD文件定义部分、并行读取VCD文件数据部分和计算并输出结果部分。其方法包括读取VCD文件定义部分；根据var_to_number将信号转为对应信号序号；根据var_to_number将信号转为信号标志，根据var_output_name将信号序号转为信号真实名称；对数据进行解析和统计，通过计算得到反转率并直接将信号输出到表格中。本发明采通过本工具使用数据统计的方式来获取各个信号的翻转率进而方便开发人员计算动态功耗。并且采用并行读取的方式进行统计，在数据量较大的情况下会拥有更高的性能，运行时间更短。
-
公开(公告)号：CN117312722A
公开(公告)日：2023-12-29
申请号：CN202311222434.1
申请日：2023-09-21
Applicant: 华东师范大学
Abstract: 本发明公开了一种基于SMT求解器的多系统任务规划方法，涉及自动化任务规划和调度领域，包括以下步骤：S1：对输入的任务序列进行解析；S2：信息预处理，根据输入的任务序列以及要求输出的序列生成相应的指令模板；S3：子系统建模，生成待求解的初始指令序列；S4：通过交互式工具将自然语言约束转化为符合要求的一阶谓词逻辑公式，并通过Z3库函数添加到SMT求解器中；S5：SMT求解器进行约束求解，子系统的约束加入到SMT求解中后，调用Solver.check(self,*assumptions)方法即可完成求解；S6：根据SMT求解器返回的结果，对任务序列进行分析，生成最终的指令序列。本发明将自然语言约束转化为一阶谓词逻辑公式，通过SMT求解器进行求解，并对结果进行解析，最终得到符合条件的指令序列。
-
公开(公告)号：CN117812085B
公开(公告)日：2024-08-27
申请号：CN202310528285.5
申请日：2023-05-11
Applicant: 华东师范大学
IPC: H04L67/1042 , G06Q20/38 , G06Q20/42 , G06Q40/04
Abstract: 本发明公开了一种基于DAG的混合型区块链共识方法，属于区块链共识协议技术领域，包括以下步骤：(1)使用POW机制对交易进行打包出块，以DPOS机制与PBFT机制相融合的机制来进行交易确认的新型区块链共识协议架构；(2)在核心的交易确认阶段，设计主链区块确定算法。本发明采用上述机制的一种基于DAG的混合型区块链共识方法，采用DPOS与PBFT结合的方法，避免了资源浪费；交易一旦确认不可逆转，保证了区块链的安全性；去中心化的特性相比于传统POS，DPOS机制得到了加强，从根本上杜绝了超级节点的出现，具有很高的去中心化特性与安全性。
-
公开(公告)号：CN117312722B
公开(公告)日：2024-03-19
申请号：CN202311222434.1
申请日：2023-09-21
Applicant: 华东师范大学
Abstract: 本发明公开了一种基于SMT求解器的多系统任务规划方法，涉及自动化任务规划和调度领域，包括以下步骤：S1：对输入的任务序列进行解析；S2：信息预处理，根据输入的任务序列以及要求输出的序列生成相应的指令模板；S3：子系统建模，生成待求解的初始指令序列；S4：通过交互式工具将自然语言约束转化为符合要求的一阶谓词逻辑公式，并通过Z3库函数添加到SMT求解器中；S5：SMT求解器进行约束求解，子系统的约束加入到SMT求解中后，调用Solver.check(self,*assumptions)方法即可完成求解；S6：根据SMT求解器返回的结果，对任务序列进行分析，生成最终的指令序列。本发明将自然语言约束转化为一阶谓词逻辑公式，通过SMT求解器进行求解，并对结果进行解析，最终得到符合条件的指令序列。
-
公开(公告)号：CN117812085A
公开(公告)日：2024-04-02
申请号：CN202310528285.5
申请日：2023-05-11
Applicant: 华东师范大学
IPC: H04L67/1042 , G06Q20/38 , G06Q20/42 , G06Q40/04
Abstract: 本发明公开了一种基于DAG的混合型区块链共识方法，属于区块链共识协议技术领域，包括以下步骤：(1)使用POW机制对交易进行打包出块，以DPOS机制与PBFT机制相融合的机制来进行交易确认的新型区块链共识协议架构；(2)在核心的交易确认阶段，设计主链区块确定算法。本发明采用上述机制的一种基于DAG的混合型区块链共识方法，采用DPOS与PBFT结合的方法，避免了资源浪费；交易一旦确认不可逆转，保证了区块链的安全性；去中心化的特性相比于传统POS，DPOS机制得到了加强，从根本上杜绝了超级节点的出现，具有很高的去中心化特性与安全性。
-
-
-
-
-
-
-
-
-
Search Results
10
records
(took 0.09 seconds)
