Specifying a Distributed Database Arranged as Ring with the Process Algebra μCRL
In this paper, we have given a specification of a distributed algorithm using the process algebra μCRL. The algorithm is about how preserving the data replication consistency in a distributed database arranged as ring, where each node is attributed a unique integer as priority. An update emitted by a node with greater priority cancels the one emitted by a node with less priority when propagating on this last, while an update originated from a node with less priority will be stopped at a node with greater priority. This strategy has been proven valid by Roscoe et al. The algorithm that we have specified by mean of the process algebra is simplified:each node is supposed to update only one slot. We have given formal definitions of both the process running at a node and the global behavior of the system in the process algebra, and verified that the specification is well-formed using the utilities of the μCRL tool set.
process algebra specification distributed database μCRL
Minglong Qi Qingping Guo Luo Zhong
School of Computer Science & Technology, Wuhan University of Technology, Ma Fang Shan Campus, 430070 Wuhan
国际会议
杭州
英文
612-615
2006-10-12（万方平台首次上网日期，不代表论文的发表时间）