Chandy, K. Mani and Go, Brian and Mitra, Sayan and Pilotto, Concetta and White, Jerome (2011) Verification of distributed systems with local–global predicates. Formal Aspects of Computing, 23 (5). pp. 649-679. ISSN 0934-5043 http://resolver.caltech.edu/CaltechAUTHORS:20110929-135751977
Full text not available from this repository.
Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechAUTHORS:20110929-135751977
This paper describes a methodology for developing and verifying a class of distributed systems inwhich 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.
|Additional Information:||© 2010 BCS. Received 28 February 2009. Revised 1 October 2009. Accepted 8 March 2010 by T. Margaria, D. Kröning, and J. Woodcock. Published online 9 April 2010. The authors would like to thank the referees for their very helpful and constructive comments. This work was supported in part by the Multidisciplinary Research Initiative (MURI) from the Air Force Office of Scientific Research.|
|Subject Keywords:||Concurrency Convergence Local–global Stability Theorem prover Verification|
|Official Citation:||Verification of distributed systems with local–global predicates K. Mani Chandy, Brian Go, Sayan Mitra, Concetta Pilotto and Jerome White|
|Usage Policy:||No commercial reproduction, distribution, display or performance rights in this work are provided.|
|Deposited By:||Ruth Sustaita|
|Deposited On:||30 Sep 2011 15:54|
|Last Modified:||30 Sep 2011 15:54|
Repository Staff Only: item control page