期刊文献+

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

原文传递
导出
摘要 This paper proposes an approach to making livehess 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.
出处 《Frontiers of Computer Science》 SCIE EI CSCD 2019年第1期51-72,共22页 中国计算机科学前沿(英文版)
  • 相关文献

参考文献1

二级参考文献46

  • 1Giannakopoulou D, Magee J, Kramer J. Checking progress with action priority: is it fair? In: Proceedings of the 7th ACM SIGSOFT Sympo?sium on the Foundations of Software Engineering. 1999,511-527.
  • 2Lamport L. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 1977,3(2): 125-143.
  • 3Kurshan R P. Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1995.
  • 4Sun J, Liu Y, Dong J S, Wang H H. Specifying and verifying event?based fairness enhanced systems. In: Proceedings of the 10th Interna?tional Conference on Formal Engineering Methods. 2008, 318-337.
  • 5Sun J, Liu y, Roychoudhury A, Liu S, Dong J. Fair model checking with process counter abstraction. FM 2009: Formal Methods, 2009, 123-139.
  • 6Fischer M J, Jiang H. Self-stabilizing leader election in networks of finite-state anonymous agents. In: Proceedings of the 10th Interna?tional Conference on Principles of Distributed Systems. 2006,395-409.
  • 7Angluin D, Aspnes J, Fischer M J, Jiang H. Self-stabilizing popula?tion protocols. In: Proceedings of the 9th International Conference on Principles of Distributed Systems. 2005, 103-117.
  • 8Angluin D, Fischer M J, Jiang H. Stabilizing consensus in mobile net?works. In: Proceedings of the 2006 International Conference on Dis?tributed Computing in Sensor Systems. 2006, 37-50.
  • 9Canepa D, Potop-Butucaru M. Stabilizing Token Schemes for Popula?tion Protocols. Computing Research Repository, 2008, abs/0806.3471.
  • 10Rozier K Y, Vardi M Y. LTL Satisfiability Checking. In: Proceedings of the 14th International SPIN Workshop. 2007, 149-167.

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部