基于代数规范的测试：Veritas案例研究

理论计算机科学电子笔记130（2005）235-261www.elsevier.com/locate/entcs结构化代数规范的测试：Veritas案例研究*帕特里西亚湾L. Machado1，2，3，Elthon A.S.Oliveira1，4，PauloE.S. Barbosa 1，5，Cas ssioL.Rodrigues1，6巴西大坎皮纳联邦大学摘要讨论了使用基于代数规范的测试来验证SML中实现的应用程序，特别是VERITAS模型检查器。测试用例，oracle和数据是从CASL中的结构化规范中生成的，测试oracle负责根据该领域的基础研究驱动和解释测试结果。这项工作的目标是双重的-关键词：Specification-based testing，structured specification，algebraic specification，oracleproblem，test harness。*论文《基于代数规范的测试：Veritas案例》的扩展版本在2004年SBMF会议上提出了“研究报告1由CNPq -巴西研究理事会支助，进程552190/2002-0和477808/2003-42由CNPq/FAPESQ-F和APOIOAPESQISaoESTaoDAPAPao RB A提供支持，项目060/033电子邮件：patricia@dsc.ufcg.edu.br4电子邮件：elthon@dsc.ufcg.edu.br5电子邮件：paulo@dsc.ufcg.edu.br6电子邮件：caleo@dsc.ufcg.edu.br1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.013236PD L Machado等人/理论计算机科学电子笔记130（2005）2351介绍基于规格说明的测试（Specification-based Testing，SBT）关注的是从程序的正式规格说明中导出测试套件。最近，在这一领域的一些工作已经开发[3，13，2]，促进正式方法和测试的结合使用，以成本效益的方式产生高完整性系统[7，4]。在代数领域，SBT包括检查特定公理是否被测试下的实现（IUT）所满足。从一个选定的测试用例（通常是一个公理），运行测试以执行引用操作，并根据测试产生的结果评估输出标准。换句话说，对于有限的测试数据集，预言机通过IUT检查特定公理的满足情况。为了将测试确立为一种有效的验证技术，有必要开发支持测试活动自动化的有根据的方法和策略[19]。在正式的框架中，仍然需要一个伟大的引擎来将测试作为一个标准活动。关于正确性的测试结果的准确解释以及如何正确选择有限的测试集以及自动化和技术转移是至关重要的。在工业环境中应用正式SBT的探索性尝试已经可以找到[2]。我们提出了一个SBT的案例研究，以验证VERITAS工具[27，28]一个面向对象的Petri网建模语言的模型检查器，称为RPOO [16]。VERITAS使用CTL时序逻辑[11]进行属性指定。该工具利用面向对象的观点RPOO模型，使我们不需要处理Petri网语法指定原子命题。VERITAS是用SML语言实现的。我们的主要贡献是使用代数SBT，专注于提出的理论解决方案和文献中提出的结果，在一个真实的案例研究，发现优势和局限性。此外，我们的目标是为缩小SBT理论与实践之间的差距做出贡献。这种研究对于技术转让至关重要。此外，同样重要的是，我们检查了VERITAS模型检查器的实现与CASL中的结构化代数规范的一致性[6]。VERITAS案例研究特别适合SBT，因为代码和操作的数据都足够复杂，无法进行完全的形式验证。本文件的结构如下。第2节介绍了代数规范、测试满意度和应遵循的SBT方法的基本术语。第3节介绍了案例研究，并给出了它在CASL中的正式规范。第4节介绍了进行案例研究所采用的方法。第5节讨论取得的成果和吸取的教训最后，PD L Machado等人/理论计算机科学电子笔记130（2005）235237第6节提出了结论性意见以及进一步工作的指针。2背景本节介绍了代数规范、测试满意度和本文遵循的SBT方法2.1代数规范作为通常的假设，实现被建模为代数。此外，规范声明了一组符号-签名-并包含给出这些符号所需属性的公理。设S =（S，F，Obs）是一个符号7，其中sort（S）=S，opns（S）=F，Obs=S排序8. 设T（X）是代数项（值是从和X构建的项），其中X是一个S-索引的可数无限变量集对于任何两个相同种类的项t和tJ，t=tJ是一个方程;一阶公式由方程、逻辑连接词（<$，惠）和量化器（，）构成。规范中的公理是没有自由变量的公式，称为句子。一个S-代数A由一个S-序集组成|一|，载波集，并且对于每个f：s1×... ×sn→sin n，函数f A：|一|s1×... × |一|sn→|一|S.我们限制到代数与非空载体。对任意的λ-代数A和v a：X→|一|这是一个唯一的同态mα#：T∈（X）→A，它推广了α（平移函数）. t ∈的值|T（X）|sin A underαisthenα#（t）∈|一|S.Ift∈T，即，t是一个基t，t在A中的值为#（t），其中#：T→A是唯一同态.设σ：ΣJ→ Σ j是一个符号态射。这就扩展到将Bj-项转换为Bj-项，将Bj-公式转换为Bj-公式。 n-代数的约化A由σ写成A|σ。若σ：<$J<$→ <$j是包含，则A|也可以使用pj。2.2行为和近似平等平等问题--甲骨文问题的一个例子--是一个问题， 关于如何定义不可观察排序上的相等性，其中不可观察排序是指不被任何特定的具体表示或标准数据类型识别的排序因此，假定这类值的相等是通常的集合论相等是不恰当的。一个代数A的值的相等可以用一个适当的行为相等来解释.这是一7一些特定语言，包括CASL，允许签名包含谓词。W.l.o.g.我们将把这些看作是产生布尔结果的运算。[8]在编程语言中，238PD L Machado等人/理论计算机科学电子笔记130（2005）235部分等价关系-对称和传递关系-的部分同余<$A=（<$A，s）s∈S（每种s∈S有一个关系），它们与）<$∈SignandChMod<$， （ SP ） 是 SP 的 “ 可 检 验 ” 模 型 类 。[1][2][3][4][5][6][7][8][9][10][11][12][13][14][15][16][17][18][19][19][19][10][19][10][10][19][10][10][19][10][10][10][11][10][10][11][10][11][10][11][11][10][11][11][11][10][11][11][11][10][12][11][11][10][11][11][12][11][10][11][11][12][11][11][12） 请注意，测试集是在规范级别定义的，并与公理相关联。上面选择的一组操作对应于一小组简化操作，这些操作使在从结构化规范进行测试时发现的单个问题能够被隔离分析。这些操作可以组合起来，以定义在文献[31，18]中发现的更复杂和有趣的操作，如富集（然后在CASL中）和任意并集或指定之和（以及在CASL中）。泛型规范的实例化可以用联合来定义，并以通常的方式进行翻译。例如，见[29]。下面的定理2.4是定理2.2对于结构化规范的推广在某些条件下，不正确的程序可以通过测试来接受不是每个可检验模型都是真实模型，但任何真实模型都是可检验模型。等式族需要是完整的（健全的）的假设似乎很强，但在定义这些族时，只需要考虑SP定理2.4（[21]）如果n是完全的，是合理的，SP的公理只有正的出现和负的出现，则A∈PD L Machado等人/理论计算机科学电子笔记130（2005）235243Mod（SP）蕴涵A∈ChMod，（SP）。在测试计划中考虑规范的结构是很重要的，因为这可以极大地影响测试用例和测试数据的生成以及测试工具的构建。3Veritas模型在本节中，我们将概述VERITAS模型检查器及其属性评估模块的CASL规范。规范用作生成测试用例的基础，以验证VERITAS实现。3.1概述模型检测是一种用于验证有限状态并发系统的自动化技术。它提供了检查设计模型是否满足给定规范的方法[12]。 为了使用VERITAS验证RPOO模型，我们需要提供模型的状态空间和我们想要检查的属性的规范。验证过程和工具架构如图1所示。Fig. 1. 验证过程和工具架构。评估模块是该工具的主要部分。它负责根据提供的状态空间验证规范中描述的属性。一般来说，如果一个普遍量化的公式被评估为假，评估模块会显示一个反例跟踪，证明该属性在系统中不为真。类似地，当一个存在性量化公式为真时，模块会显示一个证明迹，证明该性质在系统中得到满足。实现的算法是基于244PD L Machado等人/理论计算机科学电子笔记130（2005）235在前向迁移关系上，它们同时进行评价过程和迹的构造。VERITAS并不构造系统的状态空间;这个结构必须作为验证过程的参数提供。这是由于涉及促进模型检查器和用于状态空间生成的工具之间的低耦合的体系结构特征。因此，状态空间爆炸问题[30]可以以独立于模型检查问题的方式处理。工具集成是通过一个标准的状态空间表示格式来实现的。出于这个原因，工具中有一个模块这个模块被命名为状态空间模块。以类似的方式，我们检查要验证的属性是否也符合CTL语法。然而，这是由一个特定的模块完成的，称为CTL编译器。为了提高指定任务的自动化程度，工具中有一个模块，它实现了Dwyer [14]提出的有限状态验证的属性指定模式这个模块被命名为对属性规范。最后，评估模块产生的结果可以被视为文本报告或图形表示。在前一种模式中，报告包含属性的真值、证明该值的可能跟踪以及评估过程中花费的CPU时间。在后者中，我们得到了痕迹的可视化，这使我们能够以图形模式逐步分析它们。这是由对象系统模拟器模块完成的。3.2代数规范本节介绍了在CASL中对VERITAS的求值模块的一部分的规范。为了简单起见，演示文稿将重点放在检查结果上，排除了与结果相关联的跟踪，这些跟踪也是由工具。 该规范分为三个部分：KRIPKE，PATH和CTLO操作员。我们希望这个符号大多是不言自明的。 注意，为了第5节的目的，公理是根据测试用例的编号来标记的。KRIPKE规范（图2）定义了VERITAS使用的状态空间结构-一个涉及的主要数据是Kripke结构（Kripke排序），状态（State排序）和状态标识符（Nat排序）。指定导入自然数的基本指定NAT和集合的泛型指定SET，实例化为SET[NAT]。请注意，公理被所有声明的变量隐式地统一量化。任何一个kripke结构PD L Machado等人/理论计算机科学电子笔记130（2005）235245spec KRIPKE=SET[NATfitElem<$→Nat]then排序Kripke，状态;操作stateId：State→Nat;getState：Nat×Kripke→？State;getSuc：Nat × Kripke →？ Set[Nat]; getPred：Nat×Kripke→？Set[Nat];allStates：Kripke→Set[Nat];PredisNext： 纳特×纳特×克里普克;varss1，s2：Nat;k：Kripke;t1，t2：State•isNonEmpty（getSuc（s1，k））ifs1 eps allStates（k）%（0）%•def getState（s1，k）优惠s1 eps allStates（k）%（1，2）%•def getSuc（s1，k）优惠def getState（s1，k）%（3，4）%•def getPred（s1，k）优惠def getState（s1，k）%（5，6）%•（s2 eps getSuc（s1，k）惠isNext（s2，s1，k））ifs1 eps allStates（k）%（7，8）%•（s1 eps getPred（s2，k）惠isNext（s2，s1，k））ifs2 eps allStates（k）%（9，10）%•stateId（getState（s1，k））=s1ifs1 eps allStates（k）%（11）%•（getState（s1，k）=getState（s2，k））如果s1 eps allStates（k）大于s2 eps allStates（k）%（12）%•（stateId（t1）=stateId（t2）t1=t2）如果stateId（t1）eps allStates（k）则stateId（t2）eps allStates（k）%（13）%•getSuc（s1，k）isSubsetOf allStates（k）ifs1 eps allStates（k）%（14）%•getPred（s1，k）isSubsetOf allStates（k）ifs1 eps allStates（k）%（15）%端图二. KRIPKE规格。必须有一个后继（公理（0））。给定一个状态标识符，getState、getSuc和getPred分别返回状态、其后继标识符和前趋标识符。这些操作仅定义为属于kripke结构的所有状态的集合的状态标识符转移关系由isNext谓词（公理（7，8），（9，10））表示。最后，状态标识符是唯一的，没有状态可以有两个不同的标识符（公理（11），（12）和（13））。图3所示的路径规范定义了路径。kripke结构k中的路径是状态s0，s1，s2，.的无限序列。S.T. s0是初始状态，si+1是si在k中的后继，对于所有i≥0。 具体来说， tion导入KRIPKE规范，将LIST规范实例化为[10][11][12][13][14][15][16][17][18][19][1paths操作返回所有以给定状态s为初始状态的有效路径（公理（2，3））。路径是有效的，当且仅当kripke结构的转移规则被路径中的状态排序所遵守（公理（4，5））。 路径可以246PD L Machado等人/理论计算机科学电子笔记130（2005）235从状态列表构造，但constructPath操作仅针对有效路径定义（公理（0）），并且状态列表被保留（公理（1））。指定排序路径=排序路径结束specPATH=KRIPKEanddLIST[NATfitElem<$→Nat]anddSET[SORTPAThfitElem<$→Path]thenn操作constructPath：List [Nat] ×Kripke→？路径;allPathStates：Path×Kripke→List[Nat];路径：Nat×Kripke→Set[Path];predisValid： 路径×克里普克;varsp：Path;k：Kripke;l：List[Nat];•def constructPath（l，k）isValid（constructPath（l，k），k）%（0）%•def constructPath（l，k）默认路径状态（constructPath（l，k），k）=l %（1）%•（s：Nat·（p eps paths（s，k））优惠isValid（p，k）%（2，3）%•isValid（p，k）惠值j：Nat·（j <#（allPathStates（p，k））−！1⇒（allPathStates（p，k）！j eps所有国家（k）allPathStates（p，k）！（j+1）eps所有国家（k）isNext（allPathStates（p，k）！（j+1），allPathStates（p，k）！（j）、（k）%（4、5）%端图三. PATH规格。CTLO操作器规范（图4和图5）定义了语法CTL（Computation Tree Logic）公式的语义。 该规范导入路径规范和线程规范。涉及的主要附加数据是CTL公式（CTLF排序）和原子命题（PROPEVAL排序）。CTL公式可以使用AP操作从原子命题构造。eval操作表示对给定kripke结构和状态的原子命题求值。 TT和FF是平凡的CTL公式。给定两个CTL公式φ和φ，则NOTCTL（φ），ANDCTL（φ，φ），ORCTL（φ，φ），EU（φ，φ），AU（φ， φ），EF（φ），AF（φ），EX（φ），AX（φ）、EG（φ）、AG（φ）也是CTL公式。CTLO运算符公理（图5）定义了给定kripke结构k和初始状态s的公式满足（检查操作）的语义[11]。注意AX、EF、AG、AF和AU的语义是根据EX、EU和EG给出的（公理（20，21），（14，15），（24，25），（16，17），（12，13））。事实上，VERITAS只实现了后者，并使用CTLO操作器规范中使用的相同等效定律规范化了前者注意，EXφ表示当前状态存在一个后继状态，因此φ在这个状态下有效（公理（18，19））;E[φU]表示存在一条从当前状态出发的路径，因此φ必须在 路 径 的 所 有 状 态 下 有 效 ， 直 到 到 达 一 个φ 有 效 的 状 态 （ 公 理 （ 10 ，11））;EG（φ）表示存在一条从当前状态出发的路径，其中φ总是有效（公理（22，23））。的PD L Machado等人/理论计算机科学电子笔记130（2005）235247spec CTLOOPERATORS=P路径和排序CTLF，PROPEVAL;TT行动：CTLF;FF：CTLF;那就试试吧AP：String×PROPEVAL→CTLF;NOTCTL：CTLF→CTLF;ANDCTL：CTLF×CTLF→CTLF;ORCTL：CTLF×CTLF→CTLF;EU：CTLF×CTLF→CTLF;AU：CTLF×CTLF→CTLF;EF：CTLF→CTLF;AF：CTLF→CTLF;EX：CTLF→CTLF;AX：CTLF→CTLF;EG：CTLF→CTLF;AG：CTLF→CTLF;preds检查： Kripke×Nat×CTLF;评估： 克里普克×纳特×普罗佩瓦尔;...端见图4。CTLO操作符规范（排序、操作、谓词签名）。ANDCTL、ORCTL和NOTCTL的定义与通常一样（（4，5），（6，7），（8，9））。4案例研究方法这项工作的目的是产生自动化的功能测试，从一个正式的规范，可以运行，以验证实现的VER-ITAS生成。此外，通过自动化测试套件来减少模型检查理论与其具体实现之间的差距，这些测试套件可以随着正式规范的发展而发展，并在实现发生变化时有效地应用。这对于复杂的系统非常重要，例如不断发展以满足性能要求的VERITAS根据[27]中提出的CTL公式检验算法，用SML语言实现了VERITAS。在本文提出的实验之前，基于静态分析和ad-hoc/手动测试，对算法和实现进行了验证。然而，这种应用程序的实现的复杂性自然使得静态分析很难甚至不可能完全执行。在本文的案例研究中使用的验证过程有四个主要活动：1）测试规划; 2）CASL中的形式化规范; 3）测试线束构造; 4）测试套件生成，执行和分析。这些248PD L Machado等人/理论计算机科学电子笔记130（2005）235变量k： 克里普克： Nat;i： String;p： PROPEVAL;f1，f2：CTLF•notcheck（k，s，FF）%（0）%•check（k，s，TT）%（1）%•check（k，s，AP（i，p））优惠eval（k，s，p）%（2，3）%•check（k，s，NOTCTL（f1））优惠<$check（k，s，f1）%（4，5）%•check（k，s，ANDCTL（f1，f2））优惠（check（k，s，f1）减check（k，s，f2））%（6，7）%•check（k，s，ORCTL（f1，f2））优惠（check（k，s，f1）优惠check（k，s，f2））%（8，9）%•check（k，s，EU（f1，f2））优惠（c：Path·（c eps paths（s，k）j：Nat·（j#（allPathStates（c，k））

下载后可阅读完整内容，剩余1页未读，立即下载