大数据实用 DevOps/跟踪检查
跟踪检查是一种方法，用于分析记录为带时间戳事件序列的系统执行。分析收集的日志以确定系统日志是否满足属性，通常在逻辑语言中指定。在肯定的情况下，采样的系统行为符合属性建模的约束；反之，系统行为 simply does not satisfy the property.
当用于指定属性的语言允许使用时间运算符时，跟踪检查是检查系统中发生的事件顺序以及事件对之间的时间延迟的正确性的一种方法。例如，如果属性要求某个节点的所有发射事件发生的时间不晚于最新的接收事件的十毫秒，那么在跟踪上检查属性会导致布尔结果，如果两个连续且有序的发射和接收事件对之间的距离小于十毫秒，则该结果为肯定。
DICE 中可用于执行跟踪检查（Storm 应用程序）的工具是DICE-TraCT。
当从监控系统获得的聚合数据不足以得出系统执行相对于某些特定标准的正确性时，跟踪检查特别有用。实际上，在某些情况下，这些标准是依赖于应用程序的，因为它们与应用程序本身的一些非功能属性相关，并且它们不依赖于应用程序执行的物理基础设施。
跟踪检查是一种可以实现此目标的可能技术，可以有意地用于从正在运行的应用程序的执行中提取信息。
涉及跟踪检查分析的逻辑语言通常是度量时间逻辑的扩展，它们提供称为聚合模态的特殊运算符。如果跟踪满足特定的量化特征，例如跟踪中事件的特定计数属性，则这些运算符成立。
根据 DICE 愿景，跟踪检查在验证之后执行，以允许持续的模型细化。通过日志分析获得的结果确认或反驳了验证任务的结果，该验证任务在设计时运行。设计时模型中的参数值与运行时值进行比较；如果两者都是“兼容的”，那么验证的结果有效，否则必须细化模型。
与运行时验证相关的研究领域在跟踪检查方面非常活跃。支持跟踪检查并提供在线或离线分析的工具多种多样。DICE 中的跟踪检查是离线应用的，但框架的进一步扩展可能会考虑在线分析，以改进设计师可以执行的模型驱动细化。据团队所知，DICE 是（之一）第一个将跟踪检查分析用于支持 DIA 模型驱动开发的尝试。跟踪检查引擎是可以在评估过程中使用的工具，选择特定引擎取决于设计师想要实现的分析类型。The 国际运行时验证竞赛 是比较可用工具和技术的最佳参考。以下是一些参与竞赛的工具，可以被视为 DICE 中使用和实现的工具的替代方案
- Rithm2 (论文): 用于验证具有扩展版本的 LTL 的日志跟踪的有效并行算法，该算法具有计数语义。
- MonPoly: LTL 的一阶扩展，丰富了聚合模态。
- ARTiMon: 用于分析带时间戳观察流的工具，可用于检测以基于时间逻辑的语言表达的危险。
跟踪检查分析的结果用于细化在设计时使用D-VerT验证的应用程序模型。
跟踪检查在运行时执行，但它基于在设计时定义的带注释的 DTSM 模型，这些模型包含正在分析的拓扑。
DICE-TraCT 被设计为包含 Soloist 语言 Soloist，它提供以下类别的聚合模态
- 事件e在长度为d的时间窗口中的出现次数，
- 事件e的最大/平均出现次数，在长度为d的时间窗口中，对右对齐的相邻非重叠子间隔（大小为h）进行聚合，
- 在长度为d的时间窗口中，发生在事件对e和e之间的平均时间，该事件对是特定相邻且交替的事件。
但是，一些基本功能，例如在给定时间窗口中对事件进行平均，已在简单的跟踪分析器中开发，以提高工具的灵活性。因此，用户可以利用最合适的引擎来执行日志分析。
DICE-TraCT 具有客户端-服务器架构：客户端组件是与 DICE IDE 完全集成的Eclipse 插件，服务器组件是 RESTful Web 服务器。客户端组件管理从用户定义的 DTSM 模型到中间 JSON 对象的转换，然后使用该对象调用服务器。服务器组件基于 JSON 文件的内容为跟踪检查引擎生成跟踪检查实例。
DICE-TraCT 是一个 Eclipse 插件，可以在 DICE IDE 中执行。要执行跟踪检查分析，必须使用 DICE::Storm 配置文件通过 UML 类图和活动图来指定 Storm 拓扑。这些图表可以通过拖放 DICE 工具栏中提供的 Eclipse 项目来轻松绘制，而注释可以在 DICE IDE 的底部面板中指定。
DICE-TraCT 可以通过合适的运行配置窗口进行设置，允许用户启动分析。用户可以指定
- 包含正在分析的模型的文件，
- 限制分析时间窗口持续时间的时限，
- 将通过拓扑日志计算其度量（sigma 和 avg_emit_rate）的Storm bolts 和 spouts 集，
- DICE-TraCT 服务器正在运行的 IP 地址和端口，以及
- 监控平台的 IP 地址和端口。
跟踪检查是在运行的部署应用程序上执行的，该应用程序是通过一个由**D-VerT**（验证工具）验证的抽象模型设计的，并且可能还使用了从模拟和优化工具获得的结果。用**D-VerT**进行分析所使用的参数值与通过**DICE-TraCT**对应用程序日志跟踪进行分析所获得的当前值进行比较。根据分析的类型（计数、平均值或定量）和拓扑结构，**DICE-TraCT**从监控平台（D-Mon）中检索日志并执行分析。结果可用后，将显示在DICE IDE中，以便用户可以改进应用程序模型，重新运行验证工具，并根据分析结果，根据需要更改实现。这个过程是迭代的，可以重复进行，直到验证工具不再检测到可能导致部署的应用程序在运行时出现意外行为的异常。
当日志包含合适的条目，能够评估时间公式或指标时，应用程序日志的跟踪检查可以成功实现。当要检查的属性仅引用由运行应用程序的数据密集型平台的监控服务跟踪的应用程序事件时，只需定义要评估的属性（或指标）并在选定的日志历史记录上运行跟踪检查器即可。另一方面，当要检查的属性引用应用程序框架未原生监控的应用程序事件时，跟踪检查需要对应用程序代码进行特定于应用程序的检测，以便监控服务可以记录评估感兴趣属性所需的那些特定于应用程序的事件。
**DICE-TraCT**目前支持Storm日志分析。
**DICE-TraCT**的当前实现能够分析两个与**D-VerT**执行的验证分析密切相关的不同参数。特别是，**DICE-TraCT**可以计算的两个可用指标是
- *`avg_emit_rate`* 是一个Spout节点的发送速率，定义为每秒发送的元组数量，以及
- *`sigma`* 是Bolt节点输出的元组数量与接收的元组数量之比。
通过跟踪检查获得的指标值可以帮助设计人员调整用于验证的模型，使用**D-VerT**。
跟踪检查分析可以仅限于特定的时间窗口，并且只考虑在有限时间内发生的日志条目。大小决定了多少日志事件被考虑用于评估指标（单位是毫秒）。
DICE-TraCT实现了三种不同的分析方式来计算指标。每种方式都依赖于用于分析日志的基础引擎的特性。参与跟踪检查分析的逻辑语言通常是指标时态逻辑的扩展，这些逻辑提供称为聚合模态的特殊运算符。这些运算符对于在日志中计数事件或计算特定时间窗口内发生次数的平均值并将该值与给定阈值进行比较很有用。因此，分析结果始终是布尔答案，可以是“是”或“否”。**DICE-TraCT**基于Soloist，但**DICE-TraCT**的当前实现也可以调用比Soloist更简单的跟踪检查器，该检查器旨在提供从日志中计算出的定量信息。
以下类型的分析可用
- *`counting`*：通过Soloist逻辑的所谓计数公式，它能够评估选定的指标。此选项将调用Soloists跟踪检查器。
- *`average`*：通过Soloist逻辑的所谓平均公式，它能够评估选定的指标。此选项将调用Soloists跟踪检查器。
- *`quantitative`*：它能够对日志进行定量分析，提取指标的值。
由Soloist跟踪检查器实例化的分析旨在提供布尔结果，该结果通过将日志中事件的发生次数与用户定义的阈值进行比较来计算。当启动**DICE-TraCT**时，关系<、=和>以及阈值可以通过适当的配置窗口指定。
**DICE-TraCT**是一个Eclipse插件，可以在DICE IDE中执行。为了进行日志分析，必须使用UML类图和活动图来指定Storm拓扑。可以使用DICE工具栏中可用的Eclipse项目通过拖放来轻松绘制图表，而注释可以在DICE IDE的底部面板中指定。
图2描述了实现Wikistats拓扑的Storm拓扑（有关实现详细信息，请参阅GitHub存储库）。该图是一个DTSM模型，它也用于**D-VerT**的分析。
**DICE-TraCT**可以通过“运行配置”窗口设置，允许用户启动分析。用户可以指定
- 包含正在分析的模型的文件，
- 正在分析的Storm组件，
- **DICE-TraCT**服务器运行的IP地址和端口。
分析允许提取与验证相关的模型参数，即在D-VerT分析的正式模型中使用的值。DICE-TraCT提取以下参数值
- sigma：Bolt发送的元组数量与接收的元组数量之比。
- alpha：Bolt处理一个元组所需的平均时间。
- 发送速率：Spout的平均发送速率。
图3显示了**DICE-TraCT**的运行配置以及定义Wikistats拓扑的组件列表。此外，图中右侧的最后一列显示了在执行**DICE-TraCT**后，拓扑中某些组件的分析结果。
**DICE-TraCT**旨在执行Storm应用程序的日志分析。它用于评估已部署应用程序的运行时行为，因为它会分析从监控平台收集的日志跟踪，以验证其是否符合设计时假设的行为模型。如果运行时行为不符合设计，则必须改进设计，然后重新验证以获得新的正确性认证。跟踪检查可以应用于向D-VerT执行的验证任务提供信息。跟踪检查从真实执行中提取D-VerT使用的模型参数值，这些值无法从框架的监控服务中获取，因为它们本质上是验证采用的建模的特定值。