Model Checking Analysis of Observational Transition System with SMV

被引：0
|
作者：
He, Tao [1 ]
Li, Huazhong [1 ]
Qin, Guorong [1 ]
机构：
[1] Shenzhen Inst Informat Technol, Software Engn Dept, Shenzhen, Peoples R China
来源：
INFORMATION COMPUTING AND APPLICATIONS, PT II | 2011年 / 244卷
关键词：
Model Checking; Model-based verification; SMV; CafeOBJ; Model Checking Tool; VERIFICATION;
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Model checking is an important way in developing high confidence systems. A model checking method basing on theorem proving is proposed in this paper, which describes the infinite system state by CafeOBJ and transfers a CafeOBJ specification to a finite SMV specification, and its tool has been implemented. It mainly observes transition system and shows that a counter example of a corresponding SMV specification is also a counter example of a CafeOBJ specification. It can find errors lurked in systems at earlier stages of their development processes to avoid spending much money and time to correct errors later.
引用
收藏
页码：537 / 544
页数：8
相关论文
共 50 条
  • [1] Model checking PSL using HOL and SMV
    Tuerk, Thomas
    Schneider, Klaus
    Gordon, Mike
    HARDWARE AND SOFTWARE, VERIFICATION AND TESTING, 2007, 4383 : 1 - +
  • [2] Checking the TWIN elevator system by translating Object-Z to SMV
    Preibusch, Soeren
    Kammueller, Florian
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2008, 4916 : 38 - +
  • [3] Symbolic model checking of interactions in sequence diagrams with combined fragments by SMV
    Kawakami, Yuka
    Yokogawa, Tomoyuki
    Miyazaki, Hisashi
    Amasaki, Sousuke
    Sato, Yoichiro
    Hayase, Michiyoshi
    World Academy of Science, Engineering and Technology, 2010, 71 : 543 - 546
  • [4] Symbolic model checking of interactions in sequence diagrams with combined fragments by SMV
    Kawakami, Yuka
    Yokogawa, Tomoyukit
    Miyazaki, Hisashi
    Amasaki, Sousuke
    Sato, Yoichiro
    Hayase, Michiyoshi
    World Academy of Science, Engineering and Technology, 2010, 47 : 543 - 546
  • [5] Analysis and checking of safety transition system based on TLA
    Liang, Wan
    Xiang, Li
    2008 4TH INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATIONS, NETWORKING AND MOBILE COMPUTING, VOLS 1-31, 2008, : 12580 - 12583
  • [6] Petri nets behavioral equivalence checking in SMV
    Drozdov, Dmitrii
    Dubinin, Victor
    Kulagin, Vladimir
    2016 INTERNATIONAL SIBERIAN CONFERENCE ON CONTROL AND COMMUNICATIONS (SIBCON), 2016,
  • [7] Transition-by-transition FSM traversal for reachability analysis in bounded model checking
    Nguyen, MD
    Stoffel, D
    Wedler, M
    Kunz, W
    ICCAD-2005: INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, DIGEST OF TECHNICAL PAPERS, 2005, : 1068 - 1075
  • [8] Analysis and Checking of Controllable Property Transition System Based on TLA
    Wan, Liang
    Li, Xiang
    2008 2ND INTERNATIONAL CONFERENCE ON ANTI-COUNTERFEITING, SECURITY AND IDENTIFICATION, 2008, : 264 - 267
  • [9] Analysis and Checking of Internet Banking Based on Safety Transition System
    Wan Liang
    Huang Yiwang
    Li Xiang
    DCABES 2008 PROCEEDINGS, VOLS I AND II, 2008, : 907 - 911
  • [10] Model checking on state transition diagram
    Das, B
    Sarkar, D
    Chattopadhyay, S
    ASP-DAC 2004: PROCEEDINGS OF THE ASIA AND SOUTH PACIFIC DESIGN AUTOMATION CONFERENCE, 2004, : 412 - 417
12345