Verification of distributed systems with local-global predicates

K. Mani Chandy, Brian Go, Sayan Mitra, Concetta Pilotto, Jerome White

Research output: Contribution to journalArticle

Abstract

This paper describes a methodology for developing and verifying a class of distributed systems in which the state space may be discrete or continuous. Our focus is on systems where changes are local in that a small number of components change state while the remainder of the system is unchanged. A proof methodology is developed that ensures global properties, such as invariants and convergence, by guaranteeing local properties within subsystems. This methodology is used to prove the correctness of concrete examples. We present a PVS library of theorems and proofs that can be used to reduce the work required to develop and verify programs in this class. A transformation of these libraries to Java is also outlined.

Original languageEnglish (US)
Pages (from-to)649-679
Number of pages31
JournalFormal Aspects of Computing
Volume23
Issue number5
DOIs
StatePublished - Sep 1 2011

Fingerprint

Predicate
Distributed Systems
Methodology
Local Properties
Number of Components
Remainder
Java
Correctness
Subsystem
State Space
Verify
Invariant
Theorem
Class
Libraries

Keywords

  • Concurrency
  • Convergence
  • Local-global
  • Stability
  • Theorem prover
  • Verification

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science

Cite this

Verification of distributed systems with local-global predicates. / Chandy, K. Mani; Go, Brian; Mitra, Sayan; Pilotto, Concetta; White, Jerome.

In: Formal Aspects of Computing, Vol. 23, No. 5, 01.09.2011, p. 649-679.

Research output: Contribution to journalArticle

Chandy, KM, Go, B, Mitra, S, Pilotto, C & White, J 2011, 'Verification of distributed systems with local-global predicates', Formal Aspects of Computing, vol. 23, no. 5, pp. 649-679. https://doi.org/10.1007/s00165-010-0150-7
Chandy, K. Mani ; Go, Brian ; Mitra, Sayan ; Pilotto, Concetta ; White, Jerome. / Verification of distributed systems with local-global predicates. In: Formal Aspects of Computing. 2011 ; Vol. 23, No. 5. pp. 649-679.
@article{0b5d01c6a67642eea1fc82875242bbbf,
title = "Verification of distributed systems with local-global predicates",
abstract = "This paper describes a methodology for developing and verifying a class of distributed systems in which the state space may be discrete or continuous. Our focus is on systems where changes are local in that a small number of components change state while the remainder of the system is unchanged. A proof methodology is developed that ensures global properties, such as invariants and convergence, by guaranteeing local properties within subsystems. This methodology is used to prove the correctness of concrete examples. We present a PVS library of theorems and proofs that can be used to reduce the work required to develop and verify programs in this class. A transformation of these libraries to Java is also outlined.",
keywords = "Concurrency, Convergence, Local-global, Stability, Theorem prover, Verification",
author = "Chandy, {K. Mani} and Brian Go and Sayan Mitra and Concetta Pilotto and Jerome White",
year = "2011",
month = "9",
day = "1",
doi = "10.1007/s00165-010-0150-7",
language = "English (US)",
volume = "23",
pages = "649--679",
journal = "Formal Aspects of Computing",
issn = "0934-5043",
publisher = "Springer London",
number = "5",

}

TY - JOUR

T1 - Verification of distributed systems with local-global predicates

AU - Chandy, K. Mani

AU - Go, Brian

AU - Mitra, Sayan

AU - Pilotto, Concetta

AU - White, Jerome

PY - 2011/9/1

Y1 - 2011/9/1

N2 - This paper describes a methodology for developing and verifying a class of distributed systems in which the state space may be discrete or continuous. Our focus is on systems where changes are local in that a small number of components change state while the remainder of the system is unchanged. A proof methodology is developed that ensures global properties, such as invariants and convergence, by guaranteeing local properties within subsystems. This methodology is used to prove the correctness of concrete examples. We present a PVS library of theorems and proofs that can be used to reduce the work required to develop and verify programs in this class. A transformation of these libraries to Java is also outlined.

AB - This paper describes a methodology for developing and verifying a class of distributed systems in which the state space may be discrete or continuous. Our focus is on systems where changes are local in that a small number of components change state while the remainder of the system is unchanged. A proof methodology is developed that ensures global properties, such as invariants and convergence, by guaranteeing local properties within subsystems. This methodology is used to prove the correctness of concrete examples. We present a PVS library of theorems and proofs that can be used to reduce the work required to develop and verify programs in this class. A transformation of these libraries to Java is also outlined.

KW - Concurrency

KW - Convergence

KW - Local-global

KW - Stability

KW - Theorem prover

KW - Verification

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

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

U2 - 10.1007/s00165-010-0150-7

DO - 10.1007/s00165-010-0150-7

M3 - Article

AN - SCOPUS:79957955197

VL - 23

SP - 649

EP - 679

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

IS - 5

ER -