理论计算机科学电子笔记190（2007）113-125www.elsevier.com/locate/entcs测试计划域（不带模型标记器）1Franco Raimondi佛朗哥·雷蒙迪2，4英国伦敦大学学院计算机科学系Charles Pecheur CharlesPecheur3，5德·p·t INGI，Universit'ecatholiquedeLouvain，Louvain-la-neuve，Belgium纪尧姆·布拉特6RIACS/NASA艾姆斯研究中心，美国摘要我们解决的问题，验证规划域中使用的基于模型的规划，例如在空间任务。 我们提出了一种方法来测试规划域的单权规则，它是自包含的，在这个意义上，使用规划器来验证正确的规则，并且不需要外部工具。 我们回顾和分析基于需求的测试的覆盖条件，我们的理由详细的“独特的第一个原因”（UFC）覆盖测试套件。我们使用模式对规则进行编码，使用LTL进行编码，并为它们提供UFC覆盖。然后，我们提出了一个翻译的LTL公式到规划目标，并说明我们的方法的案例研究。保留字：基于规范的测试、规划和覆盖标准。1介绍自2004年1月以来，美国宇航局的勇气号和机遇号火星车[14，15]探索火星表面，是复杂系统的一个例子，具有显著的自主性。1 这项工作由NASA ETDP 6E自动化运营项目资助。2作者感谢欧洲IST项目PLASTIC和NASA艾姆斯研究中心关键任务技术的支持。3 作者感谢RIACS / USRA的支持。4电子邮件：f. cs.ucl.ac.uk5电子邮件：charles. uclouvain.be6电子邮件地址：brat@email.arc.nasa.gov1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.011114F. Raimondi等人理论计算机科学电子笔记190（2007）113飞行规则规划领域1：编码为LTL公式规划领域+新目标使用计划器进行2：生成测试用例3：转化为规划目标Fig. 1.从正确的规则到规划目标（概述）。这些功能可以使用当前的软件和硬件技术来构建。由于这些系统的复杂性，为了避免经济损失和任务失败，人们对这种自主应用程序进行正式验证的工具和方法越来越感兴趣。在本文中，我们关注的问题验证规划域。在火星漫游者的情况下，计划是使用欧罗巴2规划器生成的[11]，以满足一些科学和定位目标。 然后，在上传到漫游者之前，这些计划会被手动检查（根据一组称为“自动检查规则”的要求）。生成和验证必须在下一个火星白天周期之前完成我们提出的验证规划域的方法将加快验证阶段，并有助于确保不违反正确的规则在过去已经研究过规划域的验证，例如在[10，12]中。这些作者提出的解决方案包括将规划域翻译成一些模型检查器的输入语言。这些方法的主要局限性是可以翻译的域的大小有限，以及规划器语言和模型检查器语言之间的对应关系有问题在本文中，我们提出了一种不同的方法：我们建议将规划域的验证问题转化为规划问题。这种方法的优点是不需要外部工具，因为实际的计划者可以用来执行验证。具体地说，我们建议按照图1所示进行：给定一个规划域和一组轻量级规则（通常作为文本文档提供）作为输入，在步骤1中，我们将轻量级规则编码为LTL规范。在第二步中，我们从规范中获得测试用例;我们采用了基于需求测试的修订概念，使用类似于[17，16，8]的方法。在第三步中，我们将生成的测试用例转换为计划目标。实际的测试是通过用新的目标集“丰富”原始的规划模型来执行的论文的其余部分组织如下。在第2节中，我们回顾了基于需求的测试的覆盖率概念。我们在第3节中提出了规划问题。第4节介绍了一个激励性的例子。在第5节中，我们展示了如何将时间规则编码为时间公式，以及如何在第6节中使用所提供的示例将这些规则转换为规划目标。我们在第7节结束。F. Raimondi等人理论计算机科学电子笔记190（2007）1131152测试和基于需求的测试存在各种度量来量化测试套件的覆盖率[2]，特别是对于结构测试。功能测试的覆盖度量也可以在正式提供功能需求时定义，例如使用时间公式。以前在这个方向的工作包括[8，16，17]。在本节中，我们简要回顾MC/DC（结构）覆盖率，然后基于Whalen等人的工作，通过将MC/DC覆盖率扩展到LTL公式来推理功能测试的度量。[17 ]第10段。2.1MC/DC覆盖在本文的范围内，我们使用受流行的Modified Condition/Decision Coverage（MC/DC）启发的度量[7]。特别是，MC/DC覆盖范围需要用于最关键的航空电子软件类别[13]，其扩展可以用于基于规范的测试（见下文）。MC/DC覆盖率是根据程序中的布尔决策来定义的，例如if和while语句，以及构成这些语句的基本条件（即布尔项）他们如果一个测试集的执行确保（1）任何决策中的每个基本条件都至少对所有可能的结果采取一次，并且（2）每个基本条件都被证明独立地影响决策的结果，则该测试集被称为达到MC/DC。作为示例，程序片段如果（a|| b）{. }包含具有条件a和b的判定c∈（a∈b）。如果这一决定是在以下三个估值的情况下执行的，则可以实现MC/DC：7(1)a=T，b= T，c=T;（2）a= T，b=T，c=T;（3）a= T，b= T，c=T;事实上，评价1和3只在a中不同，表明a分别以积极和消极的方式独立地影响c同样的论证也适用于b的求值2和3。每个条件的MC/DC要求可以通过一对布尔公式（称为陷阱公式）来捕获，捕获条件显示为积极和消极影响其发生的决策的覆盖范围是通过构建-在满足每个陷阱公式的状态中执行条件的测试用例。在上面的例子中，条件a在c中的陷阱公式是a<$b和<$a<$b。2.2UFC覆盖率如上所述，如果功能规范在一个正式的框架中表达，那么功能测试可以用类似于结构测试的覆盖标准来衡量，但应用于规范而不是实现。这是基于需求的测试背后的思想，如[17]和[16]中所研究的。特别是，[17]定义了独特的第一原因覆盖（UFC）的概念，它将MC/DC的思想扩展到基于需求的测试。7 我们使用T和T来表示布尔真和假。116F. Raimondi等人理论计算机科学电子笔记190（2007）113UFC覆盖率是根据系统执行必须满足的功能属性以及这些属性中出现的原子条件如第5节所示，这些属性通常通过时间公式来表示，例如使用逻辑LTL（我们参考[3]了解更多细节）。如果满足以下条件，则测试集实现了对一组表示为时态公式的需求的UFC覆盖：（1）任何公式中的每个基本条件至少一次采用所有可能的结果。（2）每一个基本条件都被证明是唯一的第一个在[17]之后，条件a是沿着路径π的唯一第一个原因（UFC），如果在沿着π的第一个状态中，满足了条件a，那么它是因为a而满足的。这可以形式化如下。设π是一条路径，X是一组原子条件;我们用π（X）表示X中原子条件沿π的真值序列（也称为π在X上的投影）。定义2.1[a-variant]设AC（A）是线性时间公式中原子条件的出现集合。[8]给定a∈AC（λ）和一条路π，π的a-变体w.r.t.π j是路径πJ，使得π（AC（π）−{a}）=πJ（AC（π）−{a}）。定义2.2 [UFC覆盖]给定一个线性时间公式，条件a∈AC（λ）是λ沿着路径π的唯一第一原因（UFC），或者等价地，π是λ中a的充分（UFC正）测试用例，如果π|有一个a-变量π的πJ使得πJ|= 0。当a是LTL公式时，可以建立陷阱公式ufc（a，a），它是表征a的适当测试用例的时间公式，即a是UFC的路径。9UFC（a，n）是由n上的归纳法定义的。例如，给定a∈AC（λa）：ufc（a，a）=a;ufc（a，<$a）=<$aufc（a，<$a <$b）=ufc（a，<$a）<$$>bufc（a，F<$a）=（<$a）Uufc（a，<$a）ufc（a，G<$a）=<$aU（ufc（a，<$a）<$G<$a）一个完整的定义可以在[17]中找到，并在本节稍后作为一个细化版本。LTL测试用例的这种特征仅适用于完整的无限路径。然而，现实的测试实践本质上局限于有限的、截断的路径。在这种情况下，测试用例覆盖标准需要进一步细化。想想看，例如，公式G=G（a<$b）表示a或b必须在任何时候成立的要求。根据上面的定义，一个适当的测试用例必须满足ufc（a，b）=（a<$b）U（（a<$b）<$G（a<$b））[8]请注意，相同条件a的不同出现被认为是不同的。这造成了多次出现的技术困难。这也是MC/DC环境中的已知问题。9[17]使用了一个不同的符号+的一组（正）陷阱公式的条件，在，即+={ufc（a，）|aoccurr s ina. 符号ion−=（<$）+i s o定义。 我们不使用他在长时间/长时间存储数据时所保留的存储数据|=+和d|=−（se ebelow）。F. Raimondi等人理论计算机科学电子笔记190（2007）113117FFa，bba，ba图二. a在F（a<$b）中的强测试用例和a在G（a<$b）中的弱测试用例。一个概念，finite tt可以是一个可能发生错误的地方，它表明a可能有助于使错误成为现实。然而，并不保证此πf被认为是满足要求的π的预处理，因为它可以根据πf的定义来确定。在G（a/b）中定义了一个简单的概念。在[5]中发现了对截断路径上的时态逻辑的全面处理，其中定义了（πf|=+andπf|=−π，respectively），其中reπf|=−i<$πf|=+<$。我不相信，πf|=+iπf“将所有必要条件都提供给“”，其中π f|=−iit“car r i e s no evid en nce agai n st“。在实际中，如果πf|=+，thenforany（non-truncated）πextendingπfehaveπ|=0。对于更 进 一 步 ， [17] 定 义 了 针 对 s[]+andd[]−su th atπf 的 约 束 和 加 权 约 束 。|=±iπf|=[]±。[10]本质上，[G]+将弱单位元转换为强单位元，而[G] −则相反;特别地，[GG]+= G，[F] −= T。在此基础上，[17]通过要求a（finite）testπf可以将a定义为a的子集，从而将标准的定义提升到a的结果被显示的点，并根据此后的弱语义例如，陷阱公式为：ufc（a，n）=（a<$Fb）U（（<$a<$$> Fb）<$[G（a<$Fb）]−）=（a<$Fb）U（<$a<$Fb）因为[G（a<$Fb）]−约化为T。这也说明了在方法上缺乏统一性：削弱取消了Fb上的一些义务，但不是全部，尽管截断可能同样阻止所有这些义务的实现。相反，在这个在本文中，我们保留了弱和强解释，并统一应用它们，得到了UFC覆盖的两个细化变体定义2.3[强/弱UFC覆盖]给定一个线性时间公式，条件a∈AC（λ）是强（分别为弱）唯一的第一个原因，沿着一个有限的时间pathπf，或方程uivalenty，πf是一个有限的时间patrong（resp. weak）testcaseforainnn，ifπf|=+（resp. |=−）andndthereisana-variantπJofπfsu c hatπJ|=+（分别） |= −）。作为一个例子，图2中的前缀同时是F（ab）中a的强测试用例和G（ab）中a请注意，与上面的讨论一致，没有有限前缀可以强有力地检验像Ga这样的公式，其否定包含可能性。然后，我们将ufc（a，n）细化为强和弱变量-antsufc+andufc−，suchthatπf|=uf c±（a，n）iπf是一 个 连 续 的 函 数 ， 它 可 以 用 来 表 示 a在n中的值。它们的共同定义如下，给定a∈AC（λa）和b∈AC（λb）：11ufc±（a，a）=a;ufc±（a，<$a）=<$a[10]在[17]中表示强[]和弱[]，使用LTL语义扩展到[5]中的有限轨迹。[11]这个定义涵盖了所有的情况，通过将否定推到原子和布尔运算子的对称性。F和G的情况可以从U和W导出。118F. Raimondi等人理论计算机科学电子笔记190（2007）113ufc±（a，ab）=ufc±（a，a）[b]±ufc±（a，ab）=ufc±（a，a）[<$b]±ufc±（a，Xa）=Xufc±（a，Xa）ufc±（a，Fa）=[<$a]±Uufc±（a，Fa）ufc±（a，Ga）= [a]±U（ufc±（a，Ga）<$[Ga]±）ufc±（a，aUb）=[ab]±[aUb]±）ufc±（b，aUb）= [a<$b]±Uufc±（b，b）ufc±（a，aWb）=[ab]±[aWb]±）ufc±（b，aWb）= [a<$b]±Uufc±（b，b）具体地说，G和W中的子项在+-情况下被加强为n和U;特别地，ufc+（a，Gn）对于任何n（不是重言式）都归结为n，反映了Gn不存在足够的强（有限）测试情况的事实。给定一个原子条件a出现在一个公式f中，且给定一个执行模型M，如果存在一个强t e tcaseπf，|=uf c+（a，n）在M的空间中，nπf表明它可以是一个完全有效的整数，因为该序列具有πf的任意一个有效整数。在另一边，如果πf|=ufc−（a，b），则nπfonyshh 这是唯一的问题，即对于具有πf的情况，M中的r不为πf|=uf c±（a，a）：如果a是p（d）p（e）M [16];如果r是一个负的（禁止的）属性，那么它确认了r的这种特殊情况不会发生，这是期望的result。在M中的h πf处找到一个测试函数是很容易的，因为它满足一个πf|=uf c±（a，n），其中n是负性质。3规划[...] 规划可以被认为是产生如何操作某个系统以完成某事的描述的过程由此产生的描述被称为计划，而期望的成就被称为目标。 为了生成一个给定系统的计划，必须给出系统如何工作的模型。”[传统上，在系统的描述中，状态和动作是有区别的（参见，例如，CNOPS规划器及其相关语言[6]）。然而，在本文中，我们采用不同的方法，我们考虑欧罗巴2计划器[11];欧罗巴2产生有限的地平线，确定性计划。Europa 2的关键概念是代币，即，时间范围内的（真实的）事实。例如，在时间t= 2和t= 5之间准备好的打印机使用标记ready表示（参见图3中的第一个标记）。令牌可以表示系统中单个对象的状态，并且有时是互斥的。时间轴是一个标记序列连续出现的结构。例如，打印机的状态可以用一系列标记来描述，如图3所示（因此，状态是一个时间轴）。 在该示例中，语法{2}表示时刻t= 2，而F. Raimondi等人理论计算机科学电子笔记190（2007）113119{1}、{2}[3 - 5] [3 - 5]{21}{21}[30[30 - 34]. . .图三. 时间轴中的标记序列类SimplePrinter扩展时间轴{predicate ready{} /* 没有参数和没有body的谓词：这些是token */谓词忙{}}/* 强制重复循环的简单规则 */ SimplePrintert：：ready{eq（duration，10）;meets（object.busy）;met_by（object.busy）;}见图4。 一个非常简单的NDDL文件。[3- 5]表示3和5之间的tEuropa 2允许基于Allen的区间逻辑来表达令牌之间的各种关系艾伦一对标记之间的关系：meets/met by、before/after、equals、starts/ends、contains/contained by、containsstart/startsduring、contains end/ends during。在Europa 2中，规划问题被公式化为一组令牌（可能属于时间轴），一组使用上面提出的关系，以及一系列目标：这些元素定义了一个所谓的部分计划，欧罗巴2号将其细化为一个完整的计划，即，所有令牌都处于活动状态且不存在未绑定变量我们参考[11]和其中的参考文献，以获得有关欧罗巴2的理论基础的更多细节。Europa 2的输入文件使用新领域描述语言（NDDL，发音为“面条”）表示。NDDL是一种（受限的）面向对象的、类似Java的语言;图4中给出了一个NDDL文件（没有目标）的简单示例。4一个具体的例子：漫游者方案本节介绍了一个具体的案例研究，将在本文的其余部分使用，以验证我们的方法：自主漫游车。漫游车包含三个主要组成部分：一个导航仪，用于管理漫游车的位置和移动;一个仪器，用于执行科学分析;一个指挥官，接收科学家的指令并指导漫游车的操作。这些组件中的每 被映射到 一 类 （分别为：导航器、仪器和命令）;这些类中的每一个都是一个时间轴。 此外，该域包含两个类Location和Path表示物理位置和位置之间的路径。每个时间线都包含以下令牌：• 导航器：在，正在行进（漫游器要么在一个位置，要么在两个位置之间行进• 仪表：装载、卸载、装载、放置、取样（ 仪器可以存放，可以处于存放或卸载状态，可以放置在墨粉不足准备准备忙120F. Raimondi等人理论计算机科学电子笔记190（2007）113班级位置{string name; int x; int y; Location（string _name，int _x，int _y）{name =_name;x=_x; y=_y;}}[...]//导航器是一个时间轴class Navigator扩展时间轴{谓词At{位置地点;}谓词Going{位置从;位置到; neq（从，到）;//这是一个规则：它阻止rover从一个位置//直接返回该位置。}}//这是标记At Navigator：：At{met_by（object.Going from）;//Allen//a Going tokeneq（from.to，location）;// nextGoing token starts at this location meets（object.Going to）;//艾伦//a Going tokeneq（to.from，location）;//在此位置结束的连续的Going{\fnSimHei\bord1\shad1\pos（200，288）}//可能的目标goal（Commands.TakeSample sample）; sample.start.specify（50）;sample.rock.specify（rock4）;图五、摘自NDDL文件中的漫游者示例。见图6。 生成的计划。一个目标，或者它可以取一个样本）。• 命令：takesample，phonehome，phonelander（漫游者可以被指示采集样本，它可以与着陆器或直接与地球通信图5中给出了这个示例的NDDL代码的摘录，其中显示了与Navigator时间轴声明的一部分相对应的NDDL代码（注意与Java语法的相似性有关更多详细信息，请参见图5中的注释 类时间轴（未在示例中显示）是一个包含两个变量start和end的超类（注意，在NDDL中，所有变量和方法都是公共的）。这个场景的一个可能的目标在图5中代码的末尾：目标是在时间50开始rock4的一个示例。当编码场景和目标的NDDL文件被传递到Europa2时，计划器生成一个计划，类似于图6中所示的计划F. Raimondi等人理论计算机科学电子笔记190（2007）1131215飞行规则飞行规则是在每次执行时必须满足的要求。通常情况下，轻量级规则是一个纯文本文档，它伴随着对场景的描述例如，在第4节中给出的示例的一个简单规则是大多数的权利规则都属于[4]中定义的时间模式，因此可以通过LTL公式进行编码。 例如，上面的二阶矩规则可以被编码为G=G（p→q）= G（<$p<$q），其中p=移动，q=收起。5.1适用于轻量级规则的覆盖范围集由于轻量级规则可以被编码为LTL公式，所以第2节中提出的方法可以被应用于生成具有覆盖保证的轻量级规则的测试用例集。作为一个例子，我们考虑上面提出的八权规则，即G=G（<$p<$q）（其中p=移动，q=收起）。作为一个安全性公式，我们只能获得阳性测试用例的弱证据（见第2.2节），因为计划器只能生成有限的执行。具体来说，我们有以下三个测试用例：(i)ufc−（p，n）=（（q））;(ii)ufc−（q，n）=（（<$p<$q）U（p<$q））;(iii)ufc±（p，<$q）=ufc±（q，<$q）=（（<$p<$q）U（p<$q））。第一个正测试用例测试由命题p引起的整个公式的真值（即，第二个测试用例测试命题Q。对于公式的假值只有一个测试用例，并且它是由两个命题贡献的;注意这个测试用例对于弱证据和强证据是相同的对于任何给定场景，可以对规范中出现的所有正确规则重复类似的练习使用上述方法来计算具有UFC覆盖保证的测试用例，相对于当前的测试方法本身是一种改进但是我们的方法可以进一步改进，以使计划开发人员受益：在下一节中，我们将介绍如何通过将时间公式转换为计划目标来自动执行测试。6从时间公式到规划目标本节的核心思想是将LTL公式编码的测试用例转化为规划目标。这是通过构建公式的解析树并将时间轴与解析树的每个节点相关联来实现的。我们使用第4节中给出的场景的第一个正测试案例来介绍这种方法的细节，即对于公式（q），其中p=移动，q=收起我们从命题p开始，只要漫游者在移动，这个命题就成立我们122F. Raimondi等人理论计算机科学电子笔记190（2007）113//带有两个token的新时间轴：class prop-p extends时间轴{谓词TRUE{ };谓词FLASE{};}//返回TRUE：prop-p：：TRUE {导航器导航; equals（导航.Going）;met_by（object. Going f1）;meets（object. Goingf2）;}//Navigator：：Going Navigator：：Going {prop-p p;equals（p.TRUE）;}class prop-not-p{ predicateTRUE { };predicateFLASE {};}prop-not-p：：TRUE{ meets（object.bif1）;met_by（object.bif2）; prop-p p; equals（p. bif2）;}见图7。 命题p和<$p（移动）的NDDL代码。定义一个新的时间轴prop-p，其中包含两个标记TRUE和TRUE：prop-p的标记TRUE是标记Going of Navigator保持不变的情况，而标记TRUE是标记Going of Navigator保持不变的情况。当TRUE不成立时，时间轴的prop-p成立。这些需求被转换为图7（上半部分）中表示的NDDL代码。命题p的否定被定义为一个新的时间轴prop-not-p，它由两个标记TRUE和TRUE以及图7（下半部分）所示的规则命题q（表示仪器被装载的事实）及其否定-它们的定义与新的时间线相似两个命题的合取被编码为新的时间轴，其中四个标记表示两个合取的可能真值。每 个 token 的作用域是使用两个Allen关系contains和contained_by定义的。 整个骗局的真实价值-使用仅具有两个标记（TRUE和TRUE）的第三时间轴来获得接合点对应于两个命题的合取的NDDL代码可根据要求从作者处获得。我们现在可以测试这个公式了n=（q）。为简单起见，设A=AUB，其中A和B被编码分别使用时间线prop-A和prop-BLTL命题成立在该模型中，可以满足以下目标：goal（prop-A.TRUE）; goal（prop-B.TRUE）;eq（prop-A.start，0）; contains_end（prop-B.TRUE，pro p-A. TRUE）;直观地说，上面的目标指出，命题A必须在运行开始时为真（eq（prop-A.start，0）），B在A的TRUE结束之前为真（contains_end（prop-B.TRUE，prop-A.TRUE））。上面提供的附加NDDL代码将添加到场景的原始NDDL代码中（注意在这样做时，插装过程不会在原始模型中引入错误新的“丰富的”NDDL代码被传递到Europa 2以生成计划。如果一个计划可以得到与额外的约束，为积极的F. Raimondi等人理论计算机科学电子笔记190（2007）113123见图8。 生成了带有附加时间表的计划。测试用例，测试成功通过。图8描述了第一个测试用例的Europa 2输出。注意布尔命题的额外时间线（与图6比较）。这个计划说明了一个执行，其中原子条件q（stowed）是唯一的第一个原因。 可以对通过的第二个阳性测试用例和阴性测试用例重复该练习。正如预期的那样，不能为阴性测试用例生成任何计划。6.1讨论虽然上面介绍的场景不像真实的生产和任务环境那样丰富，但它仍然比可以使用模型检查器进行分析的最大示例更复杂[12，10]。我们已经在标准机器上运行了我们的测试，新时间表的引入并没有影响规划器在阳性测试用例中的性能。 这一结果是预期的，因为具有额外约束的域应该比约束较少的域“更容易”解决：新时间线的引入似乎平衡了这一好处。然而，负测试用例需要更多的计算能力，因为回溯涉及过约束域。对于漫游车示例，规划器最终尽管我们在本文中的目的主要是提供可行的覆盖率保证测试套件的规划域，我们不关心的性能问题，但我们认为我们的初步结果令人鼓舞。124F. Raimondi等人理论计算机科学电子笔记190（2007）1137结论传统上，验证规划域的问题已经通过将规划域转换为模型检查器的适当形式来解决，其中验证可以以直接的方式执行，或者通过生成测试用例来执行，除了[9]，其中建议使用规划技术来生成测试。后者的工作与我们的不同之处在于考虑了不同的覆盖条件，并且测试不是从轻量级规则（即，临时规范）。有些问题仍有待调查。例如，我们没有一种方法来处理嵌套时态运算符到规划目标的转换（但我们没有在分析的规则中找到嵌套时态运算符）。我们目前正在解决这个问题，并开发一个软件工具来自动化该方法：我们正在实现一个解析器，从时间模式编码的非线性规则到LTL陷阱公式，使用第2.2节中的定义，最后到NDDL代码。引用[1] J. F. 艾伦 保持对时间间隔的了解Commun. ACM，26（11）：832 - 8 4 3 ， 1 9 8 3 .[2] B.贝泽软件测试技术（第二版）. Van Nostrand Reinhold Co.美国纽约州纽约市，1990年。[3] E. M. Clarke，O. Grumberg和D. A.佩尔德。模型检查。麻省理工学院出版社，马萨诸塞州剑桥，1999年。[4] M. B. Dwyer， G. S. Avrunin和 J.C.科 比特 用 于 有限 状 态验 证 的 属性 指 定模 式 。Mark Ardis， 编 辑，Proceedings of the 2nd Workshop on Formal Methods in Software Practice（FMSPPress.[5] Cindy Reynner等 ， 《 截 断 路 径 上 的 时 态 逻 辑 推 理 》 （ Reasoning with Temporal Logic on TruncatedPaths）。在CAV '03会议记录Springer，2003年。[6] R. Fikes和N. J·尼尔森Strips：A New Approach to the Application of Theorem Providing to ProblemSolving. Arti Ficial Intelligence，2（3/4）：189[7] K. J. Hayhurst，D. S. Veerhusen，J.J Chilenski和L. K.里尔森修改条件/决策覆盖的实用教程。技术报告TM-2001-210876，NASA兰利研究中心，2001年。[8] Hyoung Seok Hong，Insup Lee，Oleg Sokolsky和Hasan Ural。基于时序逻辑的测试覆盖和生成理论。在TACAS史普林格出版社[9] A.E. 豪，A.von Mayrhauser和R.T.Mraz. 测试用例生成是一个AI规划问题。Journal of Automated Software Engineering，第77-106页，1997年4月。[10] L. Khatib，N.Muscettola和K.哈夫隆使用UPPAAL验证计划模型计算机科学讲义，1871，2001。[11]C.麦甘 如何解决它（Europa 2用户指南）。 NASA艾姆斯内部报告，2006年。[12] J. Penix，C. Pecheur和K. 哈夫隆使用模型检查来检查AI Planner域。 在第23届软件工程年会论文集。NASA Goddard，1998年。[13] RTCA。 机载系统和设备认证中的软件考虑，1992年。[14] S. W.机遇号火星车在子午线平原的雅典娜科学考察。Science，第1698-1703页[15] S. W.斯奎尔斯等，精神号火星车在古谢夫陨石坑的雅典娜科学调查。Science，第1698-1703页F. Raimondi等人理论计算机科学电子笔记190（2007）113125[16] L. Tan，O.索科尔斯基和我。李你基于线性时序逻辑的规范测试。 IEEE International Conference onInformation Reuse and Integration（IRI04）信息再利用与集成国际会议论文集。IEEE Society，2004.[17] M. W. Whalen，A. Rajan，M. P. E. Heimdahl和S. P·米勒。 基于需求的测试的覆盖度量.在ISSTAPress.
我的内容管理
展开
