Verification of Problem Models with Proof Scores

2009 Fiscal Year Final Research Report

• Project/Area Number: 18300008
• Research Category: Grant-in-Aid for Scientific Research (B)
• Allocation Type: Single-year Grants
• Section: 一般
• Research Field: Software
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: FUTATSUGI Kokichi Japan Advanced Institute of Science and Technology, 情報科学研究科, 教授 (50251971)
• Co-Investigator(Renkei-kenkyūsha): NAKAMURA Masaki 金沢大学, 電子情報学系, 助教 (40345658)
• Project Period (FY): 2006 – 2009
• Keywords: 仕様記述 / 仕様検証 / 形式手法 / 問題モデル / 証明スコア / 帰納法 / 場合分け

Research Abstract

「帰納法」と「場合分け」は、問題モデル(問題領域や応用領域におけるモデル)の証明スコアによる検証法の基本技術である。本研究では、多様な応用分野で有効な帰納法と場合分けについて以下の成果を得た。(1)帰納法をデータ型・プロセス型の帰納的な構造に基づき定式化した。(2)場合分けを構成子からの項の生成に基づき定式化した。(3)(1),(2)に基づき、汎用的な証明規則を定式化するとともに、推論と探索を融合した強力な検証法を開発した。

Research Products

• [Journal Article] Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications (2010)
  • Author(s): Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: J. Symb. Comput 45(5) Pages: 551-573
  • Peer Reviewed
• [Journal Article] CafeOBJ入門(1)-(6)、コンピュタソフトウェア (2009)
  • Author(s): 二木厚吉, 緒方和博, 中村正樹
  • Journal Title: 日本ソフトウェア科学会論文誌 25(2),25(2),25(3),25(4),26(1),26(2) Pages: 1-13, 14-27, 69-80, 68-84, 71-83, 93-106
  • Peer Reviewed
• [Journal Article] Constructor-based institutions (2009)
  • Author(s): D. Gaina, K. Futatsugi, K. Ogata
  • Journal Title: Proc. of CALCO 2009 5728 Pages: 398-412
  • Peer Reviewed
• [Journal Article] User-Defined On-Demand Matching (2009)
  • Author(s): Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: IEICE Transactions 92-D(7) Pages: 1401-1411
  • Peer Reviewed
• [Journal Article] フォーマルメソッドの新展開-検証進化可能電子社会の中核技術- (2008)
  • Author(s): 二木厚吉
  • Journal Title: 情報処理 Vol.49,No.5 Pages: 521-529
  • Peer Reviewed
• [Journal Article] Checking Assignments of Controls to Risks for Internal Control (2008)
  • Author(s): Yasuhito Arimoto, Yuji Watanabe, Michiharu Kudoh, Kokichi Futatsugi
  • Journal Title: Proc. of 2nd International Conference on Theory and Practice of Electronic Governance 2008, ACM Pages: 98-104
  • Peer Reviewed
• [Journal Article] Verifying Design with Proof Scores (2008)
  • Author(s): K. Futatsugi, J.A. Goguen, K. Ogata
  • Journal Title: Proc. of 1st VSTTE, LNCS 4171, Springer Pages: 277-290
  • Peer Reviewed
• [Journal Article] A Specification Translation from Behavioral Specifications to Rewrite Specifications (2008)
  • Author(s): Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: IEICE Transactions 91-D(5) Pages: 1492-1503
  • Peer Reviewed
• [Journal Article] Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes (2008)
  • Author(s): Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: Proc. of the 10th Intl. Conference on Formal Engineering Methods (10th ICFEM) 5256 Pages: 187-206
  • Peer Reviewed
• [Journal Article] Formal digital license language with OTS/CafeOBJ method (2008)
  • Author(s): Jianwen Xiang, Dines Bjorner, Kokichi Futatsugi
  • Journal Title: Proc. of IEEE/ACS Intl. Conference on Computer Systems and Applications Pages: 652-660
  • Peer Reviewed
• [Journal Article] Simulation-based verification for invariant properties in the OTS/CafeOBJ method (2008)
  • Author(s): Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: Refine 2007, ENTCS 201, Elsevier Pages: 127-154
  • Peer Reviewed
• [Journal Article] Specification and Verification of Workflows with RBAC Mechanism and SoD Constraints (2007)
  • Author(s): W. Kong, K. Ogata, K. Futatsugi
  • Journal Title: Intl. J. of Software Eng. and Knowledge Eng 17(1) Pages: 3-32
  • Peer Reviewed
• [Journal Article] On equality predicates in algebraic specification languages (2007)
  • Author(s): Masaki Nakamura, Kokichi Futatsugi
  • Journal Title: Proc. of the 4th International Colloquium on Theoretical Aspects of Computing (ICTAC 2007) 4711 Pages: 381-395
  • Peer Reviewed
• [Journal Article] Modeling and verification of real-time systems based on equations (2007)
  • Author(s): Kazuhiro Ogata, Kokichi Futatsugi
  • Journal Title: Sci. of Comp. Prog 66(2) Pages: 162-180
  • Peer Reviewed
• [Presentation] Verifying Specifications with Proof Scores in CafeOBJ (2006)
  • Author(s): Kokichi FUTATSUGI
  • Organizer: Proc. of 21st IEEE International Conference on Automated Software Engineering
  • Place of Presentation: Tokyo
  • Year and Date: 2006-02-20
• [Book] 法令工学の提案(片山卓也) (2007)
  • Author(s): 二木厚吉,緒方和博,有本泰仁
  • Total Pages: 71-93
  • Publisher: JAIST
• [Remarks] 以下のウェッブページを通じて、開発したシステムと例題、発表論文などを公開している。
  • URL: http://www.ldl.jaist.ac.jp/cafeobj