Cited By
View all- Bandyopadhyay A(2010)Spatial ordering of messages in a cyclic architectureACM SIGSOFT Software Engineering Notes10.1145/1874391.187439835:6(1-6)Online publication date: 27-Nov-2010
Weakest precondition based verification tool that models spatial ordering
Article No.: 2, Pages 1 - 5
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]
E. W. Dijkstra, A discipline of programming, Englewood Cliffs, NJ: Prentice-Hall, 1976.
[2]
David Gries, The Science of Programming, Springer-Verlag, 1981.
[3]
A. K. Bandyopadhyay and J. Bandyopadhyay, On the derivation of a correct deadlock free communication kernel for loop connected message passing architecture from its user's specification, ELSVIER Journal of System Architecture, 46(13), 2000, pp. 1257-1261.
[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]
Ravi Prakash and Roberto Baldoni, Causality and the Spatial-Temporal Ordering in Mobile Systems, Mobile Networks and Applications 9, 507--516, 2004.
[6]
James F. Allen, Maintaining knowledge about temporal intervals, CACM, 1983 Vol. 26, pp 832-843.
[7]
Jayasri Banerjee, Anup Kumar Bandyopadhyay and Ajit Kumar Mandal, Ordering of Events in Two-Process Concurrent System, ACM SIGSOFT Software Engineering Notes, Vol. 32, No. 4, July 2007
[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]
G. Ricart and A. K. Agrawala, An optimal algorithm for mutual exclusion in computer networks, Communications of the ACM, vol. 24, Jan 1981, pp 9-17.
[10]
B. A. Sanders, The information structure of distributed mutual exclusion algorithms, ACM Transactions on Computer Systems, vol. 5, No 3, August 1987, pp 284-289.
[11]
K. Raymond, A tree-based algorithm for distributed mutual exclusion, ACM transaction on Computer Systems, vol. 7 No. 1, Feb. 1989, pp 61-67.
[12]
M. Singhai, A heuristically-aided algorithm for mutual exclusion in distributed systems, IEEE Transactions on Computers, vol. 38, No. 5, May 1989, pp 651-662.
[13]
I. Suzuki and T. Kasami, A distributed mutual exclusion algorithm, ACM Transactions on Computer Systems, vol. 3, No. 4, Nov. 1985, pp 344-349.
[14]
E.W. Dijkstra, Guarded commands, nondeterminancy and formal derivation of programs. Commun. ACM 18, 8 (Aug. 1975), 453-457.
[15]
S. S. Owicki, L. Lamport, Proving liveness properties of concurrent programs, ACM-TOPLAS, vol. 4, No. pp 455-495, 1982.
[16]
Anup Kumar Bandyopadhyay, Modeling Fairness and Starvation in Concurrent Systems, ACM SIGSOFT Software Engineering Notes, Volume 32 Number 6, November 2007
Index Terms
- Weakest precondition based verification tool that models spatial ordering
Recommendations
Weakest precondition based modelling and verification of a class of concurrent systems
A weakest precondition based modelling and verification technique for a class of concurrent systems is proposed. A system in this class is defined by a set of non-terminating interactive sequential processes. The constituent processes are allowed to ...
Some investigations on deadlock freedom issues of a cyclically connected system using Dijkstra's weakest precondition calculus
Weakest precondition calculus is used to specify a system implemented by a cyclic interconnection of sequential processes. From this specification a predicate is derived that describes the deadlock freedom property of the system. Invariance of the ...
Ivy: safety verification by interactive generalization
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and ImplementationDespite several decades of research, the problem of formal verification of infinite-state systems has resisted effective automation. We describe a system --- Ivy --- for interactively verifying safety of infinite-state systems. Ivy's key principle is ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © 2008 Author.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 March 2008
Published in SIGSOFT Volume 33, Issue 2
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 134Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 11 Jan 2025
Other Metrics
Citations
Cited By
View all- Bandyopadhyay A(2010)Spatial ordering of messages in a cyclic architectureACM SIGSOFT Software Engineering Notes10.1145/1874391.187439835:6(1-6)Online publication date: 27-Nov-2010
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in