Automatic Verification of Statecharts by Abstraction and Refinement of Hierarchical Structure

• YAMAZAKI Shinichi

  Division of Electrical and Computer Engineering, Graduate School of Natural Science & Technology, Kanazawa University

• YAMANE Satoshi

  Division of Electrical and Computer Engineering, Graduate School of Natural Science & Technology, Kanazawa University

Bibliographic Information

Other Title

• 階層構造の抽象化精錬によるステートチャートの自動検証

Abstract

Statechart is a powerful modeling language that is taken in UML. We propose a verification algorithm by abstraction and refinement of hierarchical structure of statechart. The algorithm performs reachability analysis on an abstract model. Subsequently, if the counterexample exists, the algorithm refines an abstract model using it. Moreover, the algorithm checks the validity of counterexample and performs reachability analysis again when it is a spurious counterexample. The algorithm repeats these procedures automatically until a solution is provided. We have implemented a prototype of our verification algorithm and confirmed that there is an effect to downsize state space by experiments.

Journal

• Computer Software

  Computer Software 26 (3), 155-170, 2009

  Japan Society for Software Science and Technology

Details

• CRID: 1390001204737454208
• NII Article ID: 130004549140
• DOI: 10.11309/jssst.26.3_155
• ISSN: 02896540
• Data Source:
  • JaLC
  • CiNii Articles
• Abstract License Flag: Disallowed