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

2008 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 20650003
Research Category

Grant-in-Aid for Exploratory Research

Research InstitutionUniversity of Tsukuba

Principal Investigator

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

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

本研究は、モデル検査法を用いたシステム設計検証において、しばしば問題となる「モデル化の誤り(モデリング・エラー)」を発見する手法の研究を行うものである。モデル化に誤りがあるときは、仮にモデル検査器が「検証成功」という結果を出力しても、システム設計が正しいことは保証されないため、これは深刻な問題である。
本研究の中心となるアイディアは、「検証成功」という結果になったときに、モデルの一部を意図的に変更し、「検証失敗」となる限界のモデルを探索することにより、モデリング・エラーの原因を探るというものである。本年度の研究では、まず、モデリング・エラーの事例研究を行い、実際のシステムの設計検証の場面において、どのような誤りがあり得るかについて事例検討を行った。次に、限界モデルを効率的に探索する際に鍵となる技術である多値モデル検査法の性能向上に取り組んだ。その結果、有界モデル検査法を多値モデルに拡張した手法において、探索効率を向上させる符号化法を発見し、実装を行うことができた。この方法では、128値程度の多値モデルに対するモデル検査においても、2値の場合のモデル検査の数倍程度の時間で実行することができるがわかった。これにより、本研究の目的であるモデリング・エラー発見システムの構築にある程度の見通しが立った。

  • Research Products

    (12 results)

All 2009 2008

All Journal Article (9 results) (of which Peer Reviewed: 6 results) Presentation (3 results)

  • [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

    • 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 (掲載決定)

    • Peer Reviewed
  • [Journal Article] An Algebraic Semantics of Predicate Abstraction for PML2009

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

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

    • 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

    • 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

    • 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

  • [Journal Article] 書類の定式化と検証2008

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

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

      Pages: 57-59

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

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

      情報処理 49巻5号

      Pages: 499-505

  • [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

    • Peer Reviewed
  • [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
  • [Presentation] Agda言語について2008

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

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

URL: 

Published: 2010-06-11   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi