• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2009 年度 研究成果報告書

証明スコアによる問題モデルの検証技術

研究課題

  • PDF
研究課題/領域番号 18300008
研究種目

基盤研究(B)

配分区分補助金
応募区分一般
研究分野 ソフトウエア
研究機関北陸先端科学技術大学院大学

研究代表者

二木 厚吉  北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)

連携研究者 中村 正樹  金沢大学, 電子情報学系, 助教 (40345658)
研究期間 (年度) 2006 – 2009
キーワード仕様記述 / 仕様検証 / 形式手法 / 問題モデル / 証明スコア / 帰納法 / 場合分け
研究概要

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

  • 研究成果

    (17件)

すべて 2010 2009 2008 2007 2006 その他

すべて 雑誌論文 (14件) (うち査読あり 14件) 学会発表 (1件) 図書 (1件) 備考 (1件)

  • [雑誌論文] Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications2010

    • 著者名/発表者名
      Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      J. Symb. Comput 45(5)

      ページ: 551-573

    • 査読あり
  • [雑誌論文] CafeOBJ入門(1)-(6)、コンピュタソフトウェア2009

    • 著者名/発表者名
      二木厚吉, 緒方和博, 中村正樹
    • 雑誌名

      日本ソフトウェア科学会論文誌 25(2),25(2),25(3),25(4),26(1),26(2)

      ページ: 1-13, 14-27, 69-80, 68-84, 71-83, 93-106

    • 査読あり
  • [雑誌論文] Constructor-based institutions2009

    • 著者名/発表者名
      D. Gaina, K. Futatsugi, K. Ogata
    • 雑誌名

      Proc. of CALCO 2009 5728

      ページ: 398-412

    • 査読あり
  • [雑誌論文] User-Defined On-Demand Matching2009

    • 著者名/発表者名
      Masaki Nakamura, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      IEICE Transactions 92-D(7)

      ページ: 1401-1411

    • 査読あり
  • [雑誌論文] フォーマルメソッドの新展開-検証進化可能電子社会の中核技術-2008

    • 著者名/発表者名
      二木厚吉
    • 雑誌名

      情報処理 Vol.49,No.5

      ページ: 521-529

    • 査読あり
  • [雑誌論文] Checking Assignments of Controls to Risks for Internal Control2008

    • 著者名/発表者名
      Yasuhito Arimoto, Yuji Watanabe, Michiharu Kudoh, Kokichi Futatsugi
    • 雑誌名

      Proc. of 2nd International Conference on Theory and Practice of Electronic Governance 2008, ACM

      ページ: 98-104

    • 査読あり
  • [雑誌論文] Verifying Design with Proof Scores2008

    • 著者名/発表者名
      K. Futatsugi, J.A. Goguen, K. Ogata
    • 雑誌名

      Proc. of 1st VSTTE, LNCS 4171, Springer

      ページ: 277-290

    • 査読あり
  • [雑誌論文] A Specification Translation from Behavioral Specifications to Rewrite Specifications2008

    • 著者名/発表者名
      Masaki Nakamura, Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      IEICE Transactions 91-D(5)

      ページ: 1492-1503

    • 査読あり
  • [雑誌論文] Formal Analysis of the Bakery Protocol with Consideration of Nonatomic Reads and Writes2008

    • 著者名/発表者名
      Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Proc. of the 10th Intl. Conference on Formal Engineering Methods (10th ICFEM) 5256

      ページ: 187-206

    • 査読あり
  • [雑誌論文] Formal digital license language with OTS/CafeOBJ method2008

    • 著者名/発表者名
      Jianwen Xiang, Dines Bjorner, Kokichi Futatsugi
    • 雑誌名

      Proc. of IEEE/ACS Intl. Conference on Computer Systems and Applications

      ページ: 652-660

    • 査読あり
  • [雑誌論文] Simulation-based verification for invariant properties in the OTS/CafeOBJ method2008

    • 著者名/発表者名
      Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Refine 2007, ENTCS 201, Elsevier

      ページ: 127-154

    • 査読あり
  • [雑誌論文] Specification and Verification of Workflows with RBAC Mechanism and SoD Constraints2007

    • 著者名/発表者名
      W. Kong, K. Ogata, K. Futatsugi
    • 雑誌名

      Intl. J. of Software Eng. and Knowledge Eng 17(1)

      ページ: 3-32

    • 査読あり
  • [雑誌論文] On equality predicates in algebraic specification languages2007

    • 著者名/発表者名
      Masaki Nakamura, Kokichi Futatsugi
    • 雑誌名

      Proc. of the 4th International Colloquium on Theoretical Aspects of Computing (ICTAC 2007) 4711

      ページ: 381-395

    • 査読あり
  • [雑誌論文] Modeling and verification of real-time systems based on equations2007

    • 著者名/発表者名
      Kazuhiro Ogata, Kokichi Futatsugi
    • 雑誌名

      Sci. of Comp. Prog 66(2)

      ページ: 162-180

    • 査読あり
  • [学会発表] Verifying Specifications with Proof Scores in CafeOBJ2006

    • 著者名/発表者名
      Kokichi FUTATSUGI
    • 学会等名
      Proc. of 21st IEEE International Conference on Automated Software Engineering
    • 発表場所
      Tokyo
    • 年月日
      2006-02-20
  • [図書] 法令工学の提案(片山卓也)2007

    • 著者名/発表者名
      二木厚吉,緒方和博,有本泰仁
    • 総ページ数
      71-93
    • 出版者
      JAIST
  • [備考] 以下のウェッブページを通じて、開発したシステムと例題、発表論文などを公開している。

    • URL

      http://www.ldl.jaist.ac.jp/cafeobj

URL: 

公開日: 2011-06-18   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi