• 中国精品科技期刊
  • CCF推荐A类中文期刊
  • 计算领域高质量科技期刊T1类
Advanced Search
Wei Ou, Shi Yufeng, Xu Bingfeng, Huang Zhiqiu, Chen Zhe. Abstract Modeling Formalisms in Software Model Checking[J]. Journal of Computer Research and Development, 2015, 52(7): 1580-1603. DOI: 10.7544/issn1000-1239.2015.20140413
Citation: Wei Ou, Shi Yufeng, Xu Bingfeng, Huang Zhiqiu, Chen Zhe. Abstract Modeling Formalisms in Software Model Checking[J]. Journal of Computer Research and Development, 2015, 52(7): 1580-1603. DOI: 10.7544/issn1000-1239.2015.20140413

Abstract Modeling Formalisms in Software Model Checking

More Information
  • Published Date: June 30, 2015
  • Abstraction is a fundamental technique for solving the state-explosion problem in software model checking. In this paper, we survey a variety of abstract modeling formalisms that have been developed for this over the years. We first provide an overview of abstract software model checking based on the theoretical framework of abstract interpretation. We then discuss in detail several abstract modeling formalisms that are represented by 1) boolean Kripke structures, supporting traditional over-approximation or under-approximation; 2) Kripke modal transition systems and mixed transition systems, respectively corresponding to 3-valued and 4-valued Kripke structures, supporting both over-approximation and under-approximation on a single model; and 3) models with hyper transitions, including generalized Kripke modal transition systems and hyper transition systems, allowing for more precise abstract model checking. We discuss the corresponding approximation relations and optimal abstract models, and highlight their shortcomings and the motivations for the development of new formalisms. We also introduce the completeness results of abstract modeling formalisms. Finally, we discuss the problems in theoretical and practical aspects of abstract models and point out future research directions.
  • Related Articles

    [1]Wang Guoqing, Zhuang Lei, He Mengyang, Song Yu, Ma Ling. Calculation Principle and Algorithm for the Window of Exact Acceleration in Real-Time Model Checking[J]. Journal of Computer Research and Development, 2020, 57(1): 214-226. DOI: 10.7544/issn1000-1239.2020.20190052
    [2]Wang Yuquan, Wen Lijie, Yan Zhiqiang. Alignment Based Conformance Checking Algorithm for BPMN 2.0 Model[J]. Journal of Computer Research and Development, 2017, 54(9): 1920-1930. DOI: 10.7544/issn1000-1239.2017.20160756
    [3]Zhong Shan, Liu Quan, Fu Qiming, Zhang Zongzhang, Zhu Fei, Gong Shengrong. A Heuristic Dyna Optimizing Algorithm Using Approximate Model Representation[J]. Journal of Computer Research and Development, 2015, 52(12): 2764-2775. DOI: 10.7544/issn1000-1239.2015.20148160
    [4]Pang Tao, Duan Zhenhua. Symbolic Model Checking of WISHBONE on-Chip Bus[J]. Journal of Computer Research and Development, 2014, 51(12): 2759-2771. DOI: 10.7544/issn1000-1239.2014.20131164
    [5]Jiang Hua. Efficient Global Model-Checking for Propositional μ-Calculus[J]. Journal of Computer Research and Development, 2010, 47(8): 1424-1433.
    [6]Jiang Hua, Li Xiang. Model Checking for Mobile Ambients[J]. Journal of Computer Research and Development, 2009, 46(10): 1750-1757.
    [7]Zhang Junhua, Huang Zhiqiu, and Cao Zining. Counterexample Generation for Probabilistic Timed Automata Model Checking[J]. Journal of Computer Research and Development, 2008, 45(10): 1638-1645.
    [8]Huang Weiping. Program Restructuring to Improve Efficiency of Software Model Checking[J]. Journal of Computer Research and Development, 2008, 45(8): 1417-1422.
    [9]Wu Lijun, Su Kaile, Chen Qingliang, Yang Zhihua. Algorithm Research on “On the Fly” Model Checking Temporal Logics of Knowledge in Multi-Agent Systems[J]. Journal of Computer Research and Development, 2006, 43(8): 1417-1424.
    [10]He Jian, Qin Zheng. Modeling and Checking the Behavior of Software Architecture[J]. Journal of Computer Research and Development, 2005, 42(11): 2018-2024.

Catalog

    Article views (1864) PDF downloads (1178) Cited by()

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return