自动生成观测器测试实时应用程序的一致性

理论计算机科学电子笔记113（2005）23-43www.elsevier.com/locate/entcs通过自动生成观测器测试实时应用程序的一致性Saddek Bensalem，Marius Bozga，Moez Krichen，StavrosTripakis韦里马格法国，38610Gi`eres，Vignate大道2号，CentreEquation，摘要我们提出了一种新的方法，自动化测试的实时应用程序，特别是机器人应用程序。起点是一个高级规范，它可以自动转换为时间自动机网络。模拟或数字时钟观测器，然后从时间自动机规范生成。被测系统（SUT）被配置为导出可观察事件和相应的时间戳。SUT产生的轨迹被馈送到观察者（在线或离线）。后者检查每个跟踪是否符合规范。该方法已应用于NASA的K9火星探测器执行。关键词：测试，时间自动机，规划，火星探测器1介绍程序的计算机辅助验证已经被形式方法研究界研究了几十年。人们提出了不同的模型和规范语言来描述系统，并以精确的方式表达它们所需的特性。研究了这些模型在不同领域的表现力和适用性。然而，人们很早就认识到，这种方法依赖于两个基本的易处理性问题首先，不可判定性，因为许多无限状态模型的图灵机表达能力第二，由于状态爆炸，也就是说，要探索的状态空间太大，难以处理。于是，大量的专家集中精力解决这些问题，取得了许多重大进展。强大的定理证明技术，（半）自动抽象，1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.03624S. Bensalem等人/理论计算机科学电子笔记113（2005）23状态空间的符号表示，在-的-的算法，组合和假设-保证方法，等等。尽管这些，棘手性仍然是形式验证的适用性的主要障碍。另一个主要的障碍是，对于许多系统来说，一个正式的模型根本不存在，而且构建起来太困难或成本太高。一个补充或替代的方法，广泛使用的行业，今天是测试. 测试不如验证雄心勃勃，从某种意义上说，它的目的只是找出错误，而不是证明正确性。事实上，大多数测试方法都不完整（即，即使系统通过所有测试，也不能保证它是正确的）。然而，随着成功测试次数的增加，对系统正确性的信心也会增加[27]。测试的这一特性对行业特别有吸引力，因为它允许工程师决定在验证中投入多少精力，而不是此外，测试不需要被测系统（SUT）的模型大多数测试方法都是“黑箱”，在这个意义上，关于SUT的唯一知识是它与外部世界的接口（输入和输出的集合）。规范的模型对于自动化测试生成是必要的，然而，这个模型通常是有限状态的，并且比SUT的模型小得多。这一点以及上面的特性使得测试变得容易处理。在本文中，我们提出了一种新的实时应用程序的动态测试方法.它是动态的，因为它利用了SUT的工具化和运行时验证技术。我们所要研究的系统类包括所有存在一个规范的系统，并且可以转换为（或直接给出为）时间自动机（TA）网络[2]。这种系统的许多实例可以在机器人领域中找到在那里，计划定义了完成任务所需执行的步骤，并提供了有关顺序、时间等的详细信息，这些步骤。该计划作为输入提供给执行平台（该术语包括软件，中间件和硬件），该平台必须通过以指定的时间和顺序执行指定的步骤来实现它。因此，计划可以被视为规范，执行该计划的平台可以被视为SUT。我们的方法如图1所示，并在第2节中详细描述。让我们在这里简单地总结一下。起点是一个计划，它被认为是一个高层次的规范。此计划将自动转换为TA模型。从后者观察者是自动合成的。 观察者也是一个测试设备，也就是说，它检查是否 观察序列（具有时间戳）符合规范。执行平台是仪表化的，因此它可以与观察者接口。这个接口必须基本上导出可观察的事件和时间-S. Bensalem等人/理论计算机科学电子笔记113（2005）2325这些事件的邮票。最后一步是测试本身。它可以通过以下方式完成：（1）在线，通过在仪表化的执行平台上运行计划我们的方法的主要优点是它可能是全自动的。计划可以自动转换为TA的网络[1]。TA的观察者可以自动生成，如我们在这里所示。对于本文中报告的案例研究，我们依赖于NASA的Klaus Havelund和Rich Washington的帮助，用于执行平台的仪器和痕迹的生成。然而，在一般情况下，通过识别平台事件和指定事件之间的映射，并自动扫描代码，将事件/时间戳导出命令添加到已识别的平台事件，也应该可以自动化这一部分。最后，观察/测试过程也是自动的。本文的其余部分组织如下。第2节详细介绍了方法。第三节简要回顾了时间自动机模型。第4节描述了计划及其向TA网络的转化。第5节展示了如何从TA自动生成观察者。第6节讨论了我们的方法在K9漫游者案例研究中的应用。第7节载有结论和未来工作计划相关工作[4]报告工作与我们有很大关系。他们的计划也是基于仪器的SUT和运行时分析的仪器SUT使用一个观察员。他们的方法的起点是一个测试输入生成器，它生成到仪表化SUT的输入。这些输入还被馈送到属性生成器，该属性生成器生成SUT必须在这些特定输入上满足的属性。属性和执行跟踪被馈送到观察者，观察者检查前者是否被后者所满足。测试输入生成器和属性生成器是专门为要测试的应用程序编写的，而仪器包和观察器是用于不同应用程序的通用工具在[4]中报告的两个案例研究之一中，即K9漫游者控制器，输入是我们在本文中使用的计划（见第6节）。测试输入生成器生成所有可能的计划，直到给定的节点数量和时间约束的界限我们的工作与[4]的工作之间的区别如下：• [4]在他们的工具链中包括一个测试输入生成器和一个仪器包。在这些方面，我们的工作还没有完成。K9 Rover26S. Bensalem等人/理论计算机科学电子笔记113（2005）23在案例研究中，我们依赖于NASA人员和工具进行输入计划、仪器和轨迹生成。• 在[4]中，从每个计划自动生成一组不定时的时态逻辑属性（最近，这项工作已经扩展到实时时态逻辑[7]）。如[4]所述，在我们的工作中，计划被转化为时间自动机网络这是一个全自动和高效的过程，它捕获了计划的全部语义[1]。请注意，一旦生成，对应于计划的TA还可以用于生成观察者之外的其他目的例如，检查计划是否满足某些属性，测量各个子阶段的延迟等。• [4，7]中使用的观察者工具（DBRover [13]，JPax [15，8]，Eagle [6，5]）是通用工具。在我们的工作中，我们自动为每个计划生成一个观察者。这有可能优化特定计划的观察者。最后，我们认为，我们的工作是一种值得追求的替代办法2方法我们的方法主要集中在测试机器人应用，如NASA K9 Rover（见第6节）。这种应用程序通常分为两层。一个高级规划层和一个低级执行层。规划层遵循输入计划，该计划是完成手头任务所需步骤的详细描述。规划层向执行层发出命令，执行层尝试实现这些命令并返回结果，包括关于成功或失败的状态信息然后，规划层根据此反馈和计划中的说明来规划后续步骤存在许多用于机器人应用的规划语言，参见例如[20，17，18，24，22，21，14]。这些语言允许指定步骤的顺序，它们的时间，如何处理异常或失败等等。因此，它们可以被视为任务的规范。一个正确的执行平台必须符合这个规范。我们的目标是通过测试来检查这一点。更准确地说，我们的方法如图1所示。它包括以下阶段：S. Bensalem等人/理论计算机科学电子笔记113（2005）2327自动翻译输入，v ，执行z平台r自动仪表第五，v ，、、、观察员（执行仪表化执行zv是的，是/否robservation/测试z平台r诊断Fig. 1. 方法(i) 从计划自动生成时间自动机规范。(ii) 从时间自动机规范自动生成观察者。(iii) 被测系统的检测，即执行平台。(iv) 工具化执行平台的执行和测试。在图中，实线箭头表示模型和程序转换，虚线箭头表示数据流（输出/输入）。我们将在下文中详细阐述上述每个阶段第一步是将计划转换为时间自动机的形式，或时间自动机（TA）网络。翻译必须保持计划的语义，也就是说，TA和计划的语义必须相等。 也可能是TA以形式化的方式定义了计划的语义，如[1]和本文所述获得TA指定A之后，下一步是自动生成A的观测器。观察者是一种测试设备。它观察被测系统（SUT）并检查SUT生成的跟踪是否符合A。所观察到的轨迹是可观察到的事件和相关联的时间戳的序列。时间戳的准确性取决于观察者时钟的准确性。在本文中，我们考虑两种类型的观察者（我们遵循[16]的术语模拟观测器，可以精确地观测实时，数字（或双采样）观测器，用时钟在给定的时间内滴答作响来测量时间。数字时钟观测服务器显然更容易实现，因为在实践中，观测者只能访问有限精度的时钟。然而，模拟时钟观测器仍然是有用的，例如，当实现是离散时间的，但它的时间步长是未知的先验。一个观察到的迹如果可能由A产生，则它与A一致。TA模型计划28S. Bensalem等人/理论计算机科学电子笔记113（2005）23请注意，A通常被建模为TA的网络，这导致了自动机之间的非确定性和内部通信。这些是模型的人工产物，与外部行为和规范本身无关。因此，我们把它们“隐藏”起来，把它们看作是不可观察的事件。这意味着观察者检查所观察到的轨迹是否是由A的某个轨迹产生的可能观察。第三步是执行平台的仪表化。它的目的是将后者与测试设备（观察者）连接起来。这里存在两种可能性。无论是测试是在现场（或在线），也就是说，在执行的平台，这是连接到观察员在实时执行。或者它是在线执行的，也就是说，首先多次执行平台以获得一组日志跟踪，然后将这些跟踪馈送给观察者。在这两种情况下，检测平台必须能够向观察者公开一组可观察事件。在测试离线的情况下，平台还必须记录这些事件的时间戳。对于在线测试，时间戳可以由平台或观察者完成。在后一种情况下，必须考虑可能的接口延迟仪器可以手动或自动完成。根据SUT的复杂性，它可能是一项重要的任务。应小心操作，以免仪器本身改变系统的行为。例如，添加代码的开销应该是最小的，以免影响系统中任务的执行时间。这些都是任何仪表化过程中固有的问题，超出了本文的范围最后一步是测试程序本身。由仪表化平台生成的轨迹被实时地（用于在线测试）或离线地馈送到观察者。观察者检查每个跟踪的一致性。如果发现迹线不符合质量标准，则SUT不合格。否则，无法得出任何结论然而，对SUT正确性的信心随着测试次数的增加而获得一组有代表性的测试，以满足某些覆盖标准是任何测试方法中的一个问题（例如，[27]，这超出了本文的范围3预赛时序、投影和数字化设N为非负整数的集合。设R是非负有理数的集合。考虑一组有限的动作。RT（RT）（分别为， DT（DT））被定义为所有有限 长 度 实 时 序 列 的 集 合 （ 分 别 为 ， 离 散 时 间 序 列 ） ， 即 形 式 为 （ a1 ，t1）···（an，tn）的序列，其中n≥0，对于所有S. Bensalem等人/理论计算机科学电子笔记113（2005）2329δ∈∈0一1≤i≤n，ai∈R，ti∈R（分别为， ti∈N），且对所有1≤ij≤n，ti≤tj.将表示空序列。ti将被称为i的时间戳。请注意，时间戳是相对于序列的开始因此，在本发明中，当连接序列时，它们需要被调整。更精确地说，给定ρ=（a1，t1）···（an，tn）和σ=（b1，tJ1）···（bm，tJn），ρ·σ是序列（a1，t1）···（an，tn）（b1，tn+tJ1）···（bm，tn+tJm）.在一个序列ρ中花费的时间，表示为时间（ρ），是最后一个动作的时间戳（如果序列为空的）。例如，时间（（a，0. 1）（b），1. 2））= 1. 2.给定j和 ρ∈RT （ ）（ 分别为， DT （ρ ） ）， ρ到ρJ的 投影， 记为PρJ（ρ），是RT（ρJ）中的序列（分别为，DT（J）），通过从ρ中“擦除”所有对（ai，ti）使得ai/∈ j而获得例如，如果p ={a，b}，P={a}且ρ=（a，0）（b，1）（a，3），则Pp =（a，0）（a，3）。对于一组序列LRT（）（或LDT（）），Pobs（L）={Pobs（ρ）|ρ∈ L}。考虑δ∈R，δ >0，且ρ∈RT（π）。ρ相对于δ的数字化，记为[ρ] δ，是DT（π）中的一个序列，通过将每对（ai，ti）替换为ρy（ai，[ tiπ]）而获得，其中[x π]是x的整数部分。 如果ρ=（a，0. 1）（b，0. 9）（c，1）（d，2.3），n[ρ]1=（a，0）（b，0）（c，1）（d，2），[ρ]0. 5=（ a ， 0 ） （ b ， 1 ） （ c ， 2 ） （ d ， 4 ） .对 于 序 列 L∈RT （ π ） ，[L]δ={[ρ]δ|ρ∈L}。时间自动机我们使用时间自动机（TA）[2]和最后期限来模拟紧急情况[23，9]。一个在TA上的时间自动机是一个元组A=（Q，q0，X，n，E），其中Q是一个有限的位置集;q0Q是初始位置;X是一个有限的时钟集;E是一个有限的边集。 每个边是元组（q，q，J，r，d，a），其中q，q，j，Q是源位置和目的地位置; r是守卫，x #c形式的约束的合取，其中x ∈ X，c是整数常数，并且#∈ {<，≤，=，≥，>}; r ∈ X是时钟重置; d ∈ {lazy，delayable，eager}是最后期限; a ∈ f是动作。直觉的、急切的转换必须在它们延迟转换不会对时间的流逝施加任何限制;最后，当延迟转换被启用时，只要时间进程没有禁用它，就允许等待。我们将不允许具有x> c形式的守卫的渴望边缘。TAA定义了一个无限标记跃迁系统（LTS）。它的状态是对s=（q，v），其中q∈Q，v：X→R是一个clock赋值。→0是赋值0给A的每个时钟。SA是所有状态的集合，SA=（q0，→0）是初始状态。以下是两种传输类型：• 形式为（q，v）→A（qJ，vJ）的离散转移，其中a∈n，且存在是一条边（q，qJ，r，d，a），使得v满足n，vJ由下式获得：将r中的所有时钟重置为零，并保持其他时钟不变;30S. Bensalem等人/理论计算机科学电子笔记113（2005）23不→∈→A00一∈一一• 形式为（q，v） A（q，v+t）的定时转移，其中tR，t >0且没有边（q，qJ，j，r，d，a），使得：d =可延迟且存在0 ≤ t10，TAA的δ-数字观测迹集定义为：(3)DigTraces（A，Loobs，δ）=[ObsTraces（A，Loobs）]δ。注意，Traces（A）RT（）、ObsTraces（A，obs）RT（obs）和DigTraces（A，Bibbs，δ）DigDT（Bibbs）.4从计划在本节中，我们将介绍如何从计划中获取TA模型。我们给出了由K9罗孚执行者执行的计划的具体语言的构造，这实际上是我们的案例研究（见第6节）。尽管如此，TA模型是一般的，足以捕捉大多数的计划语言表达的约束。对于K9 Rover应用程序，计划是执行者必须执行的操作的层次结构。传统上，计划是行动的确定性序列。然而，增加自主权需要增加灵活性。因此，计划语言允许基于需要检查的条件进行分支，并且还允许相对于动作的开始时间的灵活性。我们在这里举一个例子，说明执行者必须执行的计划所使用的语言。ρ一一一S. Bensalem等人/理论计算机科学电子笔记113（2005）2331计划→节点节点→块|任务块→（块节点属性：node-list（Node. 节点））任务→（任务节点属性：actionSymbol）节点属性→：idSymbol：start-condition条件：waitfor-condition条件（块：idnode0：故障时继续：start-condition（（1 5））：结束条件（（1 30））：node-list（（块：idnode1：故障时继续：start-condition（15））（块：idnode2：故障时继续：启动条件（+1 +5）：结束条件（+1 +30））：条件条件）：end-condition条件）[：continue-on-failure]条件→（时间 [+]StartTime[+]EndTime）图二. 计划的具体语法（左）和计划示例（右）。计划一个计划是一个节点，一个节点或者是一个任务，对应于一个要执行的动作，或者是一个块，对应于一个逻辑节点组。图2显示了我们用来描述计划的语言的语法。除节点id外的所有节点属性都是可选的。每个节点可以指定一组条件。开始条件（在节点执行开始时必须为真）、等待条件（在条件不为真时等待）、维护条件（在节点执行过程中必须为真）和结束条件（在节点执行结束时必须为真）。每个条件包括关于相对或绝对时间窗口的信息，指示时间的下限和上限。故障时继续标记指示遇到节点故障时的行为我们在下文中提出了一种编译方法，允许从一个计划（即语法对象）中获得一个时间自动机网络（即语义模型），该网络对该计划的所有可接受的合理执行进行为了简单起见，我们考虑以下计划的抽象语法定义4.1（计划语法）计划P是元组（N，δ，λ，n0），其中• N是节点的有限集合• δ： N→N是节点分解函数，定义为图像32S. Bensalem等人/理论计算机科学电子笔记113（2005）23集合关系δε={（n，nJ）|nJ∈δ（n）}满足·无环性：n∈N。n/∈δ<$+（{n}）·不相交性：n1，n2∈N，n1/=n2. δ+（{n1}）δ+（{n2}）=• λ：N→λ×I4×B是节点标号函数，其中λ是一组动作标号，I={[l，u]|l，u∈N}是区间常数集，B是布尔值.即λ（n）=（an，（s n，w n，m n，en），f n）其中an n是作用量symbol、sn、wn、mn、en分别是开始、等待、维持和结束定时约束，并且fn是与节点n相关联的故障时继续的时间标记• n0∈ N是计划计划语义节点按顺序执行。对于每个节点，执行通过以下步骤进行：(i) 等待直到满足开始条件;如果当前时间超过了开始条件的结束，则节点超时，这是节点故障。(ii) 任务的执行通过调用相应的动作来进行。该操作所需的时间与：duration属性中指定的时间完全相同。如果：fail为true或不满足时间条件，则操作块的执行简单地通过按顺序执行节点列表中的每个节点来(iii) 如果时间超过结束条件，则节点失败。当序列中出现节点故障如果为true，则继续执行序列中的下一个节点。如果为false，则节点故障将传播到包含该节点的块，依此类推。如果节点故障传递到计划的顶层块，则执行将中止。我们现在提出的语义节点和计划的时间自动化。语义是建设性的意义上说，自动机可以有效地构造，取决于语法描述的节点。语义也是组合的，在这个意义上，语义的计划是直接获得的时间自动机相关联的节点组成。让我们首先对给定的计划P=（N，δ，λ，n0）引入一些符号动作集合RNP包含针对所有节点n定义的同步动作集合beginn、abortn、failn、endn，以及针对计划P的任务节点n定义的基本动作集合ann。时钟集合XP={Xn|n ∈ N}包含每个节点的一个时钟xn计划的N。 当执行节点n时，该时钟xnS. Bensalem等人/理论计算机科学电子笔记113（2005）2333，zr？开始n/xn：=0v？中止;中止、、、z，，<$[[afteren]]r！失败n，v，z中止rˆˆ、zv[[sn]][[wn]]、R，v，z失败，v，！失败ˆˆˆRnzz就绪rr得双曲执行z、R？中止n，v，R[[e]]nz端[[en]]！失败;失败、伏！endnzR，，z中止rˆ、、、z失败ˆ R、、、z就绪R？abortn，，[[mn]]v你要执行命令 ！法伊莲！an得双曲余切值.z端、R，，zˆˆ、、、z失败ˆˆ R？中止;中止，vv，zbefororenir ！法阿伊勒[[afteren]]n！中止ni！开始！失败;失败ni，，（？abortn 、V，、z R我的天啊！abort¬[[aftere]] ∨ ¬n）[[m]] 、nniz R？结束ni ？不及格，v，v图三.公共部分（左）、任务特定部分（右，上）和块特定部分（右，下）的模式的时间自动机。开始.如果cn= [l，u]是节点n的某个约束，我们将用[cn]]来表示定时保护（l≤xn<$xn≤u）。我们还注意到在c之后的约束[−∞，u]，其中c的下界已被移除。对于P的每个节点n，我们将一个时间自动机与时钟XP和动作XP相关联。自动机编码的顺序行为所描述的节点执行算法。注意，由于执行算法是确定性的，因此获得的时间自动机是确定性的。定义4.2（节点语义）图3说明了转换。 设n是一个节点，δ（n）= n1. nk和λ（n）=（an，（sn，wn，mn，en），fn）.节点n的语义由公共部分的时间自动机描述，如图的左侧所示具体部分按节点属性填写如下。 对于一个任务节点（δ（n）= 0），如右上角所示的一部分。对于失败时继续的块节点（fn= true），如图右下角所示。对于一个块节点没有继续失败（fn= false），如图的右下部分所示，除了标记为？failni引导回到最右底部位置。为了简单起见，我们用实线表示急切转换，用虚线表示懒惰转换。！然后呢？表示经由类似CSP的消息传递的通信。34S. Bensalem等人/理论计算机科学电子笔记113（2005）23。？开始0v。？开始1。？开始2. ！失败0[1≤x0≤5]x0：= 0 [x 0≥30]v）的x1：=0v。）的。x2：= 0v[x 2≥30]. ！失败2）的[1≤x 0 ≤5]？中止1v[x0≥30][1≤x 2 ≤5]？中止2. ！失败0）的v。）的[x2≥30]v）的？中止1. ！失败2？中止2v[x0≥30]. ！失败0）的v。）的伏！失败2[x2≥30]。）。！执行1什 么 ？中止1！执行2什 么 ？中止2v. ！失败0[x0≥30]）的！开始1。！成功1？中止1伏！未通过1）的伏！失败2。）的？中止2[1 ≤x≤30]2. ！abort 1！fa）il 0.？成功1？未通过1v [x0≥30]v。！success2v。. ！失败0！开始2vv[x0≥30] ）的.！abort 2！fa）il 0.？成功2？失败2v [x0≥30]/\/\vv[x0≥30]s//\\. ！失败0）。[1≤x0≤30]！成功0 v。node0开始（1，5）结束（1，30）该计划TA节点2TA节点1TA节点0node2开始（+1，+5）结束（+1，+30）node1start（1，5）图四、一个计划及其到三个时间自动机网络的转换最后，整个计划P的语义由并行组合给出，即为所有节点定义的时间自动机网络。注意，乘积自动机也是确定性的。定义4.3（计划语义）设P =（N，δ，λ，n0）是一个计划，XP是时钟的集合，λ P是由P定义的动作的集合。设Ani是X P上的时间自动机，λ P与节点ni∈N相关。计划P的语义由网络An0给出||An1||... ||Ank.图4给出了一个计划和相应的时间自动机的例子。5从时间自动机在本节中，我们定义了TA规范A的两种观察者。它们的特点是对时间的观察能力。的S. Bensalem等人/理论计算机科学电子笔记113（2005）2335δ⊆首先，所谓的模拟观察者（术语取自[16]）可以观察一组可观察的动作以及这些动作的确切时间戳。因此，这些观察者可以被认为拥有一个第二种，称为数字观察者（或双采样观察者），也可以观察一组可观察的动作，但他们只能访问一个数字时钟，也就是一个以给定周期δ滴答的计数器。 因此，当观察一个动作时，a发生在实时t，数字观测器只知道电流其周期时钟的值，即，[t]观测器的目标是确定给定的迹（由被观测系统生成）是否可能由指定A生成。如果是，则被观察的系统通过该测试，否则，它失败。模拟和数字观测器定义让我们把上述概念形式化。 设A是A/A的TA， 是一系列可观察的行为。A关于仿射网络的模拟观测器是一个全函数(4)O：RT（随机数）→ {0， 1}使得（5） <$ρ∈RT（<$obs）. .O（ρ）=1惠ρ∈ObsTra ces（A，ρobs）<$.因 此 ， 模 拟 观 察 者 只 执 行 成 员 测 试 ： 观 察 ρ 是 否 属 于 A 的 语 言 ， 即 ，ρ∈ObsTraces（A，obsobs）.注意，A在我们的设置中没有接受条件，因此，它的语言已关闭。还要注意，观察者必须是确定的，也就是说，每次给他们相同的观察结果时，他们都要提供相同的答案。因此，模拟观测器可以被看作是接受A语言的确定性机器。从时间自动机一般是不可确定的这一事实可以得出结论[2]，模拟观测器不能总是表示为时间自动机。此外，检查特定自动机是否是这种情况是不可判定的[26]。A关于ωb和δ >0的数字观测器（或称λ-采样观测器）是一个全函数(6)D：DT（随机数）→ {0， 1}使得（7） <$ρ∈DT（<$obs）. .D（ρ）=1惠ρ∈DigTraces（A，δbs，δ）<$.36S. Bensalem等人/理论计算机科学电子笔记113（2005）23⎨一0一科洛布斯基于状态估计技术的观测器自动生成接下来我们将展示，给定一个时间自动机A，如何为A自动生成模拟和数字观测器。该方法依赖于在[25]中提出的状态估计技术，其中它被应用于故障检测。状态估计是在给定一个观测值的情况下，计算A的与该观测值“匹配”的状态集，即，计算产生观测迹的某个迹线所能到达的所有可能状态的集合。 如果状态估计在整个观察期间保持非空，则后者确实可以由A生成，因为存在至少一个与观察相符然而，如果状态估计变为空，则该观察不能由A生成。状态估计并不比可达性分析更昂贵。事实上，在某些情况下，它更便宜。1如[25，19]所示，状态估计可以使用TA的标准数据结构表示，例如DBM[12]，并且可以使用各种版本的符号后继运算符计算，这取决于所需的估计器（模拟或数字）。生成模拟观测器考虑一个时间自动机A，它位于一个可观察的动作集合A上。A相对于最小值的模拟状态估计器是总函数SEa：RT（最小值）→2Reach（A），定义如下：Aσ（8）SE（ρ）={s|τσ∈RT（τ）。S→s<$P（σ）= ρ}。SEa（ρ）包含A在执行产生模拟观测ρ的序列之后可能处于的所有状态。现在，定义（九）O（ρ）=φ1，如果SEa（ρ）=/φ00，否则从定义中可以很容易地得出，如上定义的O是Aw.r.t.的有效模拟观测器。白痴我们继续讨论如何计算SEa设S是A的一组状态。设a∈R，t∈R.定义以下运算符：一(10) asucc（S，a）={sJ|s∈ S。 s→AsJ}(11) tsucc（S，t）={sJ|s∈ S。 τρ ∈ RT（τ\τOBSρ）的。 时间（ρ）=t s →AsJ}[1][3]研究了时间自动机中成员问题的最坏情况复杂性。在那里，它表明，对于自动机没有ε转换（即，完全可观察的），该问题是NP完全的，而对于具有ε-转换的自动机，该问题是PSPACE完全的（即，像可达性一样难）。S. Bensalem等人/理论计算机科学电子笔记113（2005）23370⎨D≤≤0一科洛布斯δasucc（S，a）包含在执行动作a之后S中的某个状态可以达到的所有状态。tsucc（S，t）包含S中某个状态通过一个不包含可观察动作且恰好需要t个时间单位的序列ρ所下面的命题展示了如何在ρ上递归地计算SEa（ρ）。提案5.1(12)(13)SEa（n）=tsucc（{sA}，0）SEa（ρ·（a，t））=asucc（tsucc（SEa（ρ），t−time（ρ）），a）生成数字观测器考虑一个时间自动机A，它位于一个可观察的动作集合A上。设δ∈R，δ >0.A相对于ωb和δ的数字状态估计器是总函数SEd：DT（ωb）→2Reach（A），定义如下：Aσ（14）SE（ρ）={s|τσ∈RT（τ）。S →s [P（σ）] =ρ}。SEd（ρ）包含A在执行产生数字观测ρ的序列之后可能处于的所有状态。现在，定义（十五）D（ρ）=1，如果SEd（ρ）/=00，否则从定义中很容易得出，如上定义的D是Aw.r.t.的有效数字观测器。和δ。滴答！x=10渴望滴答！9x11可延迟）v. x：=0完全周期的）v. x：=0具有偏差图五. 两个可能的滴答自动机。我们接着讨论如何计算D。我们首先用图5左边所示的Tick自动机形成A的乘积。这个自动机模拟了观测者的数字时钟，假设它是周期δ= 10的完美周期。也可以使用其他Tick自动机，如图中右侧的自动机，来模拟时钟偏移或漂移等现象。（注意，在这些情况下，DigTraces的定义必须是已修改。） 设乘积自动机为Atick=ATick。 我们假设38S. Bensalem等人/理论计算机科学电子笔记113（2005）230滴答声是一个新的可观察事件，而不是在地球上。 设S是Atick的一组状态。定义以下运算符：（十六）usucc（S）={sJ|s∈ S。τρ∈RT（τ\ τOBS）的。s→蜱虫 sJ}。usucc（S）包含S中某个状态通过不包含可观察动作的序列ρ注意，通过构造Atick，ρ的持续时间是有界的：因为tick是可观察的，并且必须在至多1个时间单位之后发生，所以time（ρ）≤1。对于a∈{tick}，定义：（十七） dsucc（S，a）= asucc（usucc（S），a）.d ∈ck（·，a），对k∈N，给出了d∈c（·，a）k次迭代的一个应用. 是这样的，dkc0（·，a）是幂函数，dkck+1（·，a）=dkc（dkck（·，a），a）.下面的命题展示了如何在ρ上递归地计算SEd（ρ）。提案5.2（十八）（十九）SEd（）={sAtick}SEd（ρ·（a，k））=dsucc（dsucck（SEd（ρ），tick），a）执行我们已经在IF环境之上实现了一个原型观测器生成工具，称为TTG[10]。IF建模语言允许指定由通过消息传递或共享变量进行通信的许多进程组成的系统，并包括诸如层次结构、优先级、动态创建和复杂数据类型等功能。IF工具套件包括用于仿真、模型检查和测试生成的各种TTG是用C++编写的，使用IF的基本库来解析和符号可达性的时间自动机与期 限 。TTG作为主要输入的规格自动机，写在IF语言，并产生一个O型线观察者。观察者将原始IF规范的一个迹和一组不可观察的动作作为输入。观测服务器既可以作为模拟观测器（默认），也可以作为数字观测服务器（-d选项）.6为例我们的案例研究是火星探测器控制器K9，特别是它的执行子系统，在美国宇航局艾姆斯开发。它是一个实验平台，用于自主轮式车辆，称为火星车，目标是探索火星表面。K9专门用于测试新的自主软件，ρS. Bensalem等人/理论计算机科学电子笔记113（2005）2339...ExecTimer.p.R.ocessWakeupTimes（）服务员执行时间表\\\\\/打开/关闭...executeTaskAction（）\--、\\/数据库（系统状态）J见图6。 K9 Rover建筑比如Rover ExecutiveRover Executive提供了一种灵活的方法，通过控制Rover的运动、实验设备和其他资源的计划来指挥Rover，同时考虑到指挥行动失败的可能性。Rover Executive是由NASA Ames的研究人员用C++编写的软件原型。它是一个多线程程序，由大约35，000行C++代码组成，其中9600行代码与实际功能相关。C++代码被手动翻译成Java和C，以使用三种技术进行工具实验：静态分析，模型检查和运行时分析[11，4]。系统描述Rover执行官由以下人员组成：• 一个名为Executive的主要协调组件。它提供了对计划如何执行的主要控制。Executive等待计划可用，并在计划执行结束时发出信号。因此，当计划准备就绪时，PlanWatcher发出信号，并等待执行结束以发送新计划。• 用于监视状态条件的组件由两个线程组成，数据库监视器DBMonitor只是监视数据库中的更改，而线程Internal决定需要对其执行什么操作。• ExecTimerMonitor是用于监视临时条件的组件。它由两个线程ExecTimer和ExecTimerWaiter组成。两人都很尊重--...PlanWatcher/internalRunAction（）internalDoAction（）doAction（），stopAction（），执行执行executePlan（）executeCurrentNode（）执行条件内部...DBMonitor、、......40S. Bensalem等人/理论计算机科学电子笔记113（2005）23启动节点0 922开始节点1 1932成功节点1 1932启动节点2 2942成功节点2 2942成功节点0 2942见图7。 对应于图4的平面的迹线。非常类似于DBMonitor和Internal• Rover 执 行 线 程 负 责 向 Rover 发 出 命 令 。 它 由 一 系 列 方 法 组 成 ， 包 括internalDoAction 、 doAction 、 stopAction 和 abortAction 。 Execution 运 行internalDoAction方法，其他方法只是由Execution在自己的线程上通过简单调用来调用。• 数据库只是接收对其方法的调用。通过数据库的方法对数据库的所有访问都由锁控制这些线程之间的同步是通过互斥和条件变量来执行的。结果由于知识产权限制，我们无法使用K9 Rover的扩展平台。然而，NASA为我们提供了一组由K9 Rover执行平台生成的100个计划和轨迹。我们应用我们的方法，使用计划到IF翻译器来获得每个计划的IF模型，并且TTG为计划的每个IF模型生成观察者。观察员随后被用来检查痕迹。其中一个计划如图4所示。计划中的时间单位为秒。图7中显示了执行平台生成的带有输入this计划的跟踪（跟踪中的时间单位为毫秒）。跟踪表明节点0在时间922开始，节点1在时间1932开始并同时成功完成，依此类推。这个跟踪不符合规范，因为后者要求节点2在开始后至少1秒完成（计划中节点2的块的第TTG需要几秒钟来生成观察者（这是一个C++代码生成过程，编译并与IF库链接）。观察者只需不到一秒钟的时间就可以将此声明定性为不符合。一般来说，所有的痕迹都在几秒钟内检查完毕S. Bensalem等人/理论计算机科学电子笔记113（2005）23417结论和今后的工作我们已经提出了一种方法来测试一致性的一类重要的实时应用程序的自动方式。这个类包括所有的应用程序，它的规范是可用的，并且可以被转换成一个时间自动机网络。特别是，该类包括机器人应用程序，其中规格被认为是描述机器人任务的计划。这样的计划可以自动转换为时间自动机[1]。该方法一方面依赖于从规范自动生成观察者，另一方面依赖于待测系统的仪器测试过程包括将仪表系统生成的轨迹馈送到观察器，观察器是一种测试设备，用于检查轨迹是否符合规范。我们已经在NASA K9 Rover案例研究中验证了该方法关于未来的工作，我们计划研究的仪器和跟踪生成问题。如上所述，通过识别执行平台事件和指定事件之