Modelling Peterson Mutual Exclusion Algorithm in DVE Language and Verifying LTL Properties

Abstract:

Peterson mutual exclusion algorithm is a concurrent programming algorithm for mutual exclusion that allows two processes to share a single-use resource without conflict, using only shared memory for communication. DiVinE is a LTL model checker, and DVE is the specification language. In this paper, we implement the DVE model of Peterson mutual exclusion algorithm, and verify LTL properties of Peterson mutual exclusion algorithms using DiVinE model checker. The experimental results show that the LTL formula structure is relevant to the costs of LTL verification.

• Periodical: Applied Mechanics and Materials (Volume 577)
• Pages: 1012-1016
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.577.1012
• Online since: July 2014
• Authors: Shi Gong Long*, Han Wen Yang
• Keywords: DVE, Linear Temporal Logic (LTL), Model Checking, Peterson’s Algorithm

References

[1] E. Clarke, O. Grumberg, and D. Peled. Model Checking. The MIT Press, Cambridge, MA, (1999).

[2] C. Baier and J. P. Katoen. Principles of model checking. The MIT Press, Cambridge, MA, (2008).

[3] E. Clarke, W. Klieber, M. Nováček, and P. Zuliani. Model Checking and the State Explosion Problem. Tools for Practical Software Verification. Lecture Notes in Computer Science Volume 7682, pages 1-30, (2012).

DOI: 10.1007/978-3-642-35746-6_1

[4] J. R. Burch, E. M. Clarke, and K. L. McMillan. Symbolic model checking: 1020 states and beyond. Information and Computation, 98: 142-170, (1992).

DOI: 10.1016/0890-5401(92)90017-a

[5] K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, (1993).

[6] C. Flanagan and P. Godefroid. Dynamic partial-order reduction for model checking software. In POPL, pages 110-121. ACM, (2005).

DOI: 10.1145/1047659.1040315

[7] P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An approach to the State-Explosion Problem. Phd thesis, Universite De Liege, 1994-95.

[8] Y. Yang, X. Chen, G. Gopalakrishnan, and R. M. Kirby. Efficient stateful dynamic partial order reduction. In SPIN, Lecture Notes in Computer Science, pages 288-305. Springer, (2008).

DOI: 10.1007/978-3-540-85114-1_20

[9] A. F. Donaldson and A. Miller. Symmetry reduction for probabilistic model checking using generic representatives. In Proceedings ATVA'06, vol 4218 of Lecture Notes in Computer Science, pages 9-23, (2006).

DOI: 10.1007/11901914_4

[10] A. Miller, A. Donaldson, and M. Calder. Symmetry in temporal logic model checking. Computing Surveys, (2006).

DOI: 10.1145/1132960.1132962

[11] A. N. Nepeivoda. Verification of a technical system model with linear temporal logic. Automation and Remote Control Vol 73, pages 1539-1552, (2012).

DOI: 10.1134/s0005117912090081

[12] M. Sulzmann and A. Zechner. Constructive Finite Trace Analysis with Linear Temporal Logic. Lecture Notes in Computer Science Volume 7305, pages 132-148, (2012).

DOI: 10.1007/978-3-642-30473-6_11

[13] P. Schnoebelen. The complexity of temporal logic model checking. Advances in Modal Logic Volume 4, (2003).

[14] F. Ranzato. A More Effient Simulation Algorithm on Kripke Structures. Lecture Noes in Computer Science Volume 8087, pages 753-764, (2013).

DOI: 10.1007/978-3-642-40313-2_66

[15] J. Barnat, J. Havlíček, amd P. Ročkai. Distributed LTL Model Checking with Hash Compaction. In To appear in proceedings of PASM/PDMC 2012., (2013).

DOI: 10.1016/j.entcs.2013.07.006