一种分布式数据库系统数据不一致检测方法及系统

1.本发明涉及模型流程信息技术领域，尤其涉及一种分布式数据库系统数据不一致检测方法及系统。


背景技术：

2.随着互联网技术和大数据的快速发展，传统的集中式数据库系统难以满足高并发事务处理的需求，分布式数据库系统的并发控制能够保证多个事务高效，正确执行，实现系统的自动化支持和协作运行，降低成本并提高效率。在日常生活中有着广泛的应用，如:云计算，智慧医疗以及智能轨道交通等领域。然而，在实际的分布式数据库系统中，由于各事务间存在大量的数据交互和并发数据操作(读、写、删除)。尤其在分布式数据库系统中，共享变量通常是多个表公用的变量，如果在执行过程中存在不合理的数据操作，修改共享变量之后，其它关联此共享变量的数据库表中该值没有得到及时的更新，则容易产生数据不一致，从而引发系统错误。因此，如何确保此类系统的安全性和高可靠性是当下研究热点。
3.目前已有一些研究基于petri网检测工作流系统中存在的数据不一致错误。von stackelberg等人给出一种检测bpmn工作流模型中存在数据不一致方法。他们将bpmn工作流模型映射到petri网并定义一组关于bpmn工作流模型数据流错误的反模式，利用计算树逻辑公式(computation tree logic,ctl)来形式化bpmn的反模式并利用工具对ctl公式进行验证。有相关学者提出基于petri网给出了数据不一致错误的基本定义，通过建立活动数据关联矩阵检测模型中存在的数据流不一致错误实际的工作流模型中某些路由选择依赖于特定的数据元素，实际的工作流模型中某些路由选择依赖于特定的数据元素，由此说明在某些工作流模型中活动的正确执行不仅取决于控制流，同时还依赖于数据流。如果因流程设计缺陷或工作人员操作的不当使得数据流本身就是错误的，针对这类问题。有研究给出了更为精炼的方法对数据流建模并给出对应的数据不一致检测方法，提高模型的正确性验证。上述的研究虽然在一定程度上可以解决数据不一致检测问题，但是检测方法通常都是基于抽象的数据元素操作(读、写、删除)或者对活动的执行情况(输入、输出)进行判断的，简单来说就是只能定性去分析数据不一致错误。该方法存在的缺点就是容易产生误报和漏报的情况发生。
4.另一方面，对于数据库表的研究大多数都是面向单个数据库表的研究，对于分布式数据库系统中存在的多表交互和各数据库表间的数据操作，已有的建模方法不足以刻画和表达。同时，已有的数据不一致检测方法都是基于状态可达图进行的，通过遍历所有状态的可达路径，检测不合理的数据操作，从而定性的分析出错误。而分布式数据库系统中的很多事务间的活动都是基于都后台的数据库表或共享变量的操作。因此，传统的检测数据不一致错误方法仅从数据访问层(读，写，删除)或活动的控制层(输入，输出)是不严谨的，容易出现误判和漏判的结果。主要原因是目前对分布式数据库系统形式化建模时，研究人员要么以模型中活动为中心，从控制流层面考虑流程活动中数据的输入或输出，要么以数据为中心从数据流层面考虑各数据元素的执行操作(读，写，删除)。
5.为了解决这种问题，需要给出一种更为细化的模型去描述分布式数据库系统，该模型不仅能够从控制流角度去刻画系统中活动数据，同时还能从数据流角度更加细致的描述持久层数据中具体数据项值的操作。在检测数据不一致错误时，我们利用数据项操作以及对应的数据项值变化检测出数据不一致状态,从而能够从定性和定量二个维度准确判断出数据不一致错误，以弥补传统方法存在的漏报和误报情况发生。


技术实现要素：

6.本部分的目的在于概述本发明的实施例的一些方面以及简要介绍一些较佳实施例。在本部分以及本技术的说明书摘要和发明名称中可能会做些简化或省略以避免使本部分、说明书摘要和发明名称的目的模糊，而这种简化或省略不能用于限制本发明的范围。
7.鉴于上述现有存在的问题，提出了本发明。因此，本发明提供了分布式数据库系统数据不一致检测方法，用来解决实际问题中，传统检测数据存在漏报和误报的问题。
8.为解决上述技术问题，本发明提供如下技术方案：
9.第一方面，本发明提供了分布式数据库系统数据不一致检测方法，包括：
10.将分布式数据库系统进行抽象建模，形成pdt-net模型；
11.通过所述pdt-net模型中的变迁使能条件和发生规则生成对应的状态可达图；
12.基于模型检测思想，将数据不一致定义转换成对应的计算树逻辑公式；
13.利用所述生成的状态可达图，遍历所述计算树逻辑公式中所有的状态，寻找数据不一致的变迁集和状态集。
14.作为本发明所述的分布式数据库系统数据不一致检测方法的一种优选方案，其中：形成pdt-net模型，包括：
15.根据分布式数据库系统的结构特征以及数据操作特征，从控制流和数据流的角度分析，并用带数据和表操作的petri网进行建模；
16.其中，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个表中的一个记录rj(ri)＝{d1,d2,...,dk}是由k个属性值组成，di表示为记录中的第i个属性值；j∈{1,2,...,m},i∈{1,2,...,k}。
17.作为本发明所述的分布式数据库系统数据不一致检测方法的一种优选方案，其中：变迁使能条件，包括：
18.所述变迁由三部分组成分别为，具体的活动名称，对抽象数据元素的操作，对具体数据项值的操作；
19.其中，具体的活动名称指的是当前变迁t对应的活动名字；对抽象数据元素的操作指的是对当前活动中的数据执行读、写、删除操作；对具体数据项值的操作指的是对当前活动中与表关联的数据项执行选择、插入、删除、更新操作。
20.作为本发明所述的分布式数据库系统数据不一致检测方法的一种优选方案，其
中：将数据不一致定义转换成对应的计算树逻辑公式，包括：
21.计算树逻辑公式表示为：
[0022][0023]
若判定结果为真，则说明存在数据不一致状态错误；此时，需要记录对应的数据不一致状态集合；否则，说明不存在数据不一致错误；
[0024]
其中，e表示存在某些路径；f表示从某状态起始路径中的某个状态开始；x表示从某状态起始路径中的第二个状态开始；此公式含义为，存在并发路径，在该并发路径上的将来状态中会存在变迁t1和t2在状态c1和c2下都有发生权，则变迁t1和t2都是关于数据项d的操作，产生的结果是同一个数据项d在不同状态表中产生的数值是不相等的；wt为在主内存中写数据项的标签函数，rd为在主内存中读数据项的标签函数，dt为在主内存中删除数据项的标签函数，sel为在表中选择记录的标签函数，ins为在表中插入记录的标签函数，del为在表中删除记录的标签函数，upd为在表中更新记录的标签函数；变迁t∈t在状态是使能的，记作m是n
‘
的标识函数；θd:d
→
{
⊥
,t}表示当前状态下为每个数据元素d∈d的赋值一个定义值(t)或未定义值(
⊥
)；在初始状态下，每个数据元素是未定义值(
⊥
)；当对某个数据元素执行读或写操作时，该数据元素就被赋一个值，表示它是定义值(t)；如果对某个数据元素执行删除操作，该数据元素将是未定义值(
⊥
)；r
→
{
⊥
,t}表示当前表中每个数据项值的赋值状态，也就是定义值(t)或者未定义值(
⊥
)；如果表中记录的数据项值没有被赋值，则该数据项是未定义值(
⊥
)；当对表中记录的数据项值执行更新或者插入操作，说明该数据项值被赋值一个定义值(t)。
[0025]
作为本发明所述的分布式数据库系统数据不一致检测方法的一种优选方案，其中：利用所述生成的状态可达图，遍历所述计算树逻辑公式中所有的状态，寻找数据不一致的变迁集和状态集，包括：
[0026]
定义数据不一致错误下的变迁集sat(di)，数据不一致状态集sat(c_di)，以及存放并发关系的变迁集sat(t||
co
)，同时将这些集合分别进行初始化处理。
[0027]
作为本发明所述的分布式数据库系统数据不一致检测方法的一种优选方案，其中：同时将这些集合分别进行初始化处理，包括：
[0028]
将系统中所有处于并发关系的变迁对(t1,t2)存储到sat(t||
co
)，依次选取从集合sat(t||
co
)选取变迁对；如果变迁上绑定的数据操作以及对应的数据项值都是对同一个数据项执行数据操作，则说明该变迁对之间发生数据不一致错误；否则，就不存在数据不一致错误；当判定变迁对对同一个数据项执行数据操作时，依据数据不一致错误定义公式进一步判断是否符合数据不一致错误。
[0029]
作为本发明所述的分布式数据库系统数据不一致检测方法的一种优选方案，其中：所述数据不一致错误定义的公式，包括：
[0030]
数据不一致错误定义的公式表示为：
[0031]
[0032]
当变迁对(t1,t2)对同一个数据项值操作满足数据不一致错误定义公式时，则说明存在数据不一致错误；迭代初始化处理操作，直至集合sat(t||
co
)中所有的变迁对查询完毕。
[0033]
第二方面，本发明提供了一种分布式数据库系统数据不一致检测系统，其包括：
[0034]
预处理存储模块，用于存储表数据，同时可以对变迁集和状态集进行初始化处理；
[0035]
建模模块，用于对分布式数据库系统进行抽象建模；
[0036]
判断检测模块，用于对数据不一致性进行判断，从而检测数据的不一致错误。
[0037]
第三方面，本发明提供了一种计算机设备，包括存储器和处理器，所述存储器存储有计算机程序，其中：所述处理器执行所述计算机程序时实现上述方法的任一步骤。
[0038]
第四方面，本发明提供了一种计算机可读存储介质，其上存储有计算机程序，其中：所述计算机程序被处理器执行时实现上述方法的任一步骤。
[0039]
与现有技术相比，发明有益效果为：本发明通过将分布式数据库系统转换成对应的pdt-net模型，变迁上绑定与数据库操作的语义，以此模拟出数据库系统中对各个活动的操作，并生成该pdt-net的状态可达图；同时基于pdt-net下的数据不一致错误检测算法，遍历可达图中所有的状态，能够更加精确的找到数据不一致的错误。
附图说明
[0040]
为了更清楚地说明本发明实施例的技术方案，下面将对实施例描述中所需要使用的附图作简单地介绍，显而易见地，下面描述中的附图仅仅是本发明的一些实施例，对于本领域普通技术人员来讲，在不付出创造性劳动性的前提下，还可以根据这些附图获得其它的附图。其中：
[0041]
图1为本发明一个实施例所述的分布式数据库系统数据不一致检测方法的实施流程图；
[0042]
图2为本发明一个实施例所述的分布式数据库系统数据不一致检测方法的整体系统流程图；
[0043]
图3为本发明一个实施例所述的分布式数据库系统数据不一致检测方法的数据不一致检测示意图；
[0044]
图4为本发明一个实施例所述的分布式数据库系统数据不一致检测方法的pdt-net结构示意图；
[0045]
图5为本发明一个实施例所述的分布式数据库系统数据不一致检测方法的开发工具展示图。
具体实施方式
[0046]
为使本发明的上述目的、特征和优点能够更加明显易懂，下面结合说明书附图对本发明的具体实施方式做详细的说明，显然所描述的实施例是本发明的一部分实施例，而不是全部实施例。基于本发明中的实施例，本领域普通人员在没有做出创造性劳动前提下所获得的所有其他实施例，都应当属于本发明的保护的范围。
[0047]
在下面的描述中阐述了很多具体细节以便于充分理解本发明，但是本发明还可以采用其他不同于在此描述的其它方式来实施，本领域技术人员可以在不违背本发明内涵的
情况下做类似推广，因此本发明不受下面公开的具体实施例的限制。
[0048]
其次，此处所称的“一个实施例”或“实施例”是指可包含于本发明至少一个实现方式中的特定特征、结构或特性。在本说明书中不同地方出现的“在一个实施例中”并非均指同一个实施例，也不是单独的或选择性的与其他实施例互相排斥的实施例。
[0049]
本发明结合示意图进行详细描述，在详述本发明实施例时，为便于说明，表示器件结构的剖面图会不依一般比例作局部放大，而且所述示意图只是示例，其在此不应限制本发明保护的范围。此外，在实际制作中应包含长度、宽度及深度的三维空间尺寸。
[0050]
同时在本发明的描述中，需要说明的是，术语中的“上、下、内和外”等指示的方位或位置关系为基于附图所示的方位或位置关系，仅是为了便于描述本发明和简化描述，而不是指示或暗示所指的装置或元件必须具有特定的方位、以特定的方位构造和操作，因此不能理解为对本发明的限制。此外，术语“第一、第二或第三”仅用于描述目的，而不能理解为指示或暗示相对重要性。
[0051]
本发明中除非另有明确的规定和限定，术语“安装、相连、连接”应做广义理解，例如：可以是固定连接、可拆卸连接或一体式连接；同样可以是机械连接、电连接或直接连接，也可以通过中间媒介间接相连，也可以是两个元件内部的连通。对于本领域的普通技术人员而言，可以具体情况理解上述术语在本发明中的具体含义。
[0052]
实施例1
[0053]
参照图1至图3，为本发明第一个实施例，该实施例提供了一种分布式数据库系统数据不一致检测方法，包括：
[0054]
将分布式数据库系统进行抽象建模，形成pdt-net模型；
[0055]
进一步的，形成pdt-net模型，包括：
[0056]
根据分布式数据库系统的结构特征以及数据操作特征，从控制流和数据流的角度分析，并用带数据和表操作的petri网进行建模；
[0057]
通过所述pdt-net模型中的变迁使能条件和发生规则生成对应的状态可达图；
[0058]
进一步的，关于pdt-net的定义、状态以及变迁使能条件和发生规则解释如下：
[0059]
pdt-net的定义为n
‘
＝(p,t,f,d,r,rd,wt,dt,opt,sel,ins,del,upd)；
[0060]
其中，p是库所的有限集合，t＝tm∪tw是变迁的有限集合，tm是主内存变迁集合，tw是工作内存变迁集合，并且是工作内存变迁集合，并且是弧的集合；d＝{d1,d2,
…
,dk}是一个有限的数据元素集合；}是一个有限的数据元素集合；是一个包含m个初始表的集合,每个初始表都包含n条记录.第j个表中的一个记录rj(ri)＝{d1,d2,...,dk}由k个属性值组成，di表示记录中的第i个属性值，j∈{1,2,...,m},i∈{1,2,...,k}；rd:tm→2d
是一个在主内存中读数据项的标签函数；wt:tm→2d
是一个在主内存中写数据项的标签函数；dt:tm→2d
是一个在主内存中删除数据项的标签函数；opt:tw→2d
是一个在工作内存中计算数据项的标签函数；sel:是一个在表中选择记录的标签函数；ins:是一个在表中插入记录的标签函数；del:是一个在表中删除记录的标签函数；upd:是一个在表中更新记录的标签函
数；
[0061]
pdt-net的状态为：m是n
‘
的标识函数；θd:d
→
{
⊥
,t}表示当前状态下为每个数据元素d∈d的赋值一个定义值(t)或未定义值(
⊥
)；在初始状态下，每个数据元素是未定义值(
⊥
)；当对某个数据元素执行读或写操作时，该数据元素就被赋一个值，表示它是定义值(t)；如果对某个数据元素执行删除操作，该数据元素将是未定义值(
⊥
)；r
→
{
⊥
,t}表示当前表中每个数据项值的赋值状态，也就是定义值(t)或者未定义值(
⊥
)；如果表中记录的数据项值没有被赋值，则该数据项是未定义值(
⊥
)；当对表中记录的数据项值执行更新或者插入操作，说明该数据项值被赋值一个定义值(t)；
[0062]
应当说明的是，通常在pdt-net中，给定的初始表是被定义的，也就是说表中的每个数据项的值都是一个定义值(t)；
[0063]
pdt-net的变迁使能条件和发生规则为：
[0064]
设定n
‘
是一个pdt-net，变迁t∈t在状态是使能的，记作c[t》，且使能满足条件如下：
[0065]
(1)
[0066]
(2)
[0067]
(3)
[0068]
(4)
[0069][0070]
应当说明的是，如果变迁t在c下是使能的，则可以引发t，并得到一个新的状态记作c[t》c'，其中c'满足条件如下
[0071]
(1)m[t》m
′
；
[0072]
(2)
[0073]
(3)
[0074]
(4)
[0075]
(5)(5)
[0076]
(6)(6)
[0077]
(7)(7)
[0078]
(8)(8)
[0079]
(9)
[0080]
(10)
[0081]
(11)(11)
[0082]
(12)(12)
[0083]
基于模型检测思想，将数据不一致定义转换成对应的计算树逻辑公式；
[0084]
进一步的，计算树逻辑公式表示为：
[0085][0086]
若判定结果为真，则说明存在数据不一致状态错误；此时，需要记录对应的数据不一致状态集合；否则，说明不存在数据不一致错误；
[0087]
其中，e表示存在某些路径；f表示从某状态起始路径中的某个状态开始；x表示从某状态起始路径中的第二个状态开始；此公式含义为，存在并发路径，在该并发路径上的将来状态中会存在变迁t1和t2在状态c1和c2下都有发生权，则变迁t1和t2都是关于数据项d的操作，产生的结果是同一个数据项d在不同状态表中产生的数值是不相等的；
[0088]
利用所述生成的状态可达图，遍历所述计算树逻辑公式中所有的状态，寻找数据不一致的变迁集和状态集，包括：定义数据不一致错误下的变迁集sat(di)，数据不一致状态集sat(c_di)，以及存放并发关系的变迁集sat(t||
co
)，同时将这些集合分别进行初始化处理；
[0089]
进一步的，初始化处理包括，将系统中所有处于并发关系的变迁对(t1,t2)存储到sat(t||
co
)，依次选取从集合sat(t||
co
)选取变迁对；如果变迁上绑定的数据操作以及对应的数据项值都是对同一个数据项执行数据操作，则说明该变迁对之间发生数据不一致错误；否则，就不存在数据不一致错误；当判定变迁对对同一个数据项执行数据操作时，依据数据不一致错误定义公式进一步判断是否符合数据不一致错误；
[0090]
进一步的，数据不一致错误定义的公式表示为：
[0091][0092]
当变迁对(t1,t2)对同一个数据项值操作满足数据不一致错误定义公式时，则说明存在数据不一致错误；迭代初始化处理操作，直至集合sat(t||
co
)中所有的变迁对查询完毕。
[0093]
进一步的，本实施例还提供一种分布式数据库系统数据不一致检测系统，包括：
[0094]
预处理存储模块，用于存储表数据，同时可以对变迁集和状态集进行初始化处理；
[0095]
建模模块，用于对分布式数据库系统进行抽象建模；
[0096]
判断检测模块，用于对数据不一致性进行判断，从而检测数据的不一致错误。
[0097]
本实施例还提供一种计算机设备，适用于分布式数据库系统数据不一致检测方法的情况，包括：
[0098]
存储器和处理器；存储器用于存储计算机可执行指令，处理器用于执行计算机可执行指令，实现如上述实施例提出的分布式数据库系统数据不一致检测方法。
[0099]
该计算机设备可以是终端，该计算机设备包括通过系统总线连接的处理器、存储器、通信接口、显示屏和输入装置。其中，该计算机设备的处理器用于提供计算和控制能力。该计算机设备的存储器包括非易失性存储介质、内存储器。该非易失性存储介质存储有操作系统和计算机程序。该内存储器为非易失性存储介质中的操作系统和计算机程序的运行提供环境。该计算机设备的通信接口用于与外部的终端进行有线或无线方式的通信，无线方式可通过wifi、运营商网络、nfc(近场通信)或其他技术实现。该计算机设备的显示屏可以是液晶显示屏或者电子墨水显示屏，该计算机设备的输入装置可以是显示屏上覆盖的触摸层，也可以是计算机设备外壳上设置的按键、轨迹球或触控板，还可以是外接的键盘、触控板或鼠标等。
[0100]
本实施例还提供一种存储介质，其上存储有计算机程序，该程序被处理器执行时实现如上述实施例提出的分布式数据库系统数据不一致检测方法。
[0101]
本实施例提出的存储介质与上述实施例提出的数据存储方法属于同一发明构思，未在本实施例中详尽描述的技术细节可参见上述实施例，并且本实施例与上述实施例具有相同的有益效果。
[0102]
实施例2
[0103]
参照图4，为本发明第二个实施例，该实施例提供了一种分布式数据库系统数据不一致检测方法，包括：
[0104]
pdt-net模型底层是以petri-net为基础对分布式数据库系统中的控制流进行建模；数据流层面，在变迁上绑定了对抽象数据元素的操作，包括对活动上的数据执行读(wt)、写(rd)、删除(dt)操作；为了描述对后台数据库表中的数据项值的操作，在变迁上绑定了对具体数据项值的操作，包括对数据项值的更新(upd)、插入(sel)、删除(del)、选择(sel)操作，从而实现了对数据库表中数据项的操作。
[0105]
实施例3
[0106]
参照图5，为本发明第三个实施例，该实施例提供了分布式数据库系统数据不一致检测方法，包括：
[0107]
利用开发的工具对该模型中存在的数据不一致错误进行检测；
[0108]
首先，需要将这些信息存储在.txt文件中，在输入.txt文件中描述的pdt-net后，工具可以读取文本中的信息，并生成对应的状态可达图，包括产生的状态数量，弧的数量以及生成状态可达图所需的时间；可以看到在活动t0处，对抽象的数据元素id执行写(wt)操作，在数据库表中对表中具体的数据项值id执行选择(sel)操作；图5(a)显示了一个关于在线网购的pdt-net模型；图5(b)显示买方的初始表信息；图5(c)显示卖方的初始表信息；图5(d)给出数据不一致的逻辑公式；图5(e)展示了生成的状态可达图结果以及数据不一致检测结果；从图5(e)的实验结果来看，产生203个状态和469个弧，并且一共产生了32对数据不一致错误状态。
[0109]
应说明的是，以上实施例仅用以说明本发明的技术方案而非限制，尽管参照较佳
实施例对本发明进行了详细说明，本领域的普通技术人员应当理解，可以对本发明的技术方案进行修改或者等同替换，而不脱离本发明技术方案的精神和范围，其均应涵盖在本发明的权利要求范围当中。

技术特征：
1.一种分布式数据库系统数据不一致检测方法，其特征在于，包括：将分布式数据库系统进行抽象建模，形成pdt-net模型；通过所述pdt-net模型中的变迁使能条件和发生规则生成对应的状态可达图；基于模型检测思想，将数据不一致定义转换成对应的计算树逻辑公式；利用所述生成的状态可达图，遍历所述计算树逻辑公式中所有的状态，寻找数据不一致的变迁集和状态集。2.如权利要求1所述的分布式数据库系统数据不一致检测方法，其特征在于，形成pdt-net模型，包括：根据分布式数据库系统的结构特征以及数据操作特征，从控制流和数据流的角度分析，并用带数据和表操作的petri网进行建模；其中，petri网的定义为n
‘
＝(p,t,f,d,r,rd,wt,dt,opt,sel,ins,del,upd)；p表示库所的有限集合；t＝t
m
∪t
w
表示变迁的有限集合，t
m
表示主内存变迁集合，t
w
是工作内存变迁集合并且集合并且表示为弧的集合；d＝{d1,d2,
…
,d
k
}是一个有限数据元素集合；有限数据元素集合；表示一个包含m个初始表的集合，每个初始表都包含n条记录，第j个表中的一个记录r
j
(r
i
)＝{d1,d2,...,d
k
}由k个属性值组成，d
i
表示为记录中的第i个属性值；j∈{1,2,...,m},i∈{1,2,...,k}。3.如权利要求2所述的分布式数据库系统数据不一致检测方法，其特征在于，变迁使能条件，包括：所述变迁由三部分组成分别为，具体的活动名称，对抽象数据元素的操作，对具体数据项值的操作；其中，具体的活动名称指的是当前变迁t对应的活动名字；对抽象数据元素的操作指的是对当前活动中的数据执行读、写、删除操作；对具体数据项值的操作指的是对当前活动中与表关联的数据项执行选择、插入、删除、更新操作。4.如权利要求2或3所述的分布式数据库系统数据不一致检测方法，其特征在于，将数据不一致定义转换成对应的计算树逻辑公式，包括：计算树逻辑公式表示为：若判定结果为真，则说明存在数据不一致状态错误；此时，需要记录对应的数据不一致状态集合；否则，说明不存在数据不一致错误；其中，e表示存在某些路径；f表示从某状态起始路径中的某个状态开始；x表示从某状态起始路径中的第二个状态开始；此公式含义为，存在并发路径，在该并发路径上的将来状态中会存在变迁t1和t2在状态c1和c2下都有发生权，则变迁t1和t2都是关于数据项d的操作，产生的结果是同一个数据项d在不同状态表中产生的数值是不相等的；wt为在主内存中写数据项的标签函数，rd为在主内存中读数据项的标签函数，dt为在主内存中删除数据项的标签函数，sel为在表中选择记录的标签函数，ins为在表中插入记录的标签函数，del为在
表中删除记录的标签函数，upd为在表中更新记录的标签函数；变迁t∈t在状态表中删除记录的标签函数，upd为在表中更新记录的标签函数；变迁t∈t在状态是使能的，记作c[t>，m是n
‘
的标识函数；表示当前状态下为每个数据元素d∈d的赋值一个定义值或未定义值(
⊥
)；在初始状态下，每个数据元素是未定义值(
⊥
)；当对某个数据元素执行读或写操作时，该数据元素就被赋一个值，表示它是定义值如果对某个数据元素执行删除操作，该数据元素将是未定义值(
⊥
)；表示当前表中每个数据项值的赋值状态，也就是定义值或者未定义值(
⊥
)；如果表中记录的数据项值没有被赋值，则该数据项是未定义值(
⊥
)；当对表中记录的数据项值执行更新或者插入操作，说明该数据项值被赋值一个定义值5.如权利要求4所述的分布式数据库系统数据不一致检测方法，其特征在于，利用所述生成的状态可达图，遍历所述计算树逻辑公式中所有的状态，寻找数据不一致的变迁集和状态集，包括：定义数据不一致错误下的变迁集sat(di)，数据不一致状态集sat(c_di)，以及存放并发关系的变迁集sat(t||
co
)，同时将这些集合分别进行初始化处理。6.如权利要求5所述的分布式数据库系统数据不一致检测方法，其特征在于，同时将这些集合分别进行初始化处理，包括：将系统中所有处于并发关系的变迁对(t1,t2)存储到sat(t||
co
)，依次选取从集合sat(t||
co
)选取变迁对；如果变迁上绑定的数据操作以及对应的数据项值都是对同一个数据项执行数据操作，则说明该变迁对之间发生数据不一致错误；否则，就不存在数据不一致错误；当判定变迁对对同一个数据项执行数据操作时，依据数据不一致错误定义公式进一步判断是否符合数据不一致错误。7.如权利要求6所述的分布式数据库系统数据不一致检测方法，其特征在于，所述数据不一致错误定义的公式，包括：数据不一致错误定义的公式表示为：当变迁对(t1,t2)对同一个数据项值操作满足数据不一致错误定义公式时，则说明存在数据不一致错误；迭代初始化处理操作，直至集合sat(t||
co
)中所有的变迁对查询完毕。8.一种分布式数据库系统数据不一致检测系统，基于权利要求1～7任一所述的分布式数据库系统数据不一致检测方法，其特征在于，包括：预处理存储模块，用于存储表数据，同时可以对变迁集和状态集进行初始化处理；建模模块，用于对分布式数据库系统进行抽象建模；判断检测模块，用于对数据不一致性进行判断，从而检测数据的不一致错误。9.一种计算机设备，包括存储器和处理器，所述存储器存储有计算机程序，其特征在于：所述处理器执行所述计算机程序时实现权利要求1～7任一所述方法的步骤。10.一种计算机可读存储介质，其上存储有计算机程序，其特征在于：所述计算机程序被处理器执行时实现权利要求1～7任一所述方法的步骤。

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


技术研发人员：刘关俊 宋健
受保护的技术使用者：同济大学
技术研发日：2023.05.31
技术公布日：2023/10/19