Model checking distributed systems by combining caching and process checkpointing
Model checking distributed systems by combining caching and process checkpointing
复制标题
DOI：
10.1109/ase.2011.6100043
复制
发表时间：
2011-11
期刊：
影响因子：
--
通讯作者：
Watcharin Leungwattanakit;Cyrille Artho;M. Hagiya;Yoshinori Tanabe;M. Yamamoto
中科院分区：
文献类型：
--
作者：
Watcharin Leungwattanakit;Cyrille Artho;M. Hagiya;Yoshinori Tanabe;M. Yamamoto
通过模型检查对分布式软件系统进行验证并不是过程间通信，这不是一项简单的任务。许多软件模型检查器仅探索单个多线程过程的状态空间。最近的工作提出了一种应用缓存来捕获主过程与其同行之间的通信的技术，并允许模型检查器完成状态空间探索。尽管以前的工作在主过程中处理了非确定性输出，但要产生确定性输出需要任何同行程序。本文介绍了过程检查点工具。缓存和过程检查点的结合使得可以在交流的两面处理非确定性。同行状态被保存为检查点，并在模型检查器回溯并产生缓存中不可用的请求时恢复。我们还介绍了控制检查点创建和由检查点工具引起的开销的策略概念。
Verification of distributed software systems by model checking is not a straightforward task due to inter-process communication. Many software model checkers only explore the state space of a single multi-threaded process. Recent work proposes a technique that applies a cache to capture communication between the main process and its peers, and allows the model checker to complete state-space exploration. Although previous work handles non-deterministic output in the main process, any peer program is required to produce deterministic output. This paper introduces a process checkpointing tool. The combination of caching and process checkpointing makes it possible to handle non-determinism on both sides of communication. Peer states are saved as checkpoints and restored when the model checker backtracks and produces a request not available in the cache. We also introduce the concept of strategies to control the creation of checkpoints and the overhead caused by the checkpointing tool.