Model checking with fairness assumptions using PAT

Abstract

Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Existing model checkers are deficient in verifying the systems as only limited kinds of fairness are supported with limited verification efficiency. In this work, we support model checking of distributed systems in the toolkit PAT (process analysis toolkit), with a variety of fairness constraints (e.g., process-level weak/strong fairness, event-level weak/strong fairness, strong global fairness). It performs on-the-fly verification against linear temporal properties. We show through empirical evaluation (on recent population protocols as well as benchmark systems) that PAT has advantage in model checking with fairness. Previously unknown bugs have been revealed against systems which are designed to function only with strong global fairness.

Keywords

model checking / fairness / PAT / verification tool / formal methods

References

[1] Giannakopoulou D, Magee J, Kramer J. Checking progress with action priority: is it fair? In: Proceedings of the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering. 1999, 511-527

[2] Lamport L. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 1977, 3(2): 125-143

[3] Kurshan R P. Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1995

[4] Sun J, Liu Y, Dong J S, Wang H H. Specifying and verifying eventbased fairness enhanced systems. In: Proceedings of the 10th International Conference on Formal Engineering Methods. 2008, 318-337

[5] Sun J, Liu Y, Roychoudhury A, Liu S, Dong J. Fair model checking with process counter abstraction. FM 2009: Formal Methods, 2009, 123-139

[6] Fischer M J, Jiang H. Self-stabilizing leader election in networks of finite-state anonymous agents. In: Proceedings of the 10th International Conference on Principles of Distributed Systems. 2006, 395-409

[7] Angluin D, Aspnes J, Fischer M J, Jiang H. Self-stabilizing population protocols. In: Proceedings of the 9th International Conference on Principles of Distributed Systems. 2005, 103-117

[8] Angluin D, Fischer M J, Jiang H. Stabilizing consensus in mobile networks. In: Proceedings of the 2006 International Conference on Distributed Computing in Sensor Systems. 2006, 37-50

[9] Canepa D, Potop-Butucaru M. Stabilizing Token Schemes for Population Protocols. Computing Research Repository, 2008, abs/0806.3471

[10] Rozier K Y, Vardi M Y. LTL Satisfiability Checking. In: Proceedings of the 14th International SPIN Workshop. 2007, 149-167

[11] Hammer M, Knapp A, Merz S. Truly on-the-fly LTL model checking. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 191-205

[12] Pang J, Luo Z Q, Deng Y X. On automatic verification of selfstabilizing population protocols. In: Proceedings of the 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2008, 185-192

[13] Jiang H. Distributed Systems of Simple Interacting Agents. PhD thesis, Yale University, 2007

[14] Sun J, Liu Y, Dong J S, Chen C Q. Integrating specification and programs for system modeling and verification. In: Proceedings of the third IEEE International Symposium on Theoretical Aspects of Software Engineering. 2009, 127-135

[15] Hoare C A R. Communicating Sequential Processes. International Series on Computer Science. Prentice-Hall, 1985

[16] 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

[17] Lehmann D J, Pnueli A, Stavi J. Impartiality, justice and fairness: the ethics of concurrent termination. In: Proceedings of the 8th Colloquium on Automata, Languages and Programming. 1981, 264-277

[18] Holzmann G J. The SPINModel Checker: Primer and Reference Manual. Addison Wesley, 2003

[19] Lamport L. Fairness and hyperfairness. Distributed Computing, 2000, 13(4): 239-245

[20] Pnueli A, Sa’ar Y. All you need is compassion. In: Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation. 2008, 233-247

[21] Geldenhuys J, Valmari A. More efficient on-the-fly LTL verification with Tarjan’s algorithm. Theoritical Computer Science, 2005, 345(1): 60-82

[22] Henzinger M R, Telle J A. Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In: Proceedings of the 5th Scandinavian Workshop on Algorithm Theory. 1996, 16-27

[23] Kesten Y, Pnueli A, Raviv L, Shahar E. Model checking with strong fairness. Formal Methods and System Design, 2006, 28(1): 57-84

[24] Musuvathi M, Qadeer S. Fair stateless model checking. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. 2008, 362-371

[25] Baier C, Katoen J. Principles ofModel Checking. TheMIT Press, 2008

[26] Schwoon S, Esparza J. A note on on-the-fly verification algorithms. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 174-190

[27] Tarjan R. Depth-first search and linear graph algorithms. SIAMJournal on Computing, 1972, 2: 146-160

[28] Liu Y, Pang J, Sun J, Zhao J. Verification of population ring protocols in pat. In: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2009, 81-89

[29] Alagarsamy K. Some myths about famous mutual exclusion algorithms. SIGACT News, 2003, 34(3): 94-103

[30] Sun J, Liu Y, Dong J S, Pang J. PAT: towards flexible verification under fairness. Lecture Notes in Computer Science, 2009, 5643: 709-714

[31] Apt K R, Francez N, Katz S. Appraising fairness in languages for distributed programming. Distributed Computing, 1988, 2(4): 226-241

[32] Francez N. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, 1986

[33] Attie P C, Francez N, Grumberg O. Fairness and hyperfairness inmultiparty interactions. Distributed Computing, 1993, 6(4): 245-254

[34] Queille J P, Sifakis J. Fairness and related properties in transition systems— a temporal logic to deal with fairness. Acta Informaticae, 1983, 19: 195-220

[35] Kwiatkowska M Z. Event fairness and non-interleaving concurrency. Formal Aspects of Computing, 1989, 1(3): 213-228

[36] Völzer H, Varacca D, Kindler E. Defining fairness. In: Proceedings of the 16th International Conference on Concurrency Theory. 2005, 458-472

[37] Latvala T, Heljanko K. Coping with strong fairness. Fundamenta Informaticae, 2000, 43(1-4): 175-193

[38] Courcoubetis C, Vardi M Y, Wolper P, Yannakakis M. Memoryefficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1992, 1(2/3): 275-288

[39] Zhang S, Sun J, Pang J, Liu Y, Dong J. On combining state space reductions with global fairness assumptions. FM 2011: Formal Methods, 2011, 432-447

[40] Lichtenstein O, Pnueli A. Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 1985, 97-107

[41] Emerson E A, Lei C L. Modalities for model checking: branching time logic strikes back. Science of Computer Programming, 1987, 8(3): 275-306

[42] Hardin R H, Kurshan R P, Shukla S K, Vardi M Y. A new heuristic for bad cycle detection using BDDs. Formal Methods in System Design, 2001, 18(2): 131-140

[43] Klarlund N. An n log n Algorithm for Online BDD Refinement. In: Proceedings of the 9th International Conference on Computer Aided Verification. 1997, 107-118

[44] Dong J S, Liu Y, Sun J, Zhang X. Verification of computation orchestration via timed automata. In: Proceedings of the 8th International Conference on Formal Engineering Methods. 2006, 226-245

[45] Dong J S, Hao P, Sun J, Zhang X. A reasoning method for timed CSP based on constraint solving. In: Proceedings of the 8th International Conference on Formal Engineering Methods. 2006, 342-359

[46] Sun J, Liu Y, Dong J S. Model checking csp revisited: introducing a process analysis toolkit. In: Proceedings of the 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. 2008, 307-322

RIGHTS & PERMISSIONS

Higher Education Press and Springer-Verlag Berlin Heidelberg