Verification of Faulty Message Passing Systems with Continuous State Space in PVS
Concetta Pilotto, Jerome White · NASA STI Repository (National Aeronautics and Space Administration) · 2010
We present a library of Prototype Verification System (PVS) meta-theories that verifies a class of distributed systems in which agent commu nication is through message-passing. The theoretic work, outlined in, consists of iterative schemes for solving systems of linear equations , such as message-passing extensions of the Gauss and Gauss-Seidel me thods. We briefly review that work and discuss the challenges in formally verifying it.