用于分布式应用确认的模型检查

摘要

本发明公开了用于分布式应用确认的模型检查。此处描述了模型检查系统，该模型检查系统通过提供模型和通用框架来检查应用不变属性、检测异常行为并监视应用健康从而更有效地验证和确认分布式应用的设计。模型检查系统针对从应用的正式描述所导出的应用模型来检查在线应用行为。该系统将具体应用制定为抽象模型以及期望在所有条件下适用于应用的多个规则或属性。模型检查器将实际应用执行与模型相比较，并且确认属性保持为真或是报告属性被违反。由此，模型检查系统提供了在更现实的生产条件下对分布式应用的更有效且全面的确认。

主权项

一种用于执行分布式应用以及验证分布式系统行为的正确性的计算机实现的方法，所述方法包括：接收描述所述分布式应用的期望行为的多个模型，其中通过监视学习模式中的分布式应用来生成所述多个模型，并且进一步在所述学习模式中基于所报告的错误是不正确的错误的确定来更新所述多个模型，其中接收多个模型包括接收所述分布式应用的一个或多个不变属性，其中所述多个模型包括有限状态机(FSM)模型、错误模型以及性能度量模型中的至少一个，所述FSM模型表示所述分布式应用中的各个机器，其中每个FSM包括用于验证所述FSM中每个状态的统计信息，所述错误模型描述所述分布式应用的至少一个稳定属性，所述错误模型进一步包括错误类型指示符、错误严重性指示符和用于提取用于事件相关的相关关键字的关键项，所述性能度量模型包括硬边界阈值或者软边界阈值，其中性能统计信息超过所述硬边界阈值不能进行而超过所述软边界阈值不能停留超过设定时间段，所述多个模型进一步包括在所述多个模型中将事件相关的依赖图；在线或离线地开始模型检查服务，所述模型检查服务监视所述分布式应用的执行以检查所述分布式应用的行为；收集一个或多个轨迹，所述一个或多个轨迹将所述分布式应用的行为描述为发生在所述分布式应用的分布式组件处的一系列一个或多个事件；基于所收集的轨迹来标识一个或多个事件；针对所标识的事件来检查所接收的多个模型，以确定是否已发生任何非期望的应用行为，其中所述非期望的应用行为选自包括以下的组：违反所述FSM模型之一的状态转换、由所述错误模型之一指定的错误或违反所述性能度量模型之一；以及在通过在所述依赖图中标识与所述非期望的应用行为相关的事件来确定模型检查失败之后，标识与所述失败的模型检查有关的根本原因事件；以及基于所标识的根本原因和失败的模型检查来报告错误，其中前面的各步骤由至少一个处理器来执行。