买专利卖专利找龙图腾，真高效！ 查专利查商标用IPTOP,全免费！专利年费监控用IP管家,真方便！

龙图腾网获悉同济大学申请的专利一种分布式数据库系统数据不一致检测方法及系统获国家发明授权专利权，本发明授权专利权由国家知识产权局授予，授权公告号为：CN116894042B 。

龙图腾网通过国家知识产权局官网在2025-12-23发布的发明授权授权公告中获悉：该发明授权的专利申请号/专利号为：202310635440.3，技术领域涉及：G06F16/23；该发明授权一种分布式数据库系统数据不一致检测方法及系统是由刘关俊;宋健设计研发完成，并于2023-05-31向国家知识产权局提交的专利申请。

本一种分布式数据库系统数据不一致检测方法及系统在说明书摘要公布了：本发明公开了分布式数据库系统数据不一致检测方法及系统包括，将分布式数据库系统进行抽象建模，形成PDT‑net模型；通过所述PDT‑net模型中的变迁使能条件和发生规则生成对应的状态可达图；基于模型检测思想，将数据不一致定义转换成对应的计算树逻辑公式；利用所述生成的状态可达图，遍历所述计算树逻辑公式中所有的状态，寻找数据不一致的变迁集和状态集；本发明通过将分布式数据库系统转换成对应的PDT‑net模型，变迁上绑定与数据库操作的语义，以此模拟出数据库系统中对各个活动的操作，并生成该PDT‑net的状态可达图；同时基于PDT‑net下的数据不一致错误检测算法，遍历可达图中所有的状态，能够更加精确的找到数据不一致的错误。

本发明授权一种分布式数据库系统数据不一致检测方法及系统在权利要求书中公布了：1.一种分布式数据库系统数据不一致检测方法，其特征在于，包括： 将分布式数据库系统进行抽象建模，形成PDT-net模型； 根据分布式数据库系统的结构特征以及数据操作特征，从控制流和数据流的角度分析，并用带数据和表操作的Petri网进行建模； 其中，Petri网的定义为N‘＝P,T,F,D,R,rd,wt,dt,opt,sel,ins,del,upd；P表示库所的有限集合；T＝TM∪TW表示变迁的有限集合，TM表示主内存变迁集合，TW是工作内存变迁集合并且表示为弧的集合；D＝{d1,d2,…,dk}是一个有限数据元素集合；表示一个包含m个初始表的集合，每个初始表都包含n条记录，第j个表中的一个记录Rjri＝{d1,d2,…,dk}由k个属性值组成，di表示为记录中的第i个属性值；j∈{1,2,…,m},i∈{1,2,…,k}； 通过所述PDT-net模型中的变迁使能条件和发生规则生成对应的状态可达图； 基于模型检测思想，将数据不一致定义转换成对应的计算树逻辑公式； 计算树逻辑公式表示为： 若判定结果为真，则说明存在数据不一致状态错误；此时，需要记录对应的数据不一致状态集合；否则，说明不存在数据不一致错误； 其中，E表示存在某些路径；F表示从某状态起始路径中的某个状态开始；X表示从某状态起始路径中的第二个状态开始；此公式含义为，存在并发路径，在该并发路径上的将来状态中会存在变迁t1和t2在状态c1和c2下都有发生权，则变迁t1和t2都是关于数据项d的操作，产生的结果是同一个数据项d在不同状态表中产生的数值是不相等的；wt为在主内存中写数据项的标签函数，rd为在主内存中读数据项的标签函数，dt为在主内存中删除数据项的标签函数，sel为在表中选择记录的标签函数，ins为在表中插入记录的标签函数，del为在表中删除记录的标签函数，upd为在表中更新记录的标签函数；变迁t∈T在状态是使能的，记作c[t，m是N‘的标识函数；θD:D→{⊥,T}表示当前状态下为每个数据元素d∈D的赋值一个定义值T或未定义值⊥；在初始状态下，每个数据元素是未定义值⊥；当对某个数据元素执行读或写操作时，该数据元素就被赋一个值，表示它是定义值T；如果对某个数据元素执行删除操作，该数据元素将是未定义值⊥；表示当前表中每个数据项值的赋值状态，也就是定义值T或者未定义值⊥；如果表中记录的数据项值没有被赋值，则该数据项是未定义值⊥；当对表中记录的数据项值执行更新或者插入操作，说明该数据项值被赋值一个定义值T； 利用所述生成的状态可达图，遍历所述计算树逻辑公式中所有的状态，寻找数据不一致的变迁集和状态集。

如需购买、转让、实施、许可或投资类似专利技术，可联系本专利的申请人或专利权人同济大学，其通讯地址为：200092 上海市杨浦区四平路1239号；或者联系龙图腾网官方客服，联系龙图腾网可拨打电话0551-65771310或微信搜索“龙图腾网”。

以上内容由龙图腾AI智能生成。