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

doi:10.1007/s11704-017-7036-2

Front. Comput. Sci.

2019, Vol. 13

Issue (1) : 51-72 https://doi.org/10.1007/s11704-017-7036-2

RESEARCH ARTICLE

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

Kazuhiro OGATA(

)

School of Information Science, Japan Advanced Institute of Science and Technology (JAIST) 1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan

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

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

Corresponding Author(s): Kazuhiro OGATA

Just Accepted Date: 24 July 2017 Online First Date: 15 November 2018 Issue Date: 31 January 2019

Cite this article:

Kazuhiro OGATA. A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions[J]. Front. Comput. Sci., 2019, 13(1): 51-72.

URL:

https://academic.hep.com.cn/fcs/EN/10.1007/s11704-017-7036-2
https://academic.hep.com.cn/fcs/EN/Y2019/V13/I1/51

1	KOgata, MZhang. 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 https://doi.org/10.1109/COMPSAC.2013.104
2	KOgata. Model checking liveness properties under fairness & antifairness assumptions. In: Proceedings of the 20th Asia-Pacific Software Engineering Conference. 2013, 565–570
3	ZManna, APnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Science & Business Media, 1992, 16 https://doi.org/10.1007/978-1-4612-0931-7
4	LLamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., 2002
5	E MClarke, O Grumberg, D APeled. Model Checking. Massachusetts: MIT Press, 1999
6	TLatvala. 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 https://doi.org/10.1007/3-540-45740-2_15
7	JSun, YLiu, J SDong, J Pang. PAT: towards flexible verification under fairness. In: Proceedings of the 21st International Conference on Computer Aided Verification. 2009, 709–714 https://doi.org/10.1007/978-3-642-02658-4_59
8	YSi, JSun, YLiu, J S Dong, JPang, S JZhang, XYang. Model checking with fairness assumptions using PAT. Frontiers of Computer Science, 2014, 8(1): 1–16 https://doi.org/10.1007/s11704-013-3091-5
9	KBae, J Meseguer. State/event-based LTLmodel checking under parametric generalized fairness. In: Proceedings of the 23rd International Conference on Computer Aided Verification. 2011, 132–148 https://doi.org/10.1007/978-3-642-22110-1_11
10	KBae, J Meseguer. Model checking LTLR formulas under localized fairness. In: Proceedings of the 9th International Workshop on Rewriting Logic and its Applications. 2012, 99–117 https://doi.org/10.1007/978-3-642-34005-5_6
11	KBae, J Meseguer. Model checking linear temporal logic of rewriting formulas under localized fairness. Science of Computer Programming, 2015, 99: 193–234 https://doi.org/10.1016/j.scico.2014.02.006
12	G JHolzmann. The SPINModel Checker – Primer and Reference Manual. Reading: Addison-Wesley, 2004
13	LDe Moura, SOwre, HRueß, JRushby, N Shankar, MSorea, ATiwari. SAL 2. In: Proceedings of the 16th International Conference on Computer Aided Verification. 2004, 496–500 https://doi.org/10.1007/978-3-540-27813-9_45
14	MClavel, F Durán, SEker, PLincoln, N Martí-Oliet, JMeseguer, CTalcott. All About Maude – A High-Performance Logical Framework: How to Specify, Program and Verify Systems in Rewriting Logic. Springer-Verlag, 2007
15	ISuzuki, TKasami. A distributed mutual exclusion algorithm. ACM Transactions on Computer Systems, 1985, 3(4): 344–349 https://doi.org/10.1145/6110.214406
16	KOgata, K Futatsugi. 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 https://doi.org/10.1007/978-0-387-35496-5_13
17	KOgata, K Futatsugi. 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 https://doi.org/10.1093/ietfec/e90-a.8.1690
18	KFutatsugi, J AGoguen, KOgata. 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	JMeseguer. Localized fairness: a rewriting semantics. In: Proceedings of the 16th International Conference on Term Rewriting and Applications. 2005, 250–263 https://doi.org/10.1007/978-3-540-32033-3_19
20	SChaki, E MClarke, JOuaknine, N Sharygina, NSinha. State/eventbased software model checking. In: Proceedings of the 4th International Conference on Integrated Formal Methods. 2004, 128–147 https://doi.org/10.1007/978-3-540-24756-2_8
21	K LMcMillan. 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 https://doi.org/10.1007/978-3-540-31980-1_1
22	L LMaksimova. Temporal logics with “the next” operator do not have interpolation or the Beth property. Siberian Mathematical Journal, 1991, 32(6): 989–993 https://doi.org/10.1007/BF00971204
23	AGheerbrant, B Ten Cate. Craig interpolation for linear temporal languages. In: Proceedings of the 23rd International Workshop on Computer Science Logic. 2009, 287–301 https://doi.org/10.1007/978-3-642-04027-6_22
24	E MClarke, D ELong, K LMcMillan. Compositional model checking. In: Proceedings of the 4th Symposium on Logic in Computer Science. 1989, 353–362 https://doi.org/10.1109/LICS.1989.39190
25	R PKurshan, L Lamport. Verification of a multiplier: 64 bits and beyond. In: Proceedings of the 5th International Conference on Computer Aided Verification. 1993, 166–179 https://doi.org/10.1007/3-540-56922-7_14
26	MAbadi, L Lamport. Open systems in TLA. In: Proceedings of the 13th ACM Symposium on Principles of Distributed Computing. 1994, 81–90 https://doi.org/10.1145/197917.197960

[1]

Download

[1]	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.
[2]	Anil Kumar KARNA, Yuting CHEN, Haibo YU, Hao ZHONG, Jianjun ZHAO. The role of model checking in software engineering[J]. Front. Comput. Sci., 2018, 12(4): 642-668.
[3]	Yu ZHOU, Nvqi ZHOU, Tingting HAN, Jiayi GU, Weigang WU. Probabilistic verification of hierarchical leader election protocol in dynamic systems[J]. Front. Comput. Sci., 2018, 12(4): 763-776.
[4]	Fei HE, Yuan GAO, Liangze YIN. Efficient software product-line model checking using induction and a SAT solver[J]. Front. Comput. Sci., 2018, 12(2): 264-279.
[5]	Laixiang SHAN,Xiaomin DU,Zheng QIN. Efficient approach of translating LTL formulae into Büchi automata[J]. Front. Comput. Sci., 2015, 9(4): 511-523.
[6]	Luxi CHEN,Linpeng HUANG,Chen LI,Tao ZAN. Integrating behavior analysis into architectural modeling[J]. Front. Comput. Sci., 2015, 9(1): 15-33.
[7]	Yuyue DU,Yuhui NING. Property analysis of logic Petri nets by marking reachability graphs[J]. Front. Comput. Sci., 2014, 8(4): 684-692.
[8]	Jingyuan WANG,Jiangtao WEN,Yuxing HAN,Jun ZHANG,Chao LI,Zhang XIONG. Achieving high throughput and TCP Reno fairness in delay-based TCP over large networks[J]. Front. Comput. Sci., 2014, 8(3): 426-439.
[9]	Yuanjie SI, Jun SUN, Yang LIU, Jin Song DONG, Jun PANG, Shao Jie ZHANG, Xiaohu YANG. Model checking with fairness assumptions using PAT[J]. Front. Comput. Sci., 2014, 8(1): 1-16.
[10]	Savas KONUR. A survey on temporal logics for specifying and verifying real-time systems[J]. Front. Comput. Sci., 2013, 7(3): 370-403.
[11]	Zhiyuan LIU, Jun PANG, Chenyi ZHANG. Design and formal verification of a CEM protocol with transparent TTP[J]. Front Comput Sci, 2013, 7(2): 279-297.
[12]	Anh Tuan LUU, Jun SUN, Yang LIU, Jin Song DONG, Xiaohong LI, Thanh Tho QUAN. SeVe: automatic tool for verification of security protocols[J]. Front Comput Sci, 2012, 6(1): 57-75.
[13]	Conghua ZHOU, Bo SUN, Zhifeng LIU. Abstraction for model checking multi-agent systems[J]. Front Comput Sci Chin, 2011, 5(1): 14-25.
[14]	Jiaqi ZHU, Hanpin WANG, Zhongyuan XU, Chunxiang XU, . A new model for model checking: cycle-weighted Kripke structure[J]. Front. Comput. Sci., 2010, 4(1): 78-88.
[15]	Wanwei LIU, Ji WANG, Huowang CHEN, Xiaodong MA, Zhaofei WANG. symbolic model checking APSL[J]. Front Comput Sci Chin, 2009, 3(1): 130-141.

Viewed

Full text

Abstract

Cited

Shared

Discussed