Please wait a minute...
1. 浙江大学 计算机科学与技术学院,浙江 杭州 310027; 2. 新加坡国立大学 软件工程实验室,新加坡
Analytical study on model checking with fairness assumptions
SI Yuan-jie1, GUI Lin2, YANG Xiao-hu1
1.College of Computer Science and Technology, Zhejiang University, Hangzhou 310027, China;2. School of Computing, National University of Singapore, Singapore
 全文: PDF(1037 KB)   HTML

研究模型验证中的公平性问题,全面定义了包括进程层面(process-level)的强/弱公平、事件层面(event-level)的强/弱公平以及全局强公平性(strong global fairness)等,把这些公平性条件集成进了一个模型验证工具PAT.该工具支持以on-the-fly的方式对线性时序逻辑性质进行验证.通过对多个基准模型进行实验,该工具在基于公平条件的模型验证中表现出良好的性能.


A variety of fairness constraints were proposed, including process-level strong/weak fairness, event-level strong/weak fairness, strong global fairness, etc. The constraints were integrated into a model checker PAT. The model checker performs on-the-fly verification against linear temporal properties. Empirical evaluation on various benchmark systems shows that PAT has advantage in model checking with fairness.

出版日期: 2014-08-04
:  TP 301.2  
通讯作者: 杨小虎,男,研究员     E-mail:
作者简介: 斯袁杰(1984-),男,博士生,从事模型验证和软件工程的研究.E-mail:
E-mail Alert


斯袁杰,桂林,杨小虎. 模型验证中的公平性问题[J]. 浙江大学学报(工学版), 10.3785/j.issn.1008-973X.2014.07.011.

SI Yuan-jie, GUI Lin, YANG Xiao-hu. Analytical study on model checking with fairness assumptions. JOURNAL OF ZHEJIANG UNIVERSITY (ENGINEERING SCIENCE), 10.3785/j.issn.1008-973X.2014.07.011.


1] GIANNAKOPOULOU D, MAGEE J, KRAMER J. Checking progress with action priority: is it fair [J].ACM SIGSOFT Software Engineering Notes, 1999, 24(6): 511-527.
[2] SUN Jun, LIU Yang, ROYCHOUDHURY A, et al. Fair model checking with process counter abstraction [C]∥ Proceedings of Formal Methods. Eindhoven: Springer, 2009: 123-139.
[3] FISCHER M J, JIANG H. Self-stabilizing leader election in networks of finite-state anonymous agents [C]∥ Proceedings of the 10th International Conference on Principles of Distributed Systems. Bordeaux: Springer, 2006: 395-409.
[4] ANGLUIN D, ASPNES J, FISCHER M J, et al. Self-stabilizing population protocols [C]∥ Proceedings of the 9th International Conference on Principles of Distributed Systems. Pisa: LNCS, 2005, 3974: 103-117.
[5] LAMPORT L. Proving the correctness of multiprocess programs [J]. IEEE Transactions on Software Engineering, 1977, 3(2): 125-143.
[6] HOLZMANN G J. The SPIN model checker: primer and reference manual [M]. Boston: Wesley, 2003.
[7] LAMPORT L. Fairness and hyperfairness [J]. Distributed Computing, 2000, 13(4): 239-245.
[8] GELDENHUYS J, VALMARI A. More efficient on-the-fly LTL verification with Tarjans algorithm [J]. Theoritical Computer Science, 2005, 345(1): 60-82.
[9] HENZINGER M R, TELLE J A. Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning [C]∥ Proceedings of the 5th Scandinavian Workshop on Algorithm Theory. Gothenburg: Springer, 1996: 16-27.
[10] KESTEN Y, PNUELI A, RAVIV L, et al. Model checking with strong fairness [J]. Formal Methods and System Design, 2006, 28(1): 57-84.
[11] TARJAN R. Depth-first search and linear graph algorithms [J]. SIAM Journal on Computing, 1972, 2(1): 146-160.
[12] CANEPA D, POTOP-BUTUCARU M. Stabilizing token schemes for population protocols [J]. Computing Research Repository, 2008, 806(3471): 765-784.
[13] JIANG H. Distributed systems of simple interacting agents [D]. New Haven: Yale University, 2007.
[14] SUN Jun, LIU Yang, DONG Jin-song, et al. PAT: towards flexible verification under fairness [C]∥ Proceedings of the 21st International Conference on Computer Aided Verification. Grenoble: Springer, 2009: 709-714.
[15] LAMPORT L. Proving the correctness of multiprocess programs [J]. IEEE Transactions on Software Engineering, 1977, 3(2): 125-143.
[16] APT K R, FRANCEZ N, KATZ S. Appraising fairness in languages for distributed programming [J]. Distributed Computing, 1988, 2(4): 226-241.
[17] COURCOUBETIS C, VARDI M Y, WOLPER P, et al. Memory-efficient algorithms for the verification of temporal properties [J]. Formal Methods in System Design, 1992, 1(2/3): 275-288.
[18] HARDIN R H, KURSHAN R P, SHUKLA S K, et al. A new heuristic for bad cycle detection using BDDs [J]. Formal Methods in System Design, 2001, 18(2): 131-140.

No related articles found!