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

摘要

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