Rybu：Dedan环境中用于分布式系统验证的命令式风格预处理器
分布式、并行与集群计算
2017-10-10 v1
摘要
集成分布式系统模型（IMDS）被开发用于分布式系统的规约与验证，以及针对死锁的验证。基于IMDS，构建了Dedan验证环境。通用的死锁检测公式允许自动验证，无需任何时序逻辑知识，从而简化了验证过程。然而，遵循IMDS规则的输入语言对许多用户而言似乎陌生。出于此原因，创建了Rybu预处理器。其目的在于以命令式语言在更高抽象层次上构建大型模型。
引用
@article{arxiv.1710.02722,
title = {Rybu: Imperative-style Preprocessor for Verification of Distributed Systems in the Dedan Environment},
author = {Wiktor B. Daszczuk and Maciej Bielecki and Jan Michalski},
journal= {arXiv preprint arXiv:1710.02722},
year = {2017}
}
备注
16 pages, 1 figure