嵌入式软件调试与验证3动态时态断言

3 使用动态时态断言进行调试

3.1 引言

软件产业发展迅速，程序规模越来越大。相比之下，调试文献的进展却相对缓慢。大多数调试器只适用于某一类或某一组错误。程序错误可能是由多种情况造成的，并在其根本原因出现很久之后才被发现。了解源代码和程序的执行行为对于定位和找到大多数错误的原因至关重要。这种理解可以通过不同的方式来实现；一种方式是采用不同的调试程序，捕捉、描绘、分析和研究程序在不同执行点和执行点之间的状态。

典型的交互式源代码级调试器是最有价值的调试工具之一，但它在很大程度上依赖于用户进行实时调查的能力。它可以帮助程序员定位并找到错误的根本原因，具体方法是逐步浏览源代码并检查当前的执行状态。

源代码级调试技术（如条件断点和观察点）可在调试会话期间动态插入。它们可以检查执行属性，并在满足条件时停止执行。尽管这些断点具有条件性和动态性的优势，可以随时插入、删除和修改，但它们仍然受其位置的限制；目标程序源代码中的确切行号，以及执行时该位置上引用变量和对象的当前状态。例如，类变量可能在一个方法中被分配了坏值，而当导致崩溃或核心转储的错误被揭示时，该方法并不在堆栈中。这可能会迫使用户对同一错误运行多个调试会话，然后才能理解该错误。通常情况下，用户可以调查当前状态。如果没有证据表明错误的根本原因，他/她可能会重新开始执行，希望能停在一个较早的点上，在那里仍然可以找到错误的原因。相比之下，时态断言是一种使用时态逻辑（TL）的逻辑表达式，目的不是验证一种状态，而是验证一连串的执行状态，如代码块内变量值变化的序列。

为了在传统的源代码级调试会话中引入动态时态断言（Dynamic Temporal Assertions，DTA），本研究对名为UDB的源代码级调试器进行了扩展，增加了实时时态断言（在实时调试会话中生成）。UDB是Unicon编程语言的源代码级调试器；它与 Source Forge 上的Unicon语言发行版一起打包，也可从unicon.org下载。除了时态断言扩展外，UDB的命令集与GDB相同。本研究之所以使用UDB而不是GDB，是因为UDB具有更高层次的执行监控抽象，比GDB更容易扩展。

UDB 支持的新 DTA 断言不受普通断点的限制，如局部性和时间性。UDB 的 DTA 断言有三个目的：

1.扩展传统源代码级调试器的条件断点和观察点的可用性。这简化了验证关系的能力，这些关系可能会延伸到整个执行过程，并检查评估状态之外的信息。

2.减少用户为进行基于状态的调查而不得不停止和单步执行的次数。

3.通过测试和验证功能来增强传统的基于断点的调试会话。

在两个实时程序上进行时态断言的可能性：

两个同级程序的时间断言的可能性：

3.1.1 DTA断言与普通断言

在源代码中插入标准的代码内断言是为了验证前置和后置条件或检查某些变量和表达式的值。一般来说，典型的普通断言有三个局限性：

• 位置性

普通的代码内断言受其位置（作用域）的限制；即使根据当前的执行状态，它是有效的，也不能引用其他作用域的变量。断言存在于函数中；每个断言都可以引用局部变量和全局变量。如果作用域是方法，它可以引用任何类变量。事实上，典型的断言无法检查或验证其他函数或方法中的局部变量，即使该外来局部变量是静态的，或者仍然存在于当前程序执行状态的堆栈中。例如，如果用户需要检查存储过程foo()中变量x的值与存储过程bar()中变量y的值，该怎么办？

• 时间性

普通的代码内断言受当前执行状态的限制。它只能检查引用变量的当前值。例如，如果用户需要检查变量x的值与x之前甚至初始值的比较，该怎么办？普通断言就会再次失去作用。

• 动态性

普通的代码内断言仅限于源代码，它是在源代码中编写和编译的；任何更改或修改都需要重新编译和重建可执行文件。如果普通断言评估为假，它可能会提供警告语句或终止执行。如果用户想进行调查，可以通过收紧或放宽条件或添加附近的断言来修改断言。

3.1.2 DTA断言与条件断点

条件断点和观察点是在调试过程中动态插入的。它们可以检查执行属性，并在满足条件时停止执行。尽管这类断点具有条件性和动态性的优势，可以随时插入、删除和修改，但它们仍然受其位置的限制，即目标程序源代码中的确切行号，以及执行时该位置上引用变量和对象的当前状态。而 DTA 断言可以引用在评估时不可访问（在当前执行状态下不活动）的变量。这一特性解决了图 3.2 所提供的问题，该图显示过程 foo() 和 bar() 是 baz() 的同级变量。

3.2 使用DTA断言进行调试

一般来说，源代码级调试器的用户会遇到以下问题：

1. 提供的执行历史信息有限，而且

2. 缺乏自动跟踪和分析调试技术，而这些技术可以帮助用户验证各种执行状态。

在典型的源代码级调试器中，DTA断言提供了条件断点和观察点的扩展。它们采用实现时态逻辑运算符的代理，每个代理都有自动跟踪机制。跟踪数据由断言驱动；实时收集和分析相关信息。不同的DTA断言可以动态、灵活地应用于不同的执行属性。每个断言都能验证程序属性，这些属性可能会扩展到一系列执行状态。下图使用时态断言检查不同作用域的变量：

例如，调试过程可能包括检查不同作用域的变量值。程序main()调用isPrime()，当传递的参数是一个质数时，它返回true。上图中提供的时间断言说明了如何将变量i的当前本地值与存储过程main()中变量i的最后值（用 main:i 表示）进行比较。该DTA断言假定参数i的值在isPrime()执行期间不会改变。然而，由于程序正在修改i的值，因此在isPrime()函数中每次改变i的值（时间状态）时，该断言的值都会变为false，并且在每次从isPrime()函数返回时（时间间隔），该断言的值都会变为false。

下图：时态断言：范围和时间间隔

3.3 设计

DTA断言并不取代传统的断点或观察点，相反，它们提供了一种减少断点或观察点数量的技术，这意味着它们可用于减少执行停止的次数，并改善整个调查过程。这些时态断言通过时态逻辑运算符代理（时态代理）推进断点。在停止执行时，除了源代码级调试功能外，用户还可以删除、启用、禁用和修改现有断言，甚至在有错误的程序源代码中的任何位置插入新的 DTA 断言；所有这一切都无需重新编译目标程序源代码或将其重新加载到调试器中。

UDB 支持三种DTA断言。每种类型都有自己的时态代理集。所有这些DTA都可以引用执行属性和其他内部扩展代理。

表 3.1 原子数据相关代理

表 3.2 原子执行行为相关代理

3.3.1 过去时DTA断言

这类断言包括四个过去时间操作符。这些操作符利用在进入断言作用域和到达断言源代码位置之间保留的信息。在插入时，调试器开始保留相关信息，以便在断言评估过程中使用。当执行到达虚拟执行点（断言在错误程序空间中的挂钩位置）时，将对断言时间间隔进行评估。如果由于某些信息缺失（可能在断言生命周期内从未使用过超出范围的引用数据）而导致评估无法完成，则断言评估会被标记为无效。这四个DTA断言是

1. alwaysp() {expr}：断言一个表达式在每个时态、时态间隔和整个执行过程中必须始终成立（评估为 true）。

2. sometimep() {expr}：断言表达式必须在每个时间间隔和整个执行过程中至少成立一次。

3. previous() {expr}：断言表达式必须在时间间隔结束前的最后一个状态成立。

4. since() {condition ==> expr}：断言表达式必须在条件为真后一直到时间间隔结束，以及在每个时间间隔内都必须成立。

3.3.2 未来时DTA断言

这类断言包括四个未来时间操作符。这些操作符利用在到达断言源代码位置和离开断言范围之间保留的信息。这些操作符的代理在评估触发时开始监视引用对象，调试器开始保留相关信息，直到断言的时间间隔评估完毕。如果执行在断言的时间间隔结束前终止，用户可以检查未完成的时间间隔中的时间状态。这四个 DTA 断言是

1. alwaysf() {expr}：断言表达式必须在每个状态、时间间隔和整个执行过程中始终成立（求值为 true）。

2. sometimef() {expr}：断言表达式必须在每个时间间隔和整个执行过程中至少成立一次。

3. next() {expr}：断言表达式必须在时间间隔的第一个状态成立。

4. until() {condition ==> expr}：断言表达式必须从时间间隔开始一直到条件为真或时间间隔结束，且在每个时间间隔内都必须成立。

3.3.3 全时 DTA 断言

这类断言包括两个全时运算符。这两个操作符基于进入断言作用域和退出断言作用域之间的时间间隔。当进入断言范围时，断言开始保留相关信息并评估其时间状态。当执行退出断言范围时，将对断言的时间间隔进行评估。这两个 DTA 断言是

1. always() {expr}：断言表达式必须在每个状态、时间间隔和整个执行过程中始终成立（评估为 true）。

2. sometime() {expr}：断言表达式必须在每个时间间隔和整个执行过程中至少成立一次。

3.4 断言的评估

每个已达成（已评估）的断言至少有一个时间间隔。时间间隔由一系列时间状态组成。时间间隔由断言范围和种类定义。断言的范围是根据断言命令中提供的源代码位置定义的。该范围是围绕断言位置的过程或方法。上图显示了所有三种时态断言的时间间隔，它们都与所提供的位置有关。断言的作用域和种类共同定义了时间间隔。尤其是过去时DTA断言的时间间隔始于进入断言的作用域（调用作用域过程），止于进入作用域后第一次到达断言的源代码位置。

未来时间DTA断言的时间间隔始于进入断言作用域后第一次到达断言的源代码位置，止于退出断言作用域（从作用域过程返回）。在这种时间断言中，在时间间隔结束之前，源代码位置可能会被击中不止一次。

全时DTA断言的时间间隔从进入断言作用域开始，到退出该作用域结束；与所提供的源代码位置无关。
在调试会话期间，用户有可能拥有多个断言，每个断言有多个时间间隔，每个时间间隔有多个时间状态。参见下图。每个 DTA 断言都要经过三级评估：

1. 基于状态：时间层（单一状态变化）。该评估由断言引用对象的任何变化触发。

2. 基于时间间隔：连续状态序列。当断言的时间间隔结束时（退出断言范围），就会触发评估。

3. 基于整体执行：一系列连续的时间间隔。该评估由执行结束触发。

时态断言评估示例：

断言被命中 t 次 [ $$H_1$$..$$H_t$$ ]。每次命中代表一个时间间隔，该时间间隔由不同数量的状态组成；每个状态都被评估为"True"或 "False"。每个"时间区间"的评估都是基于其基于状态的评估的连接正则表达式（在该特定命中$H_i$$ 上）。最后，在整体时间层面上，根据之前所有基于时间间隔的评估的连接正则形式，再次对断言进行评估。下图是调试过程中对各种时态断言（n 个 DTA 断言）的评估示例：

UDB的DTA断言在调试器端进行评估。默认情况下，只要断言评估为假，源代码级调试器就会以类似于断点的方式停止执行。调试器通过评估摘要将控制权移交给用户。

3.4.1 时间周期和限制

时序周期定义了连续时序间隔的最大次数（时序级评估时间的最大次数），它定义了整体评估。周期的默认值为无限次评估。时间限制定义了每个时间间隔中考虑的时间状态的最大数量。时间限制的定义会根据参考的时间断言类型而改变。特别是

1. 在过去时 DTA 断言中：限制定义了到达断言源代码位置之前和进入断言范围之后的最大连续状态数。

2. 在 Future-Time DTA 断言中：limit 定义了到达断言源代码位置后和退出断言范围前的最大连续状态数。

3. 在全时 DTA 断言中：limit 定义了断言的源代码位置达到之前和之后在断言范围内的最大状态数。

默认限制由断言作用域执行期间遇到的任何时间状态（时间间隔）定义，并基于其时间间隔。用户可以使用limit命令设置该限制，从而减少每个时间间隔内考虑的时间状态数量。

3.4.2 评估日志

此外，断言日志使用户能够查看每个断言的评估行为（评估历史）。调试器为每个断言维护一个哈希表。它将断言的时间间隔映射到列表中，列表中包含了断言的时间状态基础评估信息。每个列表反映一个时态区间，其中保留了每个时态的评估顺序和结果。每个列表反映一个时态区间，也根据其顺序进行维护。已完成评估的时间间隔会被标记为"True"或 "False"。如果评估过程已经开始，但最终结果仍未完成，或许还未到达时间间隔的终点，则这些时间间隔会标记为 "待定"，直到完成为止。这将把 "待定 "转换为 "True"或 "False"。不过，有些断言可能永远不会被触发进行评估；出现这种情况的原因可能是在特定运行期间，执行从未达到断言的插入点。这些断言的命中计数器设置为零。

参考资料

• 软件测试精品书籍文档下载持续更新 https://github.com/china-testing/python-testing-examples 请点赞，谢谢！
• 本文涉及的python测试开发库 谢谢点赞！ https://github.com/china-testing/python_cn_resouce
• python精品书籍下载 https://github.com/china-testing/python_cn_resouce/blob/main/python_good_books.md
• Linux精品书籍下载 https://www.cnblogs.com/testing-/p/17438558.html

3.4.3 DTA断言和原子代理

原子代理是一种特殊的扩展代理（非时态逻辑代理）。它们扩展了DTA断言的可用性，有助于验证不同执行状态下更具体的数据和行为关系（见表 3.1 和 3.2）。在 DTA 断言中使用原子代理时，原子代理会保留和处理数据，并观察与所用断言相关的行为。断言范围决定了代理何时开始工作，以及它能保留和处理的数据范围。例如，如果断言使用了max(var)或min(var)原子代理，代理就会在断言时间间隔内始终分别保留最大值或最小值。

这些原子代理为DTA断言及其基本时态逻辑运算符的实用性增加了更多的先进性和灵活性。特别是，引用原子代理的DTA断言可以轻松检查和比较这些原子代理获得的数据，这些原子代理封装了简单的数据处理，如查找最小值、最大值、总和、变化次数或平均值。例如，假设一个静态变量根据一个条件语句发生变化，当条件为真时，该变量递增，当条件失败时，该变量递减。如果用户对该变量达到新的最大值或最小值的时间点感兴趣，该怎么办？DTA断言为这种情况提供了一个简单的解决方案。

不同UDB的时间断言示例

例如，当变量x变为大于或等于y 时，断言1将暂停执行。又如，假设用户对无限递归背后的原因感兴趣；也许递归函数中的一个关键参数没有变化。DTA断言提供了一种机制，可以保留上次调用的参数值，并将其与当前调用的值进行比较，见断言 2。如果 old(x) == current(x)，断言将停止执行，并将控制权交给调试器，用户可以在调试器中进行进一步调查。当然，还有其他原因可能导致无限递归，例如连续调用时关键参数值的变化方向相反。

此外，DTA断言简化了在函数返回值和循环迭代次数等程序属性上插入断言的过程。例如，用户可以在函数内部插入一个断点，以调查函数的返回值，或对返回表达式的值进行代码内断言。DTA断言提供了一种更简单的机制；参见第 3 号断言。第4个断言指出，文件test.icn中第50行的while循环总是迭代少于100次。最后断言5显示了如何对函数的调用次数设置DTA断言；该断言将在调用次数为1000时停止执行。使用传统的源代码级调试功能（如断点和观察点）很难实现这一特殊断言。

3.5 实现

DTA断言实际上是在源代码级调试过程中即时插入到有错误的程序源代码中的。UDB的静态信息用于协助用户并检查插入断言的语法和语义。每个断言都与两组信息（1）基于事件的信息和（2）基于状态的信息相关联。调试器会在插入时自动分析每个断言，以确定每组信息。它能找到在评估过程中需要遇到的代理类型。如果使用了任何扩展代理，调试器会建立该代理的实例，并将其与相关对象关联。

UDB在Unicon虚拟机中对事件掩码和事件值的使用

主机调试器维护一个哈希表，将每个断言源代码位置映射到其相关对象（代理）。断言对象负责维护和评估其断言。它包含的信息有：(1) 已解析的断言；(2) 所有引用变量的列表；(3) 包含所有时间间隔及其时间状态的列表；(4) 断言事件掩码：对每个断言进行监控的一组事件代码；该事件掩码包括任何引用代理的事件掩码。执行事件是实时获取和分析的。一些事件用于控制执行，而另一些事件则用于获取信息，以支持基于状态的技术。

每个断言都有自己的事件和值掩码，这些掩码是根据断言自动构建的，见上图。所有启用的断言事件掩码的联合集与调试核心事件掩码统一。其结果是调试核心在错误程序执行过程中请求的事件集。每当断言被添加、删除、启用或禁用时，这组事件就会被重新计算。同时UDB的调试核心会开始向错误程序询问这组新事件。任何断言事件掩码的改变都会改变调试核心转发给该断言对象的事件集。时态逻辑代理会自动获取错误程序的状态信息，以评估DTA断言。每个代理都会自动观察断言引用变量，并将其信息保留在调试器空间中。

3.6 评估

DTA 断言提供了验证关系的能力，这些关系可能会延伸至整个执行过程，并检查当前评估状态之外的信息。DTA 断言的时间逻辑运算符是内部代理。这些代理可以引用其他原子代理，从而访问有价值的执行数据和行为信息。UDB 的 DTA 断言具有以下功能：

• 动态插入、删除、启用、禁用和修改。断言可在调试过程中即时管理，无需修改源代码或可执行代码。

• 无断言源代码支持的非破坏性编程方式。一般来说，只有在程序开发、测试、验证、确认和调试过程中才需要调试信息。

• 断言实际上是作为错误程序源代码的一部分插入和评估的。所有断言都存在于调试会话配置中；每个断言都由调试器在调试器执行空间中进行评估。调试器自动维护基于状态的技术，以确定评估每个断言所需的信息，并使用基于事件的技术来确定何时何地触发每个断言的评估过程。一些基于程序状态的信息是在断言评估前收集的，而其他信息则是在评估过程中获取的。所有 DTA 断言都将作为目标程序空间的一部分进行评估。

• 可选的评估套件，用户可指定评估操作，如停止、显示和隐藏。显示操作通过打印语句丰富了断言的代码内跟踪和调试功能，用户可确保评估已达到某些点，且引用变量满足条件。

• 记录断言评估结果的功能。这样，用户就能查看特定运行的断言评估历史。已评估的断言会以"True"或 "False"标记。某些 DTA断言可能会在未来引用数据；这些断言会在基于状态的精确评估中标记为 "无效"。断言的间隔标记有计数器，用于跟踪其执行顺序。如果某个断言从未被执行过，则用其计数器值来区分，在这种情况下计数器值为零。不同运行的日志比较将在今后的工作中考虑。
  最重要的是DTA断言可以超出插入位置的范围。每个断言都可以引用在以前的状态中存在，但在评估点不存在的变量或对象，而且每个断言都可以将以前的变量值与当前或未来的值进行比较。每个DTA断言都隐含地使用各种代理来跟踪引用对象，并保留其相关状态信息，以便在评估时使用。

3.6.1 性能

考虑到时间方面的性能，时态断言的实现采用了保守的基于断言的事件驱动跟踪技术。它只监控相关事件；事件掩码和值掩码在插入时为每个断言自动生成。时间断言的评估分为三个层次。首先是基于状态的级别，它取决于所引用的执行属性的任何变化。第二级是基于时间间隔的级别，由断言范围和种类决定。第三层是整体评估层，每次执行都会进行一次评估。不同的断言可以引用不同的执行属性。因此，各种断言的成本会有所不同。

为了了解时态断言对目标程序的执行和调试时间的影响，我们在一个简单的程序中应用了一个简单的时态断言。程序打印 1 到 100,000 之间的数字；见图 3.9。该时间断言使用了不同大小的时间间隔。这些时间间隔的大小分别为 1、100、1000、10000、50000 和 100000。实验基于八种运行，每种运行观察五次，并报告这些时间的平均值。这些运行类型包括测量独立模式（不涉及监控）下的程序时间、UDB 监控下未应用断言的程序时间，以及带有不同时间间隔的断言的程序时间。上图显示了这些时间断言对执行时间的影响。

3.7 挑战与未来工作

与典型断言、条件断点和观察点相比，使用DTA断言进行调试更具优势。与此同时，它也面临着一些挑战和限制，其中一些挑战和限制是基于断言与可执行源代码的关联、在调试器中评估断言，以及源代码级调试器以合理的性能获取和保留基于事件和状态的相关信息的能力。

首先，如果断言引用了在断言作用域内无法访问的变量，调试器应自动跟踪这些变量并保留其相关状态信息，以便在断言评估时使用。这样DTA断言就可以访问在断言评估时不存在的数据。
其次，如果断言源代码位置与语句重叠怎么办？应该先评估断言还是语句？保守的做法是，只有当语句中没有断言引用的变量，或者语句没有赋值给任何断言引用的变量时，才考虑在语句之后评估断言。但是，如果语句将赋值给任何断言引用的变量，则可以在语句评估之前和之后对断言进行评估。如果两次评估结果不同，如一个为真，另一个为假，或两个都为假，断言将停止执行，并将控制权交给调试器和用户进行调查。本文介绍的工作采用了最简单的方法，即在语句之前评估断言。此外，如果断言没有与可执行语句重叠，AlamoDE框架就无法报告非可执行行的行号事件。只有当该行号中的语句被获取并执行时，才会报告行号事件。在确认断言已成功插入之前，通过检查断言源代码位置来实现这一点。它还会检查行号是否为空或是否已注释。

最后，如果引用的变量是对象或数据结构（如列表），这可能会导致两个问题。首先，由于别名关系，该对象会在其他名称下发生变化。其次，如果对象是本地的，它可能会在评估时间之前被垃圾回收器处理掉。我们可以扩展这种实现方式，以实现捕获变量，从而观察结构中的某个元素，或者利用别名跟踪机制来保留所有可能以不同名称发生的变化。本文介绍的时态断言的实现并没有涉及堆变量，这将留待今后工作中解决。

3.8 小结

DTA断言将C/C++、Java和C#等主流语言中的代码内断言技术的扩展版本引入源代码级调试会话。这些时态断言可帮助用户测试和验证不同执行状态下的不同关系。此外，断言评估操作（如 show）提供了在源代码级调试会话中使用打印语句进行调试和跟踪的感觉。它们让用户有机会知道执行已达到该点，断言表达式已评估为真；它还让用户有能力中断和停止执行，以便进行更多调查。记录断言评估结果的功能可让用户查看评估过程。用户可以查看汇总结果，了解哪些出错，哪些正常。

源代码级调试器可通过不同的断点和观察点有条件地停止执行。在每次停止时，用户将通过浏览调用堆栈和变量值手动调查执行情况。源代码级调试器要求用户对错误提出假设，并让用户通过断点、观察点、单步和打印来手动研究这些假设。相比之下，DTA 断言要求用户提出逻辑表达式，断言与错误暴露行为相关的执行属性，调试器将验证这些断言。断言表达式可以引用不同执行状态、范围和不同时间间隔的执行属性。此外，与只评估当前状态的条件断点和观察点不同，DTA 断言能够引用在评估时无法访问的变量（在当前执行状态下不活动）。

DTA断言并不能取代传统的断点或观察点，但它提供了一种减少断点或观察点数量并改进整个调查过程的技术。DTA断言减少了人工调查执行状态的工作量，例如减少了错误程序停止调查的次数。

最后，利用时态断言进行调试并非新鲜事。2002年，Jozsef Kovacs等人将时态断言集成到并行调试器中，用于调试并行程序。2005 年，Volker Stolz 等人在 AspectJ pointcuts 上使用LTL来验证程序执行过程中由方面触发的属性。2008 年，Cemal Yilmaz等人提出了一种使用时间谱作为程序执行抽象的自动故障定位技术。然而，就我们所知，我们是第一个将典型源代码级调试器的条件断点和观察点功能与基于时态断言的命令进行扩展的人，这些命令捕捉并验证了一系列执行状态（时态和时态间隔）。此外，这些断言还可以引用范围外变量，这些变量在评估时可能不在执行状态中。文章来源地址https://www.toymoban.com/news/detail-710122.html

到了这里，关于嵌入式软件调试与验证3动态时态断言的文章就介绍完了。如果您还想了解更多内容，请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章，希望大家以后多多支持TOY模板网！