大数据/质量验证的实用 DevOps
系统正确性的分析对于生产运行时行为保证正确的系统至关重要。然而，正确性的概念很普遍，需要根据嵌入该系统的特定场景进行细化。为此，需要考虑适当的标准来定义什么是正确性，这取决于所考虑的系统类型以及已实现系统在运行时应该表现出来的用户需求。DICE 中的验证旨在为 DIA 定义一个可能的正确性含义，并提供支持正式分析的工具。
DICE 中可用于 DIA 安全分析的工具是 D-VerT。DICE 中的安全验证用于检查 DIA 模型中是否可以到达不希望的配置，即故障，这包括不符合质量工程师指定的一些非功能性需求的行为。
验证旨在关注对不正确设计的时间约束效果的分析，这些约束可能会导致数据处理延迟。因此，设计人员可以使用分析工具推断出反映在验证结果上的不希望行为的原因。
时间约束的设计是软件设计的一个方面，在 DICE 中考虑的应用程序中非常重要。不可预见的时间延迟实际上会导致系统出现不正确的行为，这些行为可能以各种形式在运行时出现，具体取决于正在开发的应用程序类型。低估节点的计算能力会影响节点处理输入数据所需的时间，而这反过来又可能影响整个应用程序的时间跨度，因为处理延迟可能会引发连锁反应。例如，在流式应用程序中，节点的缓慢可能会导致消息在队列中累积，并可能导致内存饱和，除非有程序采取措施处理异常。在批处理应用程序中，不可预见的时间延迟可能会影响总处理时间并改变应用程序行为，从而违反与客户的服务等级协议。
据作者所知，目前还没有可用的工具提供专门针对 DICE 参考技术开发的这些特殊功能。
DICE 采用 模型检查 技术来验证在 DTSM 图表中指定的 DIA。验证问题由 DIA 的正式描述（一个包含有关正在分析的应用程序的时间特性的适当信息的带注释的 DTSM 模型）和表示其执行必须满足的属性的逻辑公式来指定。
DICE 中的验证过程依赖于基于稠密时间时态逻辑的完全自动过程，并且它是根据有界模型检查方法实现的。它被设计为以敏捷的方式进行：DIA 设计师使用轻量级方法执行验证。更准确地说，D-VerT 鼓励一种方法，在这种方法中，正式验证通过隐藏底层模型和引擎复杂性的接口启动。这些接口允许用户轻松生成要验证的正式模型以及要检查的属性，并消除对正式验证技术的专家的需求。
验证结果用于在设计时细化应用程序模型，以防 D-VerT 检测到异常（参见 用例）。
验证过程包括以下步骤。设计人员在 DICE IDE 中绘制一个类图，表示 DIA 的 DTSM 模型，然后根据她用来实现应用程序的所选技术提供分析所需的所有注释。当用户开始分析时，带注释的 DTSM 模型将转换为正式模型，该模型表示应用程序在运行时的抽象行为。根据要实现的系统类型 - 无论是 Storm 应用程序还是 Spark 应用程序 - 该工具选择要验证的属性类别并执行分析。最后，当结果可用时，用户请求 D-VerT 在 DICE IDE 中显示结果，以查看属性是否满足，如果未满足，则显示违反该属性的系统跟踪。图 1 显示了 D-VerT 工作流程的主要步骤：通过 DICE IDE 创建应用程序的 UML DTSM 模型，从 UML 模型到正式模型的自动转换，以及实际的运行验证任务。
如图 2 所示，D-VerT 采用客户端-服务器架构：客户端组件是一个与 DICE IDE 完全集成的 Eclipse 插件，服务器组件是一个 RESTful Web 服务器。客户端组件管理从用户定义的 DTSM 模型到中间 JSON 对象的转换，然后使用该对象调用服务器。服务器组件根据 JSON 文件的内容生成正式模型，然后将其提供给核心可满足性/模型检查 工具。此工具负责验证属性是否针对提供的公式集成立，即系统的正式模型。
工具的可用性取决于某些非功能性指标的数值估计的可用性，这些指标是D-VerT用户在标注经过验证的DTSM模型时需要的。这些值可以通过监测平台收集运行应用程序（其DTSM模型是从已实施的解决方案中提取出来的）的事件来收集，或者可以通过设计师的经验或通过从与分析中的应用程序类似的其他应用程序先前收集的历史数据来估计。
应用领域
[edit | edit source]当前版本的D-VerT支持
在Storm拓扑的情况下，瓶颈分析帮助设计师发现瓶颈节点，因为它们的计时特性设计不正确。计时约束的错误设计实际上会导致异常，例如（i）处理元组的延迟和（ii）队列占用量的单调增长。
在Spark作业的情况下，可行性分析旨在检查是否存在一个执行，其持续时间低于特定截止时间，从而证明这种执行的可行性，而有界性分析检查（对应用程序的空闲时间做出强假设）系统的所有可能执行是否低于某个阈值。
大多数流和批处理参考技术可以通过表示应用程序执行的计算的图形来描述应用程序。虽然在某些情况下，这些图形可以从以声明性方式定义的应用程序中派生（例如，在 Apache Spark 和 Apache Flink 中），但其他技术，例如 Apache Storm 和 Apache Samza，允许直接指定应用程序的拓扑结构，因此可以通过组合多个计算块以组合的方式定义应用程序。
Storm
[edit | edit source]通过实现应用程序的拓扑结构，在DTSM级别指定Storm应用程序。拓扑结构是一个由两类节点组成的图形。
- 输入节点（喷口）是信息的来源，它们在定义应用程序逻辑方面没有任何作用。它们可以通过与注入拓扑的数据流相关的信息来描述，并且它们的计算特征与定义拓扑的最终结果无关。
- 计算节点（螺栓）详细说明输入数据并产生结果，这些结果反过来被发射到拓扑结构的其他节点。瓶颈分析仅关注螺栓。
此外，拓扑结构精确地定义了节点之间的连接，节点间通信基于消息交换（消息称为元组）。因此，对于任何节点n，在设计时（DTSM模型）静态地定义订阅n的节点列表（即接收其发射的消息）和n订阅的节点列表。
D-VerT用户需要以下概念（和参数）来执行验证。
螺栓的行为由五个不同状态空闲、执行、获取、发射、失败的序列定义，其含义如下
- 空闲：目前没有元组在螺栓中处理。
- 执行：至少有一个但最多Takemax个元组目前正在螺栓中详细说明。
- 发射：螺栓将元组发射到所有订阅的螺栓。
- 获取：螺栓从队列中获取至少一个但最多有限数量的元组（由以下并行度值定义），并初始化适当数量的并发线程来处理所有这些元组。
- 失败：螺栓失败，任何先前状态都无法发生。
每个螺栓都有以下参数
- σ是一个正实数，它抽象了螺栓计算的功能。如果螺栓过滤元组，即传入元组的数量大于传出元组的数量，则0 < σ < 1，否则其值为σ ≥ 0。它表示输入流和输出流大小之间的比率。
- 并行度是喷口/螺栓中可能实例化的并发线程的最大数量。因此，一个活动的喷口/螺栓可以同时从其队列中发射/删除数量等于并行度值的元组。
- α是一个正实数，它表示螺栓处理一个元组所需的时间量。
- 重启时间（最小/最大）是一个正实数，它表示螺栓在失败后恢复其功能所需的时间量。
- 空闲时间（最大）是一个正实数，它表示螺栓可能处于空闲状态的时间量。
- 故障时间（最小）是一个正实数，它表示两次连续故障之间的时间量。
每个喷口由注入拓扑结构的元组的平均发射速率描述。
Spark
[edit | edit source]通过操作数据的有向无环图 (DAG)，在 DTSM 级别指定 Spark 应用程序，这些数据在称为阶段的节点中进行聚合。
Spark 中的基本数据结构是所谓的弹性分布式数据集 (RDD)。RDD 支持两种类型的操作
- 转换是对 RDD 执行的操作（例如，映射、过滤、连接、联合等等），这些操作会产生一个新的 RDD。
- 操作是对 RDD 执行的操作（例如，规约、计数、第一个等等），这些操作会返回通过在 RDD 上执行计算获得的值。
Spark 通过以适当的方式调度其操作来安排转换，以最大限度地提高并行执行的操作数量。阶段是并行地在数据许多分区上执行的一系列转换，这些转换通常以混洗操作结束。每个阶段都是一个计算实体，一旦其所有组成操作完成，就会产生结果。每个阶段包含执行阶段转换的许多任务；任务是单个数据分区上执行的计算单元。
DAG 实现的计算称为作业。因此，DAG 通过指定操作工作流来定义Spark作业的功能，该工作流指定操作 RDD 的阶段之间的依赖关系。两个阶段之间的依赖关系是优先关系；因此，只有在所有前驱阶段完成计算后才能执行一个阶段。
在运行时，实际的计算是通过工作器、执行器和任务在节点集群上实现的。工作器是能够在集群中运行应用程序代码的节点，它包含一些执行器，即运行任务并可能在工作器节点上存储数据的进程。
D-VerT用户需要以下概念（和参数）来执行验证。
- 延迟是每个数据分区的任务持续时间的估计，并且
- Tot_cores是执行任务的 CPU 内核数量。
- Tot_tasks是要执行的任务总数
- 截止时间是Spark应用程序的最大持续时间。
可以执行的分析如下
- Spark作业的可行性分析验证是否存在一个执行，其持续时间低于截止时间；
- 有界性分析检查系统的所有可能执行是否低于截止时间。
测试用例 - DigitalPebble 网络爬虫
[edit | edit source]D-VerT 是一个可以在 DICE IDE 中执行的 Eclipse 插件。为了执行正式验证任务，需要分别使用 UML 类图和活动图来指定 Storm 拓扑和 Spark 作业，并使用 DICE::Storm 和 DICE::Spark 配置文件进行方便地注释。可以使用 DICE 工具栏中的 Eclipse 项目进行拖放来轻松绘制图表，而注释可以在 DICE IDE 的底部面板中指定。
图 3 描述了实现 DigitalPebble 网页爬虫 的 Storm 拓扑。每个节点（无论是 spout 还是 bolt）都已使用执行瓶颈分析所需的参数值进行注释。
D-VerT 可以通过运行配置窗口设置，允许用户启动分析。用户可以指定的参数如下：
- 包含正在进行分析的模型的文件。
- 时间边界限制了解决器在拓扑分析中考虑的执行长度。由于 D-VerT 基于有界 模型检查 方法，因此时间边界是解决器可以用来生成拓扑执行的最大不同连续事件数。
- 分析中要使用的求解器插件。
- 要分析的受监控螺栓集。
- D-VerT 服务器运行的 IP 地址和端口。
分析允许检测系统可能的运行情况，导致至少一个螺栓队列的无限增长。如果 D-VerT 检测到问题，它将返回一个跟踪，证明了这种系统运行的存在——即违反有界属性的反例。跟踪以文本格式（即底层求解器的裸输出）和图形格式返回给用户。图 4 显示了这种输出跟踪的示例。它表示螺栓队列中元组数量随时间的变化。跟踪由前缀和后缀组成：后缀用灰色背景突出显示，捕获队列大小的增长趋势，因为它对应于系统中可以无限次重复的一系列操作。如果未检测到跟踪，则结果为 UNSAT。
图 5 显示了实现 WordCount 应用程序的 Spark DAG。
D-VerT 向用户显示的运行配置对话框允许他们选择要执行的分析类型（可行性或有界性），以及定义要使用的模型以及服务器 IP 和端口的参数。
Spark 分析返回布尔结果（是/否），指定属性是否被违反。否定响应附带了一个反例，证明了违反。
结论
[edit | edit source]DICE 中验证的主要成就是开发了抽象模型来支持 Apache Storm 和 Spark 应用程序的安全验证。这些模型是通过逻辑方法构建的。它们被设计为可配置的，并提供了一个分层结构，通过将验证层与模型 DTSM 图表分离，从而简化了与 DICE 框架的集成。开发了特定于模型的模型到模型转换，以从用户设计中获得可验证模型，后者通过 DICE IDE 中的验证工具包实现。