@inproceedings{cd10946ac45d488288182faa59943fd5,
title = "Model Checking Chandy-Lamport Distributed Snapshot Algorithm Revisited",
abstract = "Chandy and Lamport have proposed a distributed snapshot algorithm (called CLDSA). One desired property of CLDSA is as follows. Let s1 be the state in which CLDSA initiates, s2 be the state in which CLDSA terminates, and s∗ be the snapshot taken, and then s∗ is reachable from s1 and s2 is reachable from s∗. The property is called the distributed snapshot reachability (DSR) property. We give a more faithful formal definition of the property that involves two state machines MUDS and CL(MUDS), where MUDS is a state machine of an underlying distributed system (UDS) and CL(MUDS) is a state machine of the UDS superimposed by CLDSA, while the definition of the DSR property used in an existing study only involves CL(MUDS). We also prove a theorem on equivalence of the two definitions that guarantees the validity of the model checking approach used in the existing study.",
keywords = "Model checking, distributed snapshot algorithm, reachability, state machine",
author = "Doan, \{Ha Thi Thu\} and Wenjie Zhang and Min Zhang and Kazuhiro Ogata",
note = "Publisher Copyright: {\textcopyright} 2015 IEEE.; 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015 ; Conference date: 16-11-2015 Through 19-11-2015",
year = "2016",
month = mar,
day = "15",
doi = "10.1109/DCIT.2015.13",
language = "英语",
series = "Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
pages = "30--39",
booktitle = "Proceedings - 2015 2nd International Symposium on Dependable Computing and Internet of Things, DCIT 2015",
address = "美国",
}