CCGS System
CSTR:
Author:
  • Article
  • | |
  • Metrics
  • |
  • Reference [10]
  • |
  • Related [20]
  • | | |
  • Comments
    Abstract:

    Model checking is a formal method to verify the system satisfies an expected property or not. Trere are two significant advantages of it, one is that it is fully automatic and the other is that if the system doesn't satisfy the checked property, it will generate an counterexamples which can help to fix errors in the system. The main purpose of this paper is to generate this counterexamples efficiently and intuitively. In order to generate the counterexamples efficiently and graphically display the operating processes of the system running alongside the concrete counterexamples, a system CCGS has been developed. Experimental results have shown that CCGS delivers an expected performance, and can help to improve the correctness and safety of the checked systems.

    Reference
    1 Alur R, Henzinger TA. Real-time system=discrete system + clock variables. Software Tools for Technology Transfer, 1997, 1(1/2): 86-89.
    2 Clarke EM, Grumberg O, Peled DA. Model Checking. The
    MIT Press, 1999.
    3 李广元,唐稚松.带有时钟变量的线性时序逻辑与实时系统验证.软件学报,2002,13(1):33-41.
    4 Bengtsson J, Wang Y.Timed automata: semantics, algori-thms and tools. LNCS 3098, Springer-Verlag, 2004: 87-124.
    5 Beyer D, Noack A. Efficient verification of timed automata using BDDs. Proc. of the 6th International ERCIM Workshop on Formal Methods for Industrial Critical Systems, 2001. 95-113.
    6 魏绪凯.时间自动机关于LTL性质的符号化模型检测工具及其改进[博士学位论文].北京:中国科学院软件研究所,2009.
    7 Li GY. Checking timed BÜchi automata emptiness using LU-abstractions. Proc. of the 7th International Conference on Formal Modeling and Analysis of Timed Systems, 2009. 228-442.
    8 Yu F, Wang BY. Sat-based model checking for region automata. International Journal of Foundations of Computer Science, 2006, 17(4): 775-796.
    9 Duret-Lutz A, Poitrenatud D. Spot: An extensive model checking library using transition-based generalized BÜchi automata. Volendam, Netherlands. IEEE Computer Society Process. 2004. 76-83.
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

信贤卫.具体反例生成与图形化显示系统.计算机系统应用,2013,22(11):51-57

Copy
Share
Article Metrics
  • Abstract:1666
  • PDF: 2599
  • HTML: 0
  • Cited by: 0
History
  • Received:April 12,2013
  • Revised:April 22,2013
  • Online: November 22,2013
Article QR Code
You are the first990502Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-3
Address:4# South Fourth Street, Zhongguancun,Haidian, Beijing,Postal Code:100190
Phone:010-62661041 Fax: Email:csa (a) iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063