Weakest precondition based verification tool that models spatial ordering

ABSTRACT

Weakest precondition based method for specification and verification of geographically distributed system is described. For this purpose spatial predicates have been defined. A distributed mutual exclusion algorithm is proposed and is used to illustrate this verification tool.

REFERENCES

• 1: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 2: David Gries, The Science of Programming, Springer-Verlag New York, Inc., Secaucus, NJ, 1987
• 3: A. K. Bandyopadhyay , J. Bandyopadhyay, On the derivation of a correct deadlock free communication kernel for loop connected message passing architecture from its user's specification, Journal of Systems Architecture: the EUROMICRO Journal, v.46 n.13, p.1257-1261, Nov. 2000 [doi>10.1016/S1383-7621(00)00024-2 ]
• 4: Awadhesh Kumar Singh, Umesh Ghanekar and Anup Kumar Bandyopadhyay, Specifying Mobile Network using a wp-like Formal Approach, Colombian Journal of Computation, Vol. 6, No2, December 2005, pp 59-77.
• 5: Causality and the spatial-temporal ordering in mobile systems, Mobile Networks and Applications, v.9 n.5, p.507-516, October 2004 [doi>10.1145/1027347.1027353]
• 6: James F. Allen, Maintaining knowledge about temporal intervals, Communications of the ACM, v.26 n.11, p.832-843, Nov. 1983 [doi>10.1145/182.358434]
• 7: Jayasri Banerjee , Anup Kumar Bandyopadhyay , Ajit Kumar Mandal, Ordering of events in two-process concurrent system, ACM SIGSOFT Software Engineering Notes, v.32 n.4, July 2007 [doi>10.1145/1281421.1281423]
• 8: M. Mizuno and M. L. Neilsen, A token based distributed mutual exclusion algorithm based on quorum agreements, Proceedings of the 11th International Conference on Distributed Systems, IEEE Press, 1991, pp 361-368.
• 9: Glenn Ricart , Ashok K. Agrawala, An optimal algorithm for mutual exclusion in computer networks, Communications of the ACM, v.24 n.1, p.9-17, Jan. 1981 [doi>10.1145/358527.358537]
• 10: Beverly A. Sanders, The information structure of distributed mutual exclusion algorithms, ACM Transactions on Computer Systems (TOCS), v.5 n.3, p.284-299, Aug. 1987 [doi>10.1145/24068.28052]
• 11: Kerry Raymond, A tree-based algorithm for distributed mutual exclusion, ACM Transactions on Computer Systems (TOCS), v.7 n.1, p.61-77, Feb. 1989 [doi>10.1145/58564.59295]
• 12: Mukesh Singhal, A Heuristically-Aided Algorithm for Mutual Exclusion in Distributed Systems, IEEE Transactions on Computers, v.38 n.5, p.651-662, May 1989 [doi>10.1109/12.24268 ]
• 13: Ichiro Suzuki , Tadao Kasami, A distributed mutual exclusion algorithm, ACM Transactions on Computer Systems (TOCS), v.3 n.4, p.344-349, Nov. 1985 [doi>10.1145/6110.214406]
• 14: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 15: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 16: Anup Kumar Bandyopadhyay, Modeling fairness and starvation in concurrent systems, ACM SIGSOFT Software Engineering Notes, v.32 n.6, November 2007 [doi>10.1145/1317471.1317474]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.1 Requirements/Specifications
      D.2.5 Testing and Debugging

General Terms:
Design, Experimentation, Measurement, Performance, Verification

Keywords:
correctness, distributed systems, spatial ordering, weakest precondition