Towards a verification framework for faulty message passing systems in PVS

Concetta Pilotto; Jerome White

doi:10.1007/s11334-011-0150-7

Towards a verification framework for faulty message passing systems in PVS

Concetta Pilotto, Jerome White

Computer Science

Research output: Contribution to journal › Review article › peer-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 language	English (US)
Pages (from-to)	109-118
Number of pages	10
Journal	Innovations in Systems and Software Engineering
Volume	7
Issue number	2
DOIs	https://doi.org/10.1007/s11334-011-0150-7
State	Published - Jun 2011

Keywords

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

ASJC Scopus subject areas

Software

Access to Document

10.1007/s11334-011-0150-7

Cite this

@article{2a3a93d168c4421ea5f0ab2e4f37c585,

title = "Towards a verification framework for faulty message passing systems in PVS",

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.",

keywords = "Message passing systems, Methods for solving systems of linear equations, PVS theorem-prover",

author = "Concetta Pilotto and Jerome White",

note = "Funding Information: Acknowledgments The authors would like to thank the referees for their helpful and constructive comments. This work was supported in part by the Multidisciplinary Research Initiative (MURI) from the Air Force Office of Scientific Research.",

year = "2011",

month = jun,

doi = "10.1007/s11334-011-0150-7",

language = "English (US)",

volume = "7",

pages = "109--118",

journal = "Innovations in Systems and Software Engineering",

issn = "1614-5046",

publisher = "Springer London",

number = "2",

}

TY - JOUR

T1 - Towards a verification framework for faulty message passing systems in PVS

AU - Pilotto, Concetta

AU - White, Jerome

N1 - Funding Information: Acknowledgments The authors would like to thank the referees for their helpful and constructive comments. This work was supported in part by the Multidisciplinary Research Initiative (MURI) from the Air Force Office of Scientific Research.

PY - 2011/6

Y1 - 2011/6

N2 - 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.

AB - 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.

KW - Message passing systems

KW - Methods for solving systems of linear equations

KW - PVS theorem-prover

UR - http://www.scopus.com/inward/record.url?scp=79957950543&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79957950543&partnerID=8YFLogxK

U2 - 10.1007/s11334-011-0150-7

DO - 10.1007/s11334-011-0150-7

M3 - Review article

AN - SCOPUS:79957950543

SN - 1614-5046

VL - 7

SP - 109

EP - 118

JO - Innovations in Systems and Software Engineering

JF - Innovations in Systems and Software Engineering

IS - 2

ER -

Towards a verification framework for faulty message passing systems in PVS

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this