• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2009 Fiscal Year Annual Research Report

多値モデル検査法を用いたモデリング・エラーの発見

Research Project

Project/Area Number 20650003
Research InstitutionUniversity of Tsukuba

Principal Investigator

亀山 幸義  University of Tsukuba, 大学院・システム情報工学研究科, 教授 (10195000)

Co-Investigator(Kenkyū-buntansha) 木下 佳樹  (独)産業技術総合研究所, システム検証研究センター, センター長 (60356889)
西澤 弘樹  鳥取環境大学, 環境情報学部, 講師 (60455433)
Keywords多値モデル検査 / システム検証 / モデル化 / 状態遷移系 / 安全性検証 / 抽象化 / 延焼
Research Abstract

本研究は、モデル検査法を用いたシステム設計検証において、しばしば問題となる「モデル化の誤り(モデリング・エラー)」を発見する手法の研究を行うものである。モデル化に誤りがあるときは、仮にモデル検査器が「検証成功」という結果を出力をしても、システム設計が正しいことは保証されないため、これは深刻な問題である。
本研究の中心となるアイディアは、「検証成功」という結果になったときに、モデルの一部を意図的に変更し、「検証失敗」となる限界モデルを探索することにより、モデリング・エラーの原因を探るというものである。今年度の研究では、昨年度の研究で構築した多値モデル検査のアルゴリズムを改良し、Quasi-Boolean Algebraに適用できるようにした。また、多値モデル検査の理論的基礎について、従来手法を一般化した定式化とそれに対するシミュレーション定理を証明し、多値モデル検査の効率化に対して理論的根拠を与えることに成功した。さらに、昨年度のアルゴリズムに対して実装上の改良をおこない、いくつかの具体例に対して、モデリング・エラーの発見を行う実験を行い、一定の条件のもとでは、本研究の手法で効率的なモデリング・エラー発見が可能であることがわかった。これらについては、後日、成果をまとめた論文を発表する予定である。関連研究として、「検証失敗からの情報の取得」という点で類似している型推論アルゴリズムにおける型エラーについての考察を行い、より良い失敗情報の取得を行うためのアルゴリズムの設計、開発を行った。

  • Research Products

    (6 results)

All 2010 2009

All Journal Article (5 results) (of which Peer Reviewed: 5 results) Presentation (1 results)

  • [Journal Article] Agate-an Agda-to-Haskell compiler2009

    • Author(s)
      尾崎弘幸、武山誠、木下佳樹
    • Journal Title

      コンピュータソフトウェア 26-4

      Pages: 107-119

    • Peer Reviewed
  • [Journal Article] A simple type-theoretic language : Mini-TT2009

    • Author(s)
      T.Coquand, 木下佳樹, B.Nordstrom, M.Takeyama
    • Journal Title

      From Semantics to Computer Science, Cambridge University Press

      Pages: 139-164

    • Peer Reviewed
  • [Journal Article] Multirelational models of lazy, monodic tree, and probabilitstic Kleene algebras2009

    • Author(s)
      H.Furusawa, K.Nishizawa, N.Tsumagari
    • Journal Title

      Bulletin of Informatics and Cybernetics 41

      Pages: 11-24

    • Peer Reviewed
  • [Journal Article] The cube of Kleene algebras and the triangular prism of multirelations2009

    • Author(s)
      K.Nishizawa, N.Tsumagari, H.Furusawa
    • Journal Title

      Relations and Kleene Algebra in Computer Science RelMiCS/AKA(Springer LNCS) 5827

      Pages: 276-290

    • Peer Reviewed
  • [Journal Article] Multi-valued modal fixed point logics for model checking2009

    • Author(s)
      K.Nishizawa
    • Journal Title

      Proc.Int'l Symp.On Multiple-valued Logics, IEEE CS Press

      Pages: 109-113

    • Peer Reviewed
  • [Presentation] Improving Error Message in Type System2010

    • Author(s)
      C.Kustanto, Y.Kameyama
    • Organizer
      情報処理学会プロゲラミング研究会
    • Place of Presentation
      電気通信大学
    • Year and Date
      2010-03-16

URL: 

Published: 2011-06-16   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi