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

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

Research Project

Project/Area Number 20650003
Research Category

Grant-in-Aid for Challenging Exploratory Research

Allocation TypeSingle-year Grants
Research Field Software
Research InstitutionUniversity of Tsukuba

Principal Investigator

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

Co-Investigator(Kenkyū-buntansha) 木下 佳樹  (独)産業技術総合研究所, システム検証研究センター, センター長 (60356889)
西澤 弘樹 (西澤 弘毅)  鳥取環境大学, 環境情報学部, 講師 (60455433)
Project Period (FY) 2008 – 2009
Project Status Completed (Fiscal Year 2009)
Budget Amount *help
¥3,000,000 (Direct Cost: ¥3,000,000)
Fiscal Year 2009: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2008: ¥1,700,000 (Direct Cost: ¥1,700,000)
Keywords多値モデル検査 / システム検証 / モデル化 / 状態遷移系 / 安全性検証 / 抽象化 / 延焼
Research Abstract

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

Report

(2 results)
  • 2009 Annual Research Report
  • 2008 Annual Research Report
  • Research Products

    (18 results)

All 2010 2009 2008

All Journal Article (14 results) (of which Peer Reviewed: 11 results) Presentation (4 results)

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

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

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

      Pages: 107-119

    • NAID

      130004549149

    • Related Report
      2009 Annual Research Report
    • 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

    • Related Report
      2009 Annual Research Report
    • 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

    • Related Report
      2009 Annual Research Report
    • 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

    • Related Report
      2009 Annual Research Report
    • 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

    • NAID

      10027364398

    • Related Report
      2009 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Shifting the Stage-Staging with Delimited Control2009

    • Author(s)
      Y. Kameyama, O. Kiselyov, C.-c. Sha
    • Journal Title

      Proc. Workshop on Partial Evaluation and Program Manipulation

      Pages: 111-120

    • NAID

      120007137184

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Multirelational Models of Lazy, Monodic Tree, and Probabilistic Kleene Algebra2009

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

      Bulletin of Informatics and Cybernetics (掲載決定)

    • NAID

      120003878376

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] An Algebraic Semantics of Predicate Abstraction for PML2009

    • Author(s)
      Y. Kinoshita, K. Nishizawa
    • Journal Title

      コンピュータソフトウェア (掲載決定)

    • NAID

      130004892130

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] A Direct Algorithm for Multi-Valued Bounded Model Checklng2008

    • Author(s)
      J. O. Andrade, Y. Kameyama
    • Journal Title

      Proc. Int'l Symp. on Automated Technology for Verification & Analysis, LNCS 5311

      Pages: 80-94

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Strong Normalization of Polymorphic Calculus for Delimited Continuatoins2008

    • Author(s)
      Y. Kameyama, K. Asai
    • Journal Title

      Proc. Workshop on Symbolic Computation in Software Science, RISC-LINZ report 08-08

      Pages: 96-108

    • Related Report
      2008 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Formalization of System LSI Specification and Automatic Generation of Verification Items2008

    • Author(s)
      Y. Kinoshita et al.
    • Journal Title

      TESTCOM/FATES2008, Supplementary Proceedings

      Pages: 75-76

    • Related Report
      2008 Annual Research Report
  • [Journal Article] 書類の定式化と検証2008

    • Author(s)
      木下佳樹
    • Journal Title

      第6回ディペンダブルシステムワークショップ論文集

      Pages: 57-59

    • Related Report
      2008 Annual Research Report
  • [Journal Article] フォーマルメソッドのフィールドワーク2008

    • Author(s)
      木下佳樹、高井利憲、大崎人士
    • Journal Title

      情報処理 49巻5号

      Pages: 499-505

    • Related Report
      2008 Annual Research Report
  • [Journal Article] A Non-Probablllstlc Relational Model of Probabilistic Kleene Algebras2008

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

      Proc. Relations and Kleene Algebra in Computer Science, LNCS 4988

      Pages: 110-122

    • Related Report
      2008 Annual Research Report
    • 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
    • Related Report
      2009 Annual Research Report
  • [Presentation] Improving Multi-Valued Bounded Model Checking2008

    • Author(s)
      J. O. Andrade, Y. Kameyama
    • Organizer
      日本ソフトウェア科学会第25回大会
    • Place of Presentation
      筑波大学
    • Year and Date
      2008-09-12
    • Related Report
      2008 Annual Research Report
  • [Presentation] Agda言語について2008

    • Author(s)
      木下佳樹
    • Organizer
      日本ソフトウェア科学会第25回大会
    • Place of Presentation
      筑波大学
    • Year and Date
      2008-09-12
    • Related Report
      2008 Annual Research Report
  • [Presentation] 二項多重関係の反射的推移的閉包2008

    • Author(s)
      津曲起宏、西澤弘毅、古澤仁
    • Organizer
      日本ソフトウェア科学会第25回大会
    • Place of Presentation
      筑波大学
    • Year and Date
      2008-09-11
    • Related Report
      2008 Annual Research Report

URL: 

Published: 2008-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi