A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions

Abstract

This paper proposes an approach to making liveness model checking problems under fairness feasible. The proposed method divides such a problem into smaller ones that can be conquered. It is not superior to existing tools dedicated to model checking liveness properties under fairness assumptions in terms of model checking performance but has the following positive aspects: 1) the approach can be used to model check liveness properties under anti-fairness assumptions as well as fairness assumptions, 2) the approach can help humans better understand the reason why they need to use fairness and/or anti-fairness assumptions, and 3) the approach makes it possible to use existing linear temporal logic model checkers to model check liveness properties under fairness and/or anti-fairness assumptions.

Keywords

anti-fairness / fairness / liveness property / Maude / model checking

References

[1] Ogata K, Zhang M. A divide & conquer approach to model checking of liveness properties. In: Proceedings of the 37th Annual IEEE Computer Software and Applications Conference. 2013, 648–657

[2] Ogata K. Model checking liveness properties under fairness & antifairness assumptions. In: Proceedings of the 20th Asia-Pacific Software Engineering Conference. 2013, 565–570

[3] Manna Z, Pnueli A. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Science & Business Media, 1992, 16

[4] Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., 2002

[5] Clarke E M, Grumberg O, Peled D A. Model Checking. Massachusetts: MIT Press, 1999

[6] Latvala T. Model checking LTL properties of high-level Petri nets with fairness constraints. In: Proceedings of the 22nd International Conference on Application and Theory of Petri Nets. 2001, 242–262

[7] Sun J, Liu Y, Dong J S, Pang J. PAT: towards flexible verification under fairness. In: Proceedings of the 21st International Conference on Computer Aided Verification. 2009, 709–714

[8] Si Y, Sun J, Liu Y, Dong J S, Pang J, Zhang S J, Yang X. Model checking with fairness assumptions using PAT. Frontiers of Computer Science, 2014, 8(1): 1–16

[9] Bae K, Meseguer J. State/event-based LTLmodel checking under parametric generalized fairness. In: Proceedings of the 23rd International Conference on Computer Aided Verification. 2011, 132–148

[10] Bae K, Meseguer J. Model checking LTLR formulas under localized fairness. In: Proceedings of the 9th International Workshop on Rewriting Logic and its Applications. 2012, 99–117

[11] Bae K, Meseguer J. Model checking linear temporal logic of rewriting formulas under localized fairness. Science of Computer Programming, 2015, 99: 193–234

[12] Holzmann G J. The SPINModel Checker – Primer and Reference Manual. Reading: Addison-Wesley, 2004

[13] De Moura L, Owre S, Rueß H, Rushby J, Shankar N, Sorea M, Tiwari A. SAL 2. In: Proceedings of the 16th International Conference on Computer Aided Verification. 2004, 496–500

[14] Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott C. All About Maude – A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, 2007

[15] Suzuki I, Kasami T. A distributed mutual exclusion algorithm. ACM Transactions on Computer Systems, 1985, 3(4): 344–349

[16] Ogata K, Futatsugi K. Formal analysis of Suzuki&Kasami distributed mutual exclusion algorithm. In: Proceedings of the 5th International Conference on Formal Methods for Open Object-Based Distributed Systems. 2002, 181–195

[17] Ogata K, Futatsugi K. Comparison of Maude and SAL by conducting case studies model checking a distributed algorithm. IEICE Transactions on Fundamentals of Electronics, Communications and Comptuter Sciences, 2007, 90(8): 1690–1703

[18] Futatsugi K, Goguen J A, Ogata K. Verifying design with proof scores. In: Proceedings of the 1st IFIP TC 2/WG 2.3 Conference on Verified Software: Theories, Tools, Experiments. 2008, 277–290

[19] Meseguer J. Localized fairness: a rewriting semantics. In: Proceedings of the 16th International Conference on Term Rewriting and Applications. 2005, 250–263

[20] Chaki S, Clarke E M, Ouaknine J, Sharygina N, Sinha N. State/eventbased software model checking. In: Proceedings of the 4th International Conference on Integrated Formal Methods. 2004, 128–147

[21] McMillan K L. Applications of Craig interpolants in model checking. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 1–12

[22] Maksimova L L. Temporal logics with “the next” operator do not have interpolation or the Beth property. Siberian Mathematical Journal, 1991, 32(6): 989–993

[23] Gheerbrant A, Ten Cate B. Craig interpolation for linear temporal languages. In: Proceedings of the 23rd International Workshop on Computer Science Logic. 2009, 287–301

[24] Clarke E M, Long D E, McMillan K L. Compositional model checking. In: Proceedings of the 4th Symposium on Logic in Computer Science. 1989, 353–362

[25] Kurshan R P, Lamport L. Verification of a multiplier: 64 bits and beyond. In: Proceedings of the 5th International Conference on Computer Aided Verification. 1993, 166–179

[26] Abadi M, Lamport L. Open systems in TLA. In: Proceedings of the 13th ACM Symposium on Principles of Distributed Computing. 1994, 81–90

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag GmbH Germany, part of Springer Nature