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

    VL - 23

    SP - 649

    EP - 679

    JO - Formal Aspects of Computing

    JF - Formal Aspects of Computing

    SN - 0934-5043

    IS - 5

    ER -