Methodology and Environment for Effectively Using Theorem Provers and Model Checkers

2008 Fiscal Year Final Research Report

• Project/Area Number: 18500019
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: OGATA Kazuhiro Japan Advanced Institute of Science and Technology, 情報科学研究科, 准教授 (30272991)
• Project Period (FY): 2006 – 2008
• Keywords: 仕様記述 / 仕様検証 / モデル検査 / 仕様変換 / 観測遷移システム / CafeOBJ、Maude / メタプログラミング

Research Abstract

証明支援系とモデル検査器を効果的に利用できるよう、定理証明向きのシステム仕様をモデル検査向きのシステム仕様に自動変換する方法を考案した。変換により、モデル検査向きのシステム仕様が大きくなりすぎて効果的にモデル検査ができなくなることを防ぐための工夫を行った。提案した変換方法の有効性を確認するため、電子商取引プロトコルiKPとMondex の検証実験に適用した。また、変換を支援する変換ツールの拡張性の高い実装方法も提案した。この実装方法では、複数の変換規則をモジュラーに組み入れることを可能にする。

Research Products

• [Journal Article] A Specification Translation from Behavioral Specifications to Rewrite Specifications (2008)
  • Author(s): Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: IEICE TRANSACTIONS on Information and Systems E91-D(5) Pages: 1492-1503
  • Peer Reviewed
• [Journal Article] Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm, IEICE TRANSACTIONS on Fundamental of Electronics (2007)
  • Author(s): Kazuhiro Ogata and Kokichi Futatsugi
  • Journal Title: Communications, Computer Science E90-A(8) Pages: 1690-1703
  • Peer Reviewed
• [Presentation] Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System (2007)
  • Author(s): Weiqiang Kong, Kazuhiro Ogata and Kokichi Futatsugi
  • Organizer: Proceedings of the 6th International Conference on Integrated Formal Methods (6th IFM), LNCS 4591, Springer
  • Place of Presentation: Oxford, UK
  • Year and Date: 20070702-05
• [Presentation] Falsification of OTSs by Searches of Bounded Reachable State Spaces (2006)
  • Author(s): Kazuhiro Ogata, Weiqiang Kong and Kokichi Futatsugi
  • Organizer: Proceedings of the 18th International Conference on Software Engineering and Knowledge Engineering (18th SEKE), Knowledge Systems Institute
  • Place of Presentation: San Francisco, USA.
  • Year and Date: 20060705-07
• [Presentation] Induction-Guided (2006)
  • Author(s): Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong and Kokichi Futatsugi
  • Organizer: Falsification, Prceedings of the 8th International Conference on Formal Engineering Methods (8th ICFEM), LNCS 4260, Springer
  • Place of Presentation: Macao
  • Year and Date: 20060601-03