article

Weakest precondition based modelling and verification of a class of concurrent systems

Author:

Anup Kumar BandyopadhyayAuthors Info & Claims

International Journal of Artificial Intelligence and Soft Computing, Volume 2, Issue 1/2

Pages 115 - 131

https://doi.org/10.1504/IJAISC.2010.032516

Published: 01 April 2010 Publication History

Abstract

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 include both if-then-else and terminating while-do type control structures. The properties of the system are verified by proving the invariance of logical formulae. The technique is illustrated by considering Dekker's two process mutual exclusion algorithm as an example.

References

[1]

Allen, J.F. (1983) 'Maintaining knowledge about temporal intervals', CACM, Vol. 26, pp. 832-843.

Digital Library

[2]

Bandyopadhyay, A.K. (2007) 'Modeling fairness and starvation in concurrent systems', ACM SIGSOFT Software Engineering Notes, Vol. 32, No. 6, November, pp. 1-6.

Digital Library

[3]

Bandyopadhyay, A.K. and Bandyopadhyay, J. (2000) 'On the derivation of a correct deadlock free communication kernel for loop connected message passing architecture from its user's specification', Elsevier Journal of System Architecture, Vol. 46, No. 13, pp. 1257-1261.

Digital Library

[4]

Banerjee, J., Bandyopadhyay, A.K. and Mandal, A.K. (2007a) 'On the correctness issues in two - process mutual exclusion algorithms', ACM SIGSOFT Software Engineering Notes, Vol. 32, No. 6, November, pp. 1-6.

Digital Library

[5]

Banerjee, J., Bandyopadhyay, A.K. and Mandal, A.K. (2007b) 'Ordering of events in two-process concurrent system', ACM SIGSOFT Software Engineering Notes, Vol. 32, No. 4, July, pp. 1-7.

Digital Library

[6]

Ben-Ari, M. (1993) Mathematical Logic for Computer Science, Prentice-Hall, Inc., Upper Saddle River, NJ.

[7]

Chandi, K.M. and Sanders, B.A. (1995) 'Predicate transformers for reasoning about concurrent computation',Elsevier Science of Computer Programming, Vol. 24, pp. 129-148.

[8]

Dijkstra, E.W. (1968) 'Cooperating sequential processes', in Genuys, F. (Ed.): Programming Languages, Academic Press, pp. 43-112.

[9]

Dijkstra, E.W. (1976) A Discipline of Programming, Englewood Cliffs, Prentice-Hall, NJ.

[10]

Gries, D. (1981) The Science of Programming, Springer-Verlag.

[11]

Hoare, C.A.R. (1969) 'An axiomatic basis for computer programming', Commun. ACM, Vol. 12, No. 10, October, pp. 576-583.

Digital Library

[12]

Hoare, C.A.R. and Writh, N. (1973) 'An axiomatic definition of the programming language', Pascal, Acta Informatica, Vol. 2, pp. 335-355.

Digital Library

[13]

Lamport, L. (1990) 'Win and sin: predicate transformers for concurrency', ACM Transactions on Programming Languages and Systems, Vol. 12, No. 3, pp. 396-428.

Digital Library

[14]

Manna, Z. and Pnueli, A. (1990) 'A temporal proof methodology for reactive systems', Proceedings of the Jerusalem Conference on Information Technology, pp. 757-773.

Digital Library

[15]

Owicki, S.S. and Lamport, L. (1982) 'Proving liveness properties of concurrent programs', ACM-TOPLAS, Vol. 4, No. 3, pp. 455-495.

Digital Library

[16]

Singh, A.K. and Bandyopadhyay, A.K. (2004a) 'Adding the leads-to operator to Dijkstra's calculus', ACM SIGPLAN Notices, Vol. 39, No. 2, February, pp. 12-17.

Digital Library

[17]

Singh, A.K. and Bandyopadhyay, A.K. (2004b) 'Reasoning about protocols using Dijkstra's calculus', JCS&T, Vol. 4, No. 1, April, pp. 26-31.

[18]

Singh, A.K. and Bandyopadhyay, A.K. (2004c) 'Verifying mutual exclusion and liveness properties with split preconditions', Journal of Computer Science and Technology, Springer-Verlag, New York Inc., Vol. 19, No. 6, November, pp. 795-802.

Digital Library

Cited By

Bandyopadhyay A(2012)Application of TLRO to refute an incorrect mutual exclusion algorithmACM SIGSOFT Software Engineering Notes10.1145/2347696.234770237:5(1-5)Online publication date: 2-Sep-2012
https://dl.acm.org/doi/10.1145/2347696.2347702
Bandyopadhyay A(2010)Modeling of state transition rules and its applicationACM SIGSOFT Software Engineering Notes10.1145/1734103.173410935:2(1-7)Online publication date: 27-Mar-2010
https://dl.acm.org/doi/10.1145/1734103.1734109

Weakest precondition based modelling and verification of a class of concurrent systems
1. Theory of computation
  1. Models of computation

Recommendations

Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Weakest precondition based verification tool that models spatial ordering

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 ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image International Journal of Artificial Intelligence and Soft Computing

International Journal of Artificial Intelligence and Soft Computing Volume 2, Issue 1/2

April 2010

161 pages

ISSN:1755-4950

EISSN:1755-4969

Issue’s Table of Contents

Publisher

Inderscience Publishers

Geneva 15, Switzerland

Publication History

Published: 01 April 2010

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bandyopadhyay A(2012)Application of TLRO to refute an incorrect mutual exclusion algorithmACM SIGSOFT Software Engineering Notes10.1145/2347696.234770237:5(1-5)Online publication date: 2-Sep-2012
https://dl.acm.org/doi/10.1145/2347696.2347702
Bandyopadhyay A(2010)Modeling of state transition rules and its applicationACM SIGSOFT Software Engineering Notes10.1145/1734103.173410935:2(1-7)Online publication date: 27-Mar-2010
https://dl.acm.org/doi/10.1145/1734103.1734109

View Options

View options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents