Towards a verification framework for faulty message passing systems in PVS

Concetta Pilotto, Jerome White

Research output: Contribution to journalReview articlepeer-review

Abstract

We present a library of PVS meta-theories that can be used to verify a class of distributed systems in which agent communication is via message-passing. The theoretical work, as outlined in Chandy et al. (Form Aspect Comput 2011, to appear) consists of iterative schemes for solving systems of linear equations, such as message-passing extensions of the Gauss and Gauss-Seidel methods. We briefly review that work and discuss the challenges in formally verifying it.

Original languageEnglish (US)
Pages (from-to)109-118
Number of pages10
JournalInnovations in Systems and Software Engineering
Volume7
Issue number2
DOIs
StatePublished - Jun 2011

Keywords

  • Message passing systems
  • Methods for solving systems of linear equations
  • PVS theorem-prover

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Towards a verification framework for faulty message passing systems in PVS'. Together they form a unique fingerprint.

Cite this