Model checking with fairness assumptions using PAT

doi:10.1007/s11704-013-3091-5

Front. Comput. Sci.

2014, Vol. 8

Issue (1) : 1-16 https://doi.org/10.1007/s11704-013-3091-5

RESEARCH ARTICLE

Model checking with fairness assumptions using PAT

Yuanjie SI¹, Jun SUN²(

), Yang LIU³, Jin Song DONG⁴, Jun PANG⁵, Shao Jie ZHANG², Xiaohu YANG¹

1. College of Computer Science, Zhejiang University, Hangzhou 310027, China; 2. Information System Technology and Design, Singapore University of Technology and Design, Singapore 138682, Singapore; 3. School of Computer Engineering, Nanyang Technological University, Singapore 639798, Singapore; 4. School of Computing, National University of Singapore, Singapore 117417, Singapore; 5. Faculty of Science, Technology and Communication, University of Luxembourg, Luxembourg L-1359, Luxembourg

Download: PDF(606 KB)
Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks

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

Corresponding Author(s): SUN Jun

Issue Date: 01 February 2014

Cite this article:

Yuanjie SI,Jun SUN,Yang LIU, et al. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-013-3091-5
https://academic.hep.com.cn/fcs/EN/Y2014/V8/I1/1

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 doi: 10.1109/TSE.1977.229904
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 doi: 10.1007/11945529_28
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 doi: 10.1007/978-3-540-31980-1_13
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 doi: 10.1007/3-540-10843-2_22
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 doi: 10.1007/PL00008921
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 doi: 10.1007/978-3-540-78163-9_21
21	Geldenhuys J, Valmari A. More efficient on-the-fly LTL verification with Tarjan’s algorithm. Theoritical Computer Science, 2005, 345(1): 60-82 doi: 10.1016/j.tcs.2005.07.004
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 doi: 10.1007/s10703-006-4342-y
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 doi: 10.1145/1375581.1375625
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 doi: 10.1007/978-3-540-31980-1_12
27	Tarjan R. Depth-first search and linear graph algorithms. SIAMJournal on Computing, 1972, 2: 146-160 doi: 10.1137/0201010
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 doi: 10.1145/945526.945527
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 doi: 10.1007/978-3-642-02658-4_59
31	Apt K R, Francez N, Katz S. Appraising fairness in languages for distributed programming. Distributed Computing, 1988, 2(4): 226-241 doi: 10.1007/BF01872848
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 doi: 10.1007/BF02242712
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 doi: 10.1007/BF00265555
35	Kwiatkowska M Z. Event fairness and non-interleaving concurrency. Formal Aspects of Computing, 1989, 1(3): 213-228 doi: 10.1007/BF01887206
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 doi: 10.1007/BF00121128
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 doi: 10.1145/318593.318622
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 doi: 10.1016/0167-6423(87)90036-0
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 doi: 10.1023/A:1008727508722
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

[1]	Genan DAI, Xiaoyang HU, Youming GE, Zhiqing NING, Yubao LIU. Attention based simplified deep residual network for citywide crowd flows prediction[J]. Front. Comput. Sci., 2021, 15(2): 152317-.
[2]	Jingke XU, Yidan ZHAO, Ge YU. An evaluation and query algorithm for the influence of spatial location based on RkNN[J]. Front. Comput. Sci., 2021, 15(2): 152604-.
[3]	Chuan SHI, Jiayu DING, Xiaohuan CAO, Linmei HU, Bin WU, Xiaoli LI. Entity set expansion in knowledge graph: a heterogeneous information network perspective[J]. Front. Comput. Sci., 2021, 15(1): 151307-.
[4]	Zhihan JIANG, Yan LIU, Xiaoliang FAN, Cheng WANG, Jonathan LI, Longbiao CHEN. Understanding urban structures and crowd dynamics leveraging large-scale vehicle mobility data[J]. Front. Comput. Sci., 2020, 14(5): 145310-.
[5]	Fangfang LIU, Yan SHEN, Tienan ZHANG, Honghao GAO. Entity-related paths modeling for knowledge base completion[J]. Front. Comput. Sci., 2020, 14(5): 145311-.
[6]	Minxi LI, Jiali MAO, Xiaodong QI, Cheqing JIN. A framework for cloned vehicle detection[J]. Front. Comput. Sci., 2020, 14(5): 145609-.
[7]	Lydia LAZIB, Bing QIN, Yanyan ZHAO, Weinan ZHANG, Ting LIU. A syntactic path-based hybrid neural network for negation scope detection[J]. Front. Comput. Sci., 2020, 14(1): 84-94.
[8]	Yuanrui ZHANG, Frédéric MALLET, Yixiang CHEN. A verification framework for spatio-temporal consistency language with CCSL as a specification language[J]. Front. Comput. Sci., 2020, 14(1): 105-129.
[9]	Zhefan ZHONG, Xin LIN, Liang HE, Jing YANG. Answering why-not questions on KNN queries[J]. Front. Comput. Sci., 2019, 13(5): 1062-1071.
[10]	Fei WANG, Tieyun QIAN, Bin LIU, Zhiyong PENG. Patent expanded retrieval via word embedding under composite-domain perspectives[J]. Front. Comput. Sci., 2019, 13(5): 1048-1061.
[11]	Kai HU, Zhangbo DUAN, Jiye WANG, Lingchao GAO, Lihong SHANG. Template-based AADL automatic code generation[J]. Front. Comput. Sci., 2019, 13(4): 698-714.
[12]	Satoshi MIYAZAWA, Xuan SONG, Tianqi XIA, Ryosuke SHIBASAKI, Hodaka KANEDA. Integrating GPS trajectory and topics from Twitter stream for human mobility estimation[J]. Front. Comput. Sci., 2019, 13(3): 460-470.
[13]	Siyuan TANG, Bei HUA. Increasing multicast transmission rate with localized multipath in software-defined networks[J]. Front. Comput. Sci., 2019, 13(2): 413-425.
[14]	Rizwan Ahmed KHAN, Alexandre MEYER, Hubert KONIK, Saida BOUAKAZ. Saliency-based framework for facial expression recognition[J]. Front. Comput. Sci., 2019, 13(1): 183-198.
[15]	Xuepeng FAN, Xiaofei LIAO, Hai JIN. FunctionFlow: coordinating parallel tasks[J]. Front. Comput. Sci., 2019, 13(1): 73-85.

Viewed

Full text

Abstract

Cited

Shared

Discussed