Verification of distributed systems with local–global predicates
Formal Aspects of Computing2010Vol. 23(5), pp. 649–679
Citations Over TimeTop 10% of 2010 papers
Abstract
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.
Related Papers
- → “So my program doesn’t run!” Definition, origins, and practical expressions of students’ (mis)conceptions of correctness(2008)28 cited
- → A Fault-Localization Approach Based on the Coincidental Correctness Probability(2015)6 cited
- → Program Repair by Stepwise Correctness Enhancement(2016)3 cited
- → Correctness and Bounded Correctness [Keynote Address](2019)
- → Relative Correctness of Real-Time Systems(1992)