大规模分布式系统实时可预测在线分析研究

鉴于大规模分布式系统的复杂性，对其进行调试、测试和监控是一项重大的挑战。现有的基于有限路径的在线模型检测方法缺少实时概念；可预测分析方法中缺少与定量时间有关的依赖。本课题提出了分布式系统定量时间依赖模型，通过动态实时向量时钟算法给出系统的一致状态。根据时间依赖等偏序关系和可预测调度算法得到实时计算格，通过窗口尺寸调整、时间依赖和BDD技术优化其存储和遍历。建立实时有限路径时态逻辑RFLTL的形式化模型，采用RFLTL描述带定量时间约束的安全性和活性性质，并用重写逻辑描述RFLTL典范项代数和典范可达模型。通过二叉决策有限自动机BDFSM压缩RFLTL状态空间，并根据重写逻辑提供的商代数模型、等式抽象和代数模拟抽象，结合现有的偏序规约、SAT/SMT等优化算法，通过实时计算格的划分，在现有谓词检测基础上，提供一个高效的分布式实时可预测在线分析方法，更有效地检测系统错误和性能缺陷。