On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency
On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency
复制标题
分布式算法验证框架：分布式检查与一致性
DOI：
10.1007/978-3-319-92612-4_9
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
S. Akili
中科院分区：
文献类型：
--
作者：
K. Völlinger;S. Akili
软件工程中的一个主要问题是保证分布式系统的正确性。证明分布式算法（CDA）为其输入输出对（i，o）计算附加的不确定性w-（i，o）正确性的形式参数。每个CDA都有一个见证谓词，如果见证谓词对三元组（i，o，w）成立，则输入输出对（i，o）是正确的。伴随检查器算法决定见证谓词。因此，CDA的用户不必信任CDA，而是信任其检查器算法。通常，检查器更简单，其验证是可行的。总而言之，CDA的思想是在设计时调整程序的底层算法，以便在运行时验证自己的输出。虽然序列算法的认证已经很成熟，但如何将认证应用于分布式算法仍然存在一些问题。在本文中，我们讨论了分布式证人的分布式检查，其中一个挑战是，分布式证人的所有部分必须相互一致。此外，我们提出了一种形式化实例验证的方法（即获得一个机器检查的证明，一个特定的输入输出对是正确的），并实现了该方法的定理proverCoq的框架。
A major problem in software engineering is assuring the correctness of a distributed system. Acertifying distributed algorithm(CDA) computes for its input-output pair (i,o) an additionalwitnessw– a formal argument for the correctness of (i,o). Each CDA features awitness predicatesuch that if the witness predicate holds for a triple (i,o,w), the input-output pair (i,o) is correct. An accompanyingcheckeralgorithm decides the witness predicate. Consequently, a user of a CDA does not have to trust the CDA but its checker algorithm. Usually, a checker is simpler and its verification is feasible. To sum up, the idea of a CDA is to adapt the underlying algorithm of a program at design-time such that it verifies its own output at runtime. While certifyingsequentialalgorithms are well-established, there are open questions on how to apply certification todistributed algorithms. In this paper, we discussdistributed checkingof adistributed witness; one challenge is that all parts of a distributed witness have to beconsistentwith each other. Furthermore, we present a method forformal instance verification(i.e. obtaining amachine-checkedproof that a particular input-output pair is correct), and implement the method in a framework for the theorem proverCoq.
登录
查看更多内容
证明标签方案
DOI：
--
发表时间：
2005
期刊：
ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing
影响因子：
--
作者：
Amos Korman;S. Kutten;D. Peleg
通讯作者：
D. Peleg
DOI：
10.1007/978-3-319-57288-8_27
发表时间：
2017
期刊：
影响因子：
--
作者：
K. Völlinger;S. Akili
通讯作者：
S. Akili
DOI：
10.1007/s10817-013-9289-2
发表时间：
2014
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
E. Alkassar;S. Böhme;K. Mehlhorn;C. Rizkallah
通讯作者：
C. Rizkallah
施工顺序和认证 3-连通性
影响因子：
1.1
作者：
Jens M. Schmidt
通讯作者：
Jens M. Schmidt
从算法到工作程序：关于 LEDA 中程序检查的使用
DOI：
10.1007/bfb0055759
发表时间：
1998
期刊：
Theor. Comput. Sci.
影响因子：
--
作者：
K. Mehlhorn;S. Näher
通讯作者：
S. Näher