|
|||||
|
|
A computer checked algebraic verification of a distributed summation algorithm |
|
| Authors: | Jan Friso Groote François Monin Jan Springintveld |
| Affiliation: | (1) Division of Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands;(2) CWI, Amsterdam, The Netherlands;(3) Department of Computer Science, University of Western Brittany, Brest, France;(4) CMG Trade, Transport & Industry, Rotterdam, The Netherlands;(5) Department of Mathematics and Computer Science, Eindhoven University of Technology, Box 513, 5600, MB, Eindhoven, The Netherlands |
| Abstract: | We present an algebraic verification of Segall s propagation of information with feedback algorithm and we report on the verification of the proof using the PVS system. This algorithm serves as a nice benchmark for verification exercises (see [2, 8, 17]). The verification is based on the methodology presented in [7] and demonstrates its suitability to deliver mechanically verifiable correctness proofs of highly nondeterministic distributed algorithms.The research of the second author was supported by Human Capital Mobility (HCM). The research of the third author was supported by the Netherlands Organization for Scientific Research (NWO) under contract SION 612-33-006.Received October 1988 by J. RushbyRevised July 2004Accepted September 2004 by C. B. Jones |
| Keywords: | Distributed summation algorithm Verification Formal proof checking Process algebra  CRL PVS |
| 本文献已被 SpringerLink 等数据库收录！ | |