测试基于模型的数据库抽象方法

理论计算机科学电子笔记264（2010）53-68www.elsevier.com/locate/entcs当前集和缺失集：用于测试反应式系统的数据库作者：Peter Olsen，Kim G.Larsen和ArneSkou1丹麦奥尔堡大学计算机科学系摘要我们提出了一个新的抽象反应系统与数据库交互。 这种抽象是为了用于基于模型的测试我们将数据库抽象为两个集合：存在集和缺失集，并给出了这种抽象的证明。 本文提出了有限状态机的两种扩展：DBFSM和PAFSM。DBFSM是一种结合数据库的FSM形式。 PAFSM是DBFSM的抽象，使用present-absent集. 根据要进行的测试类型，翻译将根据此目的进行调整。 我们说明这种翻译是如何与在场-缺席的抽象相联系的。最后，我们通过一个小例子来说明这种方法，并展示如何使用基于模型的测试工具UPPAAL TRON进行测试。保留字：测试，模型检测，抽象，基于模型的测试1引言测试通常被认为是软件系统中最广泛使用的错误检测技术今天的许多系统都严重依赖于数据库，然而，没有有效的技术来测试系统使用数据库可用。在测试依赖于数据库的系统时会出现几个问题例如，执行的考虑一个需要创建用户的测试用例。如果不首先删除用户，则无法在创建用户后运行此测试用例。另一个问题是存储在这些数据库中的大量数据。最近，自动化技术和正式的方法已经开发的测试。其中一个是基于模型的测试（MBT）[1，6，7]。然而，对数据库系统进行MBT并不是一件小事考虑对整个数据库进行建模，1电子邮件：petur@cs.aau.dk、kgl@cs.aau.dk和ask@cs.aau.dk1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.12.01454P. Olsen等人理论计算机科学电子笔记264（2010）53这需要巨大的模型，实际上是不可能的。为了使MBT适用于测试数据库系统，需要进行一些抽象本文提出了这样一个抽象。我们将数据库建模为两个集合，当前集合和缺席集合。当前集合是数据库中存在的数据的欠近似，并且不存在集合是数据库中不存在的数据的欠近似。这样，我们可以用两个小集合抽象无限数量的数据库为了使基于模型的测试使用这种抽象，我们提出了两种新形式的FSM：DBFSM和PAFSM。我们展示了存在-不存在的抽象用于从DBFSM到PAFSM的转换，以及如何使用PAFSM开发测试规范。此外，我们展示了一个例子，以及如何从这个例子中生成测试用例。在本文中，我们考虑以浅层方式与数据库交互的反应式系统，这意味着不会对数据执行复杂的操作相反，系统可以向数据库插入值或从数据库中删除值，并且系统的控制流程可以取决于值的存在或不存在。我们把这种简单化的观点称为数据库，尽管数据库要复杂得多。本文中的简单视图是一个起点，旨在扩展到更复杂的数据库视图本文的结构如下：第2部分介绍了一些相关的工作。第3节描述了基于模型的测试的两种形式，在线和在线。 第4节至第7节描述了本文的理论部分。首先，解释和证明了在场-缺席抽象。然后解释扩展的有限状态机，并进一步扩展到包括数据库和当前缺失集。DBFSM和PAFSM之间的抽象和转换在第8节中描述。第10节给出了一个简短的例子，第11节结束了本文。2相关工作Ran等人[5，4]在他们称为AutoDBT的系统中提出了类似的方法。他们使用FSM对基于Web的系统进行建模，并将数据库建模为两组，实际数据库和合成数据库。合成数据库包含实际数据库中没有的值，但可用于测试。当测试需要向数据库中输入一些值时，使用合成数据库。这两个数据库类似于我们的present-absent集。然而，它们不同，因为我们只对实际数据库中的一小部分数据建模。此外，测试算法的不同之处在于，AutoDBT生成要在每个测试用例之前执行的保护，以确保数据库处于符合状态，而我们根据实际数据库填充建模数据库，以确保模型始终处于符合状态。Ran等人没有说明如果系统从未进入特定测试用例的符合状态会发生什么。此外，AutoDBT只支持在线测试，而我们的方法支持在线和在线测试。P. Olsen等人理论计算机科学电子笔记264（2010）53553基于模型的测试基于模型的测试起源于Tretmans[6，7]开发的正式方法，并在工具T或 X[8]中实现。这些方法已经由Hessel等人扩展到包括实时。[1]，并在U PPAAL TRON [2]中实现。此外，一些商业的基于UML的工具正在出现，如Qtronic和ATG。尽管本文的方面不直接涉及实时性，但它旨在用于扩展UPPAAL TRON，以允许数据密集型测试系统. UPPAALTRON假设时间自动机作为规范，并支持实时系统的一致性测试。由于本文中提出的抽象在某种程度上取决于目的是在线测试还是在线测试，因此对这两种类型的测试进行了简短的描述3.1在线测试在线测试将测试用例生成和执行合并到一个活动中。测试用例是从模型的模拟中动态地导出的，并直接发送到被测实现（IUT）。观察IUT的输出，并相应地更新模型的状态。在线测试的优点包括更容易处理非确定性和减少状态空间。非确定性更容易处理，因为IUT是动态观察的，从而揭示了已经采取了哪些非确定性选择，消除了测试工具跟踪不必要状态的需要。由于同样的原因，状态空间也被缩小了。缺点包括难以推断覆盖率，以及任意长的跟踪使将错误的测试用例与IUT中的错误联系起来的过程复杂化。3.2O-精氨酸检测在线测试涉及在IUT上执行测试用例之前生成一批测试用例。测试用例是通过为特定目的进行模型检查并存储来自模型检查器的跟踪而生成的。此跟踪用作要执行的测试用例，以测试目的。在线测试的优点包括能够以非常精确的方式指定和推理覆盖率。缺点包括处理非确定性的问题和模型检查模型的要求，需要探索整个状态空间，这可能导致状态空间爆炸。处理非确定性是一个问题，因为测试用例需要考虑测试目的的所有可能结果。考虑一个测试用例，它要求用户出现在数据库中如果用户不存在，则需要在测试继续之前创建用户。一些测试用例执行工具不支持这种非确定性。QTP是一种工业上使用的测试用例执行工具，它只支持生成的输入和观察的输出的静态测试用例当测试数据库时，需要静态测试用例的问题是主要的，这些数据库固有地依赖于内部状态并在测试期间动态地演变56P. Olsen等人理论计算机科学电子笔记264（2010）534Present和Absent集我们现在介绍最初在[3]中提出的现在和不存在集合抽象抽象将数据库抽象为两个集合：当前集合和缺席集合。当前集合是存在于数据库中的值的欠近似，并且不存在集合是不在数据库中这可以被看作是一个三值逻辑，其中如果值在当前集合中，则对应于真，如果值在不存在集合中，则对应于假，如果值不在两者中，则对应于未知。 如果值为在这两个集合中，它对应于错误状态，这应该被避免。这种抽象允许我们抽象无限数量的数据库，并使用相对较小的值集抽象数据库的实际内容我们定义以下集合[3]：D是一组元素（例如记录、关系、元组等）。可以输入数据库的完整值数据库的具体状态。真实系统所使用的数据库，可以包含大量的数据。CD是一组具有代表性的元素。这些可以通过直觉或一些启发式方法来选择，例如每张桌子上都有几个PnC是当前集合，包含已知存在于数据库中的元素Dn.AnC是缺失集，包含已知从数据库中缺失的元素Dn.d∈D是实际系统中的一个元素。c∈C是抽象系统中的一个元素。图1显示了这些集合。Pn可以增长以填充整个空间CDn，An可以增长以填充整个空间C\Dn。从这些集合中可以得出一些有趣的观察结果：PnDn当前集合中的每个元素都必须在数据库中一个nDn=在缺失集合中没有元素可以在数据库中Pn=An=n表示不知道数据库Dn的内容。Pn<$An=C意味着数据库Dn的所有信息都是已知的，C.Pn<$An=<$必须始终成立。同一个元素不能同时出现在同一个数据库中，也不能同时不在同一个数据库中允许对数据库执行三种操作：插入、删除和查询是否存在。这些操作在下面的数据库和存在-不存在集合上定义因为处理方式不同，所以将它们分为正和负P. Olsen等人理论计算机科学电子笔记264（2010）5357Fig. 1. 在场-缺席抽象集插入插入到数据库中会产生一个新的状态，其中添加了插入的元素：DNJ =Dn{c}这相当于将元素添加到当前集合并将其从缺失集合中删除：PnJ=Pn{c}AJn=An\{c}去除从数据库中删除会导致一个新的状态，而不包含已删除的元素：DNJ =Dn\{c}在present-absent集合中，这导致从present集合中删除并添加到absent集合：PnJ=Pn\{c}AJn=An<${c}肯定质疑这意味着该元素在数据库中c∈Dn如果一个查询是肯定的，我们知道元素在数据库中，这意味着我们可以将元素添加到当前集合中。 我们需要断言元素不存在，这是一个一致性检查。PnJ=Pn{c}assert c∈/An58P. Olsen等人理论计算机科学电子笔记264（2010）53否定质疑这意味着该元素不在数据库中c∈/Dn我们可以类似于肯定查询来更新present-absent集合：AJn=An<${c}assert c∈/Pn定理4.1在Pn和An上的运算相对于实际的Dn是一致的和合理的，在下面的意义上：(i) Pn和An捕获的信息不矛盾。(a) <$c∈Dn<$c∈/An(b) <$c∈/Dn<$c∈/Pn(ii) Pn和An俘获了Dn态的一部分.(a) c∈Pn(b) <$c∈An<$c∈/Dn证据我们用归纳法构造一个证明.我们表明，该属性保持为PnAn=，并显示每个动作的属性后，将其应用于任意集。(i) 我们不知道数据库的数据;PnAn=N。定理1.i.a成立，因为箭头的右侧总是为真，因为An是空的，类似地，1.i.b.定理1.ii.a成立，因为Pn为空，所以箭头的右侧永远不需要求值，类似于1.ii.b。(ii) 我们假设任意集合Pn和An都满足上述要求。对于每一个操作，我们现在展示了在应用该操作后属性保持不变。(a) 插入：在插入c之后，1.i.a成立，因为c从An中移除。 1.i.b持有因为Dn包含c。1.ii.a成立，因为Pn和Dn都包含c。1.ii. b成立，因为An不包含c。(b) 移除：移除c后，1.i.a成立，因为Dn不包含c。1.i.b成立，因为c从Pn中去掉。1.ii.a成立，因为Pn不包含c。1.ii.b成立，因为Dn不包含c。(c) 肯定查询：在对c的肯定查询之后，1.i.a成立，因为我们断言An不包含c。1.i.b成立，因为Dn包含c。 1.ii.a成立，因为我们把c加到Pn上。1.ii. b成立，因为An不包含c。(d) 否定查询：在对c1.i.a的否定查询保持之后，因为Dn不包含c。1.i.b成立，因为我们断言Pn不包含c。1.ii.a成立，因为Pn不包含c。1.ii.b成立，因为Dn不包含c。Q定理4.2F或任意运算在Dn，Pn，andAn上进行，得到DnJ，PnJ，P. Olsen等人理论计算机科学电子笔记264（2010）5359和AJn中的计算信息更精确，即，PnAnPnJAJn.证据证据显而易见。当我们从Pn或An中删除一个元素时（在插入和删除操作期间），我们总是将相同的元素添加到另一个集合中。这意味着集合的并集永远不会缩小。在查询操作期间，我们向其中一个集合添加一个元素，并且Q推论4.3一旦Pn和An捕获了Dn的全部知识，即Pn<$An=C、执行操作将始终保持属性PnAn=C因为知识永远不会缩小，一旦我们达到了最大的知识，我们将停留在最大的知识。5扩展的可编程状态机在介绍新的有限状态机之前，我们介绍了DBFSM和PAFSM所基于的EFSM [9EFSM是一种扩展了内部变量的FSM定义5.1扩展有限状态机是一个7元组（Q，q0，r，V，r，δ），其中：• Q是一个有限的、非空的状态。•q0∈Q是初始状态。• 是输入字母表，一个非空的有限标签集• Γ是输出字母表，一个非空的有限标签集• V是一组有限的变量名。• ψ⊂V×Intassigns integer values to the variables.• δ是一个状态转移关系。δ将源状态q和动作a与目标状态qJ相关联，给定当前变量状态，Thisiswriten：q−→a系统 有五种类型的行动：• 输入，σ∈ε• 输出，γ∈Γ• 零作用，τ• 布尔条件• 变量更新qJ，并且对应于60P. Olsen等人理论计算机科学电子笔记264（2010）53仅当条件的计算结果为true时，才会启用布尔条件操作。布尔条件和变量更新可以使用常规算术和关系运算符。6数据库FSM数据库有限状态机（DBFSM）是一种EFSM，其中变量可以具有我们称为数据库的类型。数据库类型有三个操作：插入、删除和查询成员资格，对应于真实数据库上的相同操作在present-absent抽象的上下文中，DBFSM应该被看作是一个包含真实数据库的系统。定义6.1数据库有限状态机是一个8元组（Q，q0，r，V，r，D，δ），其中：• Q、q0、r、r、V、r和δ的定义与EFSM相同• D是一组数据库。数据库可以保存来自变量的无限数量的值定义了三个函数来操作数据库：Insert（d，v），Remove（d，v），Query（d，v），其中d∈D，v∈V。Insert（d，v）将v的值插入数据库d，Remove（d，v）从数据库d中删除v的值，Query（d，v）返回一个布尔值，如果v的值存在于数据库中，则为true，否则为false这种形式主义为我们提供了一种使用数据库建模系统的方便方法。然而，DBFSM是有限状态系统，因此不适合建模和测试。7在场-缺席FSM我们现在介绍PAFSM，它是DBFSM的抽象。抽象是根据在场-缺席抽象来完成的。定义7.1存在-不存在有限状态机是一个9元组（Q，q0，r， V，V，DP，DA，δ），其中：• Q、q0、r、r、V和δ的定义与DBFSM相同• 将整数值赋给变量。值是整数值的有限集合。• DP是集合的集合，每个集合的大小|瓦卢埃斯|，表示当前集合。DBFSM中的每个数据库一个• DA是集合的集合，每个集合的大小|瓦卢埃斯|，代表缺席集合。DBFSM中的每个数据库一个DP（d）表示数据库d的当前集合，DA（d）表示数据库d的不存在集合。P. Olsen等人理论计算机科学电子笔记264（2010）5361这种抽象允许我们用一个小集合抽象一个无限的数据库集合。此外，PAFSM是有限状态的，这使得可以直接进行状态空间探索。对整数值的要求可以很容易地提升到任何值。此外，这种限制在实践中并不是问题，因为整数值可以在发送到IUT之前在适配器中转换为实际的数据库属性。8翻译我们现在介绍从DBFSM到PAFSM的转换。提出了两种翻译，它们在处理未知值的方式上有所不同。第一次转换假设数据库的全部知识，如果在任何时候观察到未知值，则进入错误状态。第二个假设没有知识，并允许非确定性地选择一个未知值是否应该被视为存在或不存在。DBFSM和PAFSM在每个方面都是相同的，除了使用数据库上的三个操作之一的转换：插入、删除和查询。对于这两个翻译，解释了谁处理这些8.1不知情这种转换假设不知道数据库，即。 PnAn=。它适合于在线测试，其中数据库的知识可以在测试执行期间获得。这种转换也可以用来生成抽象轨迹或树，其中树中的分支对应于模型中的选择。通过这种方式，可以生成在线测试用例8.1.1插入如果该值在当前集合中，则该转换没有效果。如果该值在缺失集合中，则将其添加到当前集合并从缺失集合中删除。如果该值既不存在也不存在，则将该值添加到当前集合。8.1.2去除如果该值在当前集合中，则将其从当前集合中删除并添加到缺失集合中。如果该值在缺失集合中，则该转换没有效果。如果该值既不存在也不存在，则将该值添加到缺失集合。8.1.3查询如果值在当前集合中，则返回true。如果该值在缺失集合中，则返回false。如果值不在两者中，则非确定性地选择true或false并将该值添加到相应的集合中。这种转换符合存在-不存在抽象，因为每个动作根据抽象更新集合。当使用此翻译为62P. Olsen等人理论计算机科学电子笔记264（2010）53在在线测试中，非确定性选择允许模型检查器同时处于两种状态，并且当来自IUT的观察揭示哪个选择是正确的时减小状态空间。当生成树用于O型线测试时，测试人员可以根据观察到的输出遍历树并跟随分支。在实践中如何处理非决定论，将在第10节的具体例子中更详细地说明。8.2完全知情这种转换需要完全了解数据库，即PnAn=C。这个翻译基本上与上面的相同，除了我们删除了三值逻辑的未知方面。这种转换适用于在线测试，在这种情况下，需要生成完整的静态跟踪以简化测试执行。8.2.1插入由于我们对数据库有充分的了解，我们知道该值要么存在，要么不存在，而永远不会同时存在。进行转换将值添加到当前集合，并将其从缺失集合中删除。8.2.2去除接受转换将其添加到缺席集合并将其从当前集合中删除。8.2.3查询如果值在当前集合中，则返回true，否则返回false。由于我们已经排除了未知因素，所以我们不需要查询缺失这种翻译也符合在场-缺席的抽象。由于我们从数据库的最大知识开始，我们知道所有的值都在当前或不存在的集合中。从推论1我们知道我们永远不会失去知识。这使我们能够简化查询操作。这种转换特别适合于需要静态跟踪的在线测试使用这种方法有两个问题：它要求数据库的状态是已知的先验知识，并且它要求在每次执行测试套件之前重新执行测试用例生成（不是针对每个测试用例或测试目的，仅适用于整个测试套件。）数据库的状态只需要在第一次执行测试套件之前检查，因为执行测试套件之后的状态可以被存储并用作下一次执行的输入。重新执行测试用例生成的需求可能是一个主要问题。模型检查和测试用例生成可能需要很长时间才能完成，并且每次测试套件执行都需要这样做可能会显著增加执行测试所需的执行时间为了缓解这个问题，可能会产生一种策略，使数据库进入特定的已知状态。通过这种方式，可以以该状态为起点生成测试用例，并且在测试执行结束时，P. Olsen等人理论计算机科学电子笔记264（2010）5363回到了想要的状态。9优势与使用数据库相比，使用present-absent抽象有几个优点。与对整个数据库建模相比，状态空间最初被大大减少。传统的数据库测试要求数据库在开始测试时处于特定的状态，并且要求测试以特定的顺序执行， 确保数据库始终处于已知状态。利用存在-缺失集和MBT，我们可以将数据库状态的子集输入到存在和缺失集中，然后基于数据库的当前状态来快速生成测试用例。 这样我们就可以从数据库的初始状态中抽象出来，并且仍然可以进行自动测试。传统的测试并不是在实际使用的系统上进行的，因为测试用例可以任意地与实际数据库交互。通过在present-absent集上证明正确性，并证明测试用例只与特定的测试数据交互，测试可以在实际运行的系统上执行。通过观察数据库的状态，可以将系统的状态输入到集合中，并且可以执行测试，仅需将测试数据存储在数据库中在在线测试过程中，可以在不了解数据库的情况下开始测试过程，即 PnAn=。这就是说，数据库的状态可以通过观察系统来动态地学习。随着知识的积累，减小了状态空间，并且可以在期望的方向上引导测试10例如为了说明抽象和测试用例生成，一个例子。这个例子是手工制作的，因为还没有开发工具支持IUT的规范是UPPAAL语法中的时间自动机网络。三个网络的时间自动机：一个建模系统使用数据库，一个翻译假设没有知识和一个假设充分的知识。这个例子是一个简单的系统，用户可以登录并执行一些工作。在系统中，我们有一个单一的数据库，由当前登录的用户组成。用户有三个操作：登录、注销和工作。用户只能在尚未登录时登录。只有登录后才能注销。只有在他登录后才能请求工作。当用户执行操作时，系统将返回OK或Error。图2说明了使用数据库的系统。这被用作IUT的规格。该规范是一个在UPPAAL中实现的时间自动机。 的Q方法查询名为dbLogin的登录数据库，如果cid在数据库中，则返回true。该系统有三个输入通道：工作？，登录？，然后注销？，和两个输出通道：好的！ 错误！. 用户使用输入通道进行查询64P. Olsen等人理论计算机科学电子笔记264（2010）53图二. 使用数据库图三. 用户系统的输出通道用于返回给用户。共享变量currentId用于将调用用户的id传递给系统，确保结果返回给正确的用户。Add和Remove方法分别用于在数据库中添加和删除cid图3示出了系统的用户。这是一个不聪明的用户，按下所有按钮的随机顺序。另一种类型的用户是遵循系统规范的用户。在这个例子中，这样的用户例如只会在他知道他已经登录的情况下尝试请求工作。位置WorkOK和WorkErr是用于指定测试目的的虚拟位置（类似于登录和注销）。为实例来测试用户是否能够请求工作并获得肯定的响应，则会要求UPPAAL提供用户模板进入WorkOK位置的跟踪。在所有示例中使用相同的用户我们现在解释如何使用上面解释的两种方法转换模型我们还解释了如何使用这些模型进行测试。10.1不知情图4示出了假设没有知识的系统。对数据库的每个查询都被转换为对IsLogin方法的调用，该方法有三种可能的结果：TRUE、TRUE和UNKNOWN，对应于抽象中的三值逻辑IsLogin查询当前集和缺席集，并根据P. Olsen等人理论计算机科学电子笔记264（2010）5365价值观如果该值未知，则可以使用非确定性选项，返回OK并将用户添加到当前集合，或者返回Error并从集合中删除用户。Login和Logout方法处理这个问题。这具有在从IUT观察到正确选择时更新数据库的效果。请注意，当登录操作的结果未知时，OK和Error选项都会添加用户。这是因为，返回Error意味着用户在数据库中，因此我们添加他。如果我们返回OK，用户不在数据库中，我们应该删除他，但是，由于登录成功，用户现在添加到数据库中，因此我们添加他。可 以 看 出 ， 我 们 没 有 对 存 在 - 缺 失 集 进 行 任 何 一 致 性 检 查 ， 即 ， checkforPn<$An/=<$. 这是因为我们可以通过使用模型检查器和以下查询来验证这种情况A[] forall（id：UserID）！（存在（id）&&不存在（id））此查询声明：通常情况下，没有用户同时在场和缺席。如果此查询验证，则模型中不会出现不一致。该系统开始时两个集合都是空的。无论何时选择，集合都会相应地更新。如果以该系统作为规范执行在线测试，UPPAAL将采用两种选择并跟踪系统中的两种状态。当从IUT观察到实际动作时，丢弃所有非同步状态。通过在UPPAAL中的模拟器中运行该系统，我们可以模拟在线测试，UPPAAL选择IUT。可以看出，执行一段时间后，我们达到了一种情况，即我们完全了解数据库，即PnAn=C。这个系统已经过测试，对使用UPPAAL TRON的实现。系统实例化有10个用户。一个突变体被制造出来，操作有1/500的机会无法更新数据库。该系统已经实现，使得数据库在初始化时填充随机值。这样，测试人员在开始测试时就无法知道数据库的状态。测试在正确的实现上运行了10次，在突变体上运行了10次每个成功的测试执行了大约22.000个操作（输入和输出组合）。其中一个突变体运行未能检测到突变体，这是由于突变体的随机性。测试表明，存在-缺失集方法具有自动测试与数据库交互的系统的能力，而无需在测试之前了解该数据库的状态我们也可以使用这种转换来生成抽象的轨迹。将为每个测试目的生成一个树。树中的一个分支对应于模型中的一个选择。UPPAALCO VER可用于生成这些树。10.2完全知情图5说明了假定具有全部知识的系统。这个系统类似于没有知识的系统。 因为我们有充分的知识，我们可以删除数据库状态未知的所有转换。这简化了模型。该模型对于生成静态轨迹以用于在线测试是有用的，66P. Olsen等人理论计算机科学电子笔记264（2010）53图四、没有知识的例子图五. 以充分的知识为静态测试工具为了生成跟踪，可以询问UPPAAL模型检查器是否可以到达特定位置，并获取如何到达该位置的跟踪。此跟踪可用作测试用例。我们在用户模板中使用虚拟位置，如图3所示。以下查询用于测试ID为0的用户是否可以成功登录：E>用户（0）.登录OK如果所有用户都不存在，则会生成以下跟踪：用户登录[0]！登录OK [0]！含义：第一个ID为0的用户向IUT发送登录请求，然后IUT向用户0发送loginOK。为了证明我们可以根据不同的数据库的状态，我们在数据库中存在所有用户的情况下再次运行验证器。这将生成以下跟踪：用户，退出[0]！IUT.LogoutOK[0]！用户登录[0]！登录OK [0]！在这里我们可以看到，用户首先必须注销，然后才能成功登录。这表明，通过更新数据库的状态，我们可以生成符合数据库状态这个简单的例子用于说明抽象，但它并不代表实际的数据库系统。使用属性扩展数据库中的用户表可以很容易地通过为每个属性创建存在集和不存在集来实现P. Olsen等人理论计算机科学电子笔记264（2010）5367财产这种方法也可以扩展到包括表之间的关系。一对多关系可以使用一个关系中每个条目的存在和不存在集合来建模，这些集合可以保存对应条目所涉及的值。在今后的工作中需要分析这在实践中是如何形成的11结论我们已经介绍了从数据库到现在和缺席集的抽象和这种抽象的证明。我们介绍了两种新形式的FSM，DBFSM和PAFSM，并解释了如何从DBFSM转换为PAFSM。此外，我们解释了两种不同的翻译，以及它们如何与在场-缺席的抽象相关联。我们已经举例说明了一个使用数据库的简单系统的例子，以及如何将这个系统转换为使用存在集和不存在集的系统。我们已经解释了如何从这个系统中生成测试用例，以及在执行在线和在线测试时使用我们的方法我们能够执行系统的在线测试，而无需考虑任何关于数据库状态的假设。随着测试的进行，我们逐渐获得了有关数据库状态的更多信息。这种知识的增加将减少仿真模型的状态空间，并使我们能够潜在地引导测试在期望的方向。我们可以进行两种形式的O-半胱氨酸测试。一个不需要假设任何关于数据库状态的知识。我们能够生成抽象的跟踪，自动学习数据库的状态，并相应地做出选择，以达到所需的状态。通过在生成测试用例之前检查数据库的状态，我们能够生成可以在没有任何分支的情况下执行的静态跟踪。这就消除了在数据库系统上执行联机测试时的状态依赖性问题。这种方法存在一些潜在的性能问题，但我们希望找到解决这些问题的作为未来的工作，我们计划扩展本文提出的简单的数据库视图我们计划在更大的例子上测量这种方法的有效性，最好是工业上的。我们目前正致力于扩展UPPAAL模型检测器，以提高模型检测系统的有效性，使用现在和缺席集。引用[1] Anders Hessel，Kim Guldstrand Larsen，Marius Mikucionis，Brian Nielsen，Paul Pettersson，and ArneSkou. 使用uppaal测试实时系统正式方法和测试，第77-117页，2008年[2] K.G. Larsen，M. Mikucionis，和B.尼尔森使用UPPAAL进行实时系统的在线测试。 软件测试的正式方法，奥地利林茨，2004年9月21日计算机科学讲义[3] 作者：Peter Olsen，Kim G. Larsen，Marius Mikucionis，and Arne Skou. 现在和不存在的集合：抽象适合测试的数据密集型系统。In R. Huuck，G. Klein，and B. Schlich编辑，系统软件验证博士研讨会（DSSSV亚琛工业大学.68P. Olsen等人理论计算机科学电子笔记264（2010）53[4] 李华冉，柯蒂斯戴瑞森，和安妮莉丝安德鲁斯。 Autodbt：一个自动测试web数据库应用程序的框架。计算机科学讲义，3306/2004：181[5] Li huaRan，CurtisDyreson，AnnelieseAndrews，Re n'eeBryce，andChristopherMallery.构建测试用例和Oracle以自动化测试Web数据库应用程序。信息软件Technol. ，51（2）：460[6] 简·崔特曼。测试并发系统：一种形式化的方法。CONCUR，第46-65页，1999年[7] 简·崔特曼。基于标记转换系统的模型测试。正式方法和测试，第1-38页，2008年[8] Jan Tretmans和Ed Brinksma。Torx：基于模型的自动化测试。在第一届欧洲模型驱动软件工程会议中，第12页，2003年。[9] Gregor von Bochmann和Jan Gecsei。一种规范和验证协议的统一方法。IFIPCongress，第229