research-article

Modeling of state transition rules and its application

Author:

Anup Kumar BandyopadhyayAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 35, Issue 2

Pages 1 - 7

https://doi.org/10.1145/1734103.1734109

Published: 27 March 2010 Publication History

Get Access

Abstract

A state transition rule is viewed as a cause and effect relationship. An example is selected from the common sense world. Six different instances of this relationship are enumerated. A temporal logic based on observation is proposed. This logic is used to model the enumerated instances. Assuming some necessary properties of a transition rule only two relevant models are selected. One of them ensures that the precondition is necessary where the other guarantees its sufficiency. Noting these two characteristics the first one is opted for proving the safety property where the second is used to prove progress. We have considered Peterson's two process mutual exclusion algorithm as an illustrative example

References

[1]

Lamport Leslie (1993): Verification and Specifications of Concurrent Programs, Lecture Notes In Computer Science; Vol. 803, pp 347--374.

Digital Library

Google Scholar

[2]

Lamport Leslie (1983): Specifying concurrent program modules. ACM Transactionson Programming Languages and Systems, 5(2):190--222.

Digital Library

Google Scholar

[3]

Owicki S.S., L. Lamport (1982): Proving liveness properties of concurrent programs, ACM-TOPLAS, vol. 4, No. pp 455--495.

Digital Library

Google Scholar

[4]

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

Digital Library

Google Scholar

[5]

Ben-Ari M (1993): Mathematical Logic For Computer Science, Prentice Hall International (UK) Ltd.

Digital Library

Google Scholar

[6]

Bandyopadhyay Anup Kumar (2007): Modeling Fairness and Starvation in Concurrent Systems, ACM SIGSOFT Software Engineering Notes, Volume 32 Number 6, November 2007.

Digital Library

Google Scholar

[7]

Peterson Gary L. (1981): Myths about the mutual exclusion problem, Information Processing Letters, vol. 12, No. 3, 115--116.

Crossref

Google Scholar

[8]

Hoare C.A.R. (1969): An axiomatic basis for computer programming, Commun. ACM, 12(10), Oct 1969, pp. 576--583.

Digital Library

Google Scholar

[9]

Owicki S., D. Gries (1976): An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319--340.

Digital Library

Google Scholar

[10]

Dijkstra E.W.(1976): A discipline of programming, Englewood Cliffs, NJ: Prentice***Hall, 1976.

Digital Library

Google Scholar

[11]

Chandi K. Mani, Beverly A. Sanders (1995): Predicate transformers for reasoning about concurrent computation, ELSEVIER Science of Computer Programming, vol. 24, pp 129--148.

Digital Library

Google Scholar

[12]

Schneider F.B. (1997): On Concurrent Programming, Springer Verlag, N. Y., Inc. 1997.

Digital Library

Google Scholar

[13]

Anup Kumar Bandyopadhyay : Weakest Precondition Based Modeling and Verification of a Class of Concurrent Systems, to be published in International Journal of Artificial Intelligence and Soft Computing.

Digital Library

Google Scholar

Cited By

View all

Banerjee ABandyopadhyay A(2017)Safe registers can achieve correct implementation of peterson’s two process mutual exclusion algorithmCSI Transactions on ICT10.1007/s40012-017-0164-x5:3(259-264)Online publication date: 7-Mar-2017
https://doi.org/10.1007/s40012-017-0164-x
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(2011)TLRO based modeling of alternative commands and its application to generalized distributed resource allocation problemACM SIGSOFT Software Engineering Notes10.1145/2047414.204742136:6(1-5)Online publication date: 14-Nov-2011
https://dl.acm.org/doi/10.1145/2047414.2047421
Show More Cited By

Recommendations

Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems
Automated Technology for Verification and Analysis
Abstract
To overcome the complexity of verification of real-time systems with dense time dynamics, Dutertre and Sorea proposed timeout and calender based transition systems to model real-time systems and verify safety properties using k-induction. In this ...
Formalization and Verification of Safety Properties of Statechart Specifications
APSEC '96: Proceedings of the Third Asia-Pacific Software Engineering Conference

There have been many analysis methods proposed for the verification of safety properties of real-time systems. Most of these methods, however, are not powerful enough for complex and safety-critical real-time systems due mainly to the lack of language ...
Verification of parameterized hierarchical state machines using action language verifier
MEMOCODE '05: Proceedings of the 2nd ACM/IEEE International Conference on Formal Methods and Models for Co-Design

Action language verifier (ALV) is an infinite-state symbolic model checker. ALV can verify (or falsify, by generating counter-examples) temporal logic properties of systems that can be modeled using a combination of Boolean logic and linear arithmetic ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 35, Issue 2

March 2010

113 pages

ISSN:0163-5948

DOI:10.1145/1734103

Issue’s Table of Contents

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 March 2010

Published in SIGSOFT Volume 35, Issue 2

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
137
Total Downloads

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

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Banerjee ABandyopadhyay A(2017)Safe registers can achieve correct implementation of peterson’s two process mutual exclusion algorithmCSI Transactions on ICT10.1007/s40012-017-0164-x5:3(259-264)Online publication date: 7-Mar-2017
https://doi.org/10.1007/s40012-017-0164-x
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(2011)TLRO based modeling of alternative commands and its application to generalized distributed resource allocation problemACM SIGSOFT Software Engineering Notes10.1145/2047414.204742136:6(1-5)Online publication date: 14-Nov-2011
https://dl.acm.org/doi/10.1145/2047414.2047421
Bandyopadhyay ALenka N(2010)Application of TLRO to dining philosophers problemACM SIGSOFT Software Engineering Notes10.1145/1874391.187439735:6(1-6)Online publication date: 27-Nov-2010
https://dl.acm.org/doi/10.1145/1874391.1874397

View Options

Login options

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

Cited By

Recommendations

Timeout and Calendar Based Finite State Modeling and Verification of Real-Time Systems

Formalization and Verification of Safety Properties of Statechart Specifications

Verification of parameterized hierarchical state machines using action language verifier