一句话：提出 Dara 混合模型检测方法，结合抽象建模与透明模型检测，缓解状态空间爆炸与验证人力成本。
摘要指出，构建正确的分布式系统实现仍然非常困难。现有方案大致分为两类：一类使用 TLA+、PlusCal 等抽象建模语言描述系统模型，再用 Coq、SPIN 等工具验证模型正确性，但需要投入大量人力；另一类如 MODIST、CMC、CHESS 等透明模型检测器可直接检测实现，却受状态空间爆炸影响，运行过慢而难以实用。Dara 提出一种混合模型检测方法，旨在结合抽象建模与透明模型检测的优势，以缓解状态爆炸和人工验证成本问题。摘要未给出具体技术机制与实验评估结果。
Building correct implementations of distributed systems continues to elude us. Solutions consist of abstract modeling languages such as TLA+, PLusCal, which specify models of systems and tools like Coq, and SPIN which verify correctness of models but require considerable amount of effort, or transparent model checkers like MODIST, CMC and CHESS which suffer from state space explosion, rendering them impractical to use as they are too slow.
DOI 原文 ·
@inproceedings{paperbot4646,
title = {Dara: hybrid model checking of distributed systems},
author = {Vaastav Anand},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3275438}
}