Methodology and Environment for Effectively Using Theorem Provers and Model Checkers

• 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
• Project Status: Completed (Fiscal Year 2008)
• Budget Amount: ¥4,350,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥750,000); Fiscal Year 2008: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000); Fiscal Year 2007: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000); Fiscal Year 2006: ¥1,100,000 (Direct Cost: ¥1,100,000)
• Keywords: 仕様記述 / 仕様検証 / モデル検査 / 仕様変換 / 観測遷移システム / CafeOBJ、Maude / メタプログラミング / 定理証明 / 変換 / CafeOBJ / Maude / 変換器 / 有界モデル検査 / 数学的帰納法 / 反例 / 補題 / IGF / 補題発見

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
  • NAID: 10026803820
  • Peer Reviewed
• [Journal Article] A Specification Translation from Behavioral Specifications to Rewrite Specifications (2008)
  • Author(s): M. Nakamura, K. Weiqiang, K. Ogata, K. Futatsugi
  • Journal Title: IEICE TRANSACTIONS on Information and Systems E91-D Pages: 1492-1503
  • NAID: 10026803820
  • Peer Reviewed
• [Journal Article] Maude : 書換え論理に基づく計算機言語および処理系 (2008)
  • Author(s): 緒方和博, 中村正樹, 二木厚吉
  • Journal Title: コンピュータソフトウェア(日本ソフトウェア科学会論文誌) 25 Pages: 78-84
  • NAID: 130004549110
  • 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
• [Journal Article] Comparison of Maude and SAL by Conducting Case Studies Model Checking a Distributed Algorithm (2007)
  • Author(s): K.Ogata, K.Futatsugi
  • Journal Title: IEICE Trans.Fundamentals E90-A Pages: 1690-1703
  • NAID: 110007540867
  • Peer Reviewed
• [Journal Article] Creme: An Automatic Invariant Prover of Behavioral Specifications (2007)
  • Author(s): M.Nakano, K, Ogata, M.Nakamura, K.Futatsugi
  • Journal Title: Int'l J.Software Engineeing & Knowledge Engineering 17 Pages: 783-804
  • Peer Reviewed
• [Journal Article] Algebraic Approaches to Formal Analysis of the Mondex Electronic Purse System (2007)
  • Author(s): W.Kong, K.Ogata, K.Futatsugi
  • Journal Title: Proc.of the 6th Int'l Conf on Integrated Formal Methods LNCS4951 Pages: 393-412
  • NAID: 110006386813
  • Peer Reviewed
• [Journal Article] Specification and Verification of Workflows with RBAC Mechanism and SoD Constraints (2007)
  • Author(s): Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: International Journal of Software Engineering and knowledge Engineering 17・1 Pages: 3-32
• [Journal Article] Induction-Guided Falsification (2006)
  • Author(s): Kazuhiro Ogata, Masahiro Nakano, Weiqiang Kong, Kokichi Futatsugi
  • Journal Title: Proc. of the 8^th International Conference on Formal Engineering Methods (LNCS 4260) Pages: 114-131
  • NAID: 120000861068
• [Journal Article] Falsification of OTSs by Searches of Bounded Reachable State Spaces (2006)
  • Author(s): Kazuhiro Ogata, Weiqiang Kong, Kokichi Futatsugi
  • Journal Title: Proc. of the 18^th International Conference on Software Engineering and knowledge Engineering Pages: 440-445
• [Journal Article] A Review of Induction-Guided Falsification and Towards its Automation (2006)
  • Author(s): W.kong, K.Ogata, M.Nakamura, K.Futatsugi
  • Journal Title: Proc. of the 1^st Asian Working Conference on Verified Software Pages: 48-59
• [Journal Article] Automating Invariant Verification of Behavioral Specifications (2006)
  • Author(s): M.Nakano, K.Ogata, M.Nakamura, K.Futatsugi
  • Journal Title: Proc. of the 6^th International Conference on Quality Software Pages: 49-56
• [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
• [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.
• [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