基于TLA+形式化规范模型检查的分布式系统测试方法及装置

摘要

本发明公开了一种基于TLA+形式化规范模型检查的分布式系统测试方法及装置，所述方法包括：针对目标分布式系统的TLA+形式化规范，将所述TLA+形式化规范的要素映射到所述目标分布式系统的实现中，并收集所述目标分布式系统的运行数据；使用TLC模型检查器验证所述TLA+形式化规范，获取验证过正确性的抽象状态空间图；对所述抽象状态空间图进行路径遍历，将得到的每一条路径视为一个测试用例；基于所述测试用例对所述目标分布式系统进行受控测试，得到受控测试数据；将所述运行数据与所述受控测试数据进行比对，以生成测试报告。本发明可以发现分布式系统潜在的缺陷。