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

Advanced methods of design and verification for dynamically reconfigurable embedded systems

Research Project

Project/Area Number 24500034
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Research Field Software
Research InstitutionKanazawa University

Principal Investigator

YAMANE Satoshi  金沢大学, 電子情報学系, 教授 (70263506)

Project Period (FY) 2012-04-01 – 2015-03-31
Project Status Completed (Fiscal Year 2014)
Budget Amount *help
¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000)
Fiscal Year 2014: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2013: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2012: ¥2,600,000 (Direct Cost: ¥2,000,000、Indirect Cost: ¥600,000)
Keywords組込みシステム / ハイブリッドオートマトン / モデル検査 / 抽象化精錬 / 仕様記述 / 形式的検証 / 動的再構成可能システム / CEGAR / 動的再構成 / 動的再構成可能組込みシステム / 動的ハイブリッドオートマトン / 検証器 / ハイブリッドシステム
Outline of Final Research Achievements

A system which can changes its configuration during operations is called Dynamically Reconfigurable System. In a Dynamically reconfigurable system, software (CPU) and hardware (DRP(Dynamically Reconfigurable Processor)) behaves cooeratively.
In this study, we develop dynamic hybrid automata, and CEGAR(CounterExample-Guided Abstraction Refinement) based model checking. Also we develop our model checker based on our proposed methods, and show them effective.

Report

(4 results)
  • 2014 Annual Research Report   Final Research Report ( PDF )
  • 2013 Research-status Report
  • 2012 Research-status Report
  • Research Products

    (20 results)

All 2015 2014 2013 2012

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

  • [Journal Article] 線形ハイブリッドオートマタのCEGARを適用したSMTベースモデル検査2015

    • Author(s)
      冨坂征平,柳瀬龍,櫻井孝平,山根智
    • Journal Title

      IEICE Techniacal Report

      Volume: 114(493) Pages: 47-52

    • Related Report
      2014 Annual Research Report
  • [Journal Article] 組込みアセンブリプログラムからのモデル抽出による記号モデル検査2015

    • Author(s)
      加藤友紀,公下亮佑,櫻井孝平,山根 智
    • Journal Title

      IEICE Techniacal Report

      Volume: 114(493) Pages: 65-70

    • Related Report
      2014 Annual Research Report
  • [Journal Article] Development of SMT-Based Bounded Model Checker for Embedded Assembly Program2014

    • Author(s)
      J.Kobashi, A.Takeshita, S.Yamane
    • Journal Title

      IEEE 3rd Global Conference on Consumer Electronics

      Volume: 3 Pages: 1-3

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Model Generation by the Exhaustive Search for Embedded Assembly Programs and Application to Model Checking2014

    • Author(s)
      R.Konoshita, S. Yamane, K.Sakurai
    • Journal Title

      IEEE 3rd Global Conference on Consumer Electronics

      Volume: 3 Pages: 1-4

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] Development of Probabilistic Timed CEGAR2014

    • Author(s)
      S.Yamane,T.Shimizu
    • Journal Title

      IEEE International Conference on Systems and Informatics

      Volume: 2 Pages: 482-491

    • NAID

      120005593945

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 組込みアセンブリプログラムのモデル構築によるモデル検査2014

    • Author(s)
      公下亮佑,山根 智,櫻井孝平
    • Journal Title

      組込みシステムシンポジウム(ESS2014)

      Volume: ESS2014 Pages: 1-10

    • NAID

      170000087146

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] 組込みアセンブリプログラム解析によるSMTモデル検査2014

    • Author(s)
      小橋潤平,山根 智,竹下 淳
    • Journal Title

      組込みシステムシンポジウム(ESS2014)

      Volume: ESS2014 Pages: 1-6

    • NAID

      170000087147

    • Related Report
      2014 Annual Research Report
    • Peer Reviewed
  • [Journal Article] AspectJを用いたFault-InjectionによるHadoop MapReduceの耐故障処理に関する性能評価2014

    • Author(s)
      中川洋介,櫻井孝平,清水裕亮,山根智
    • Journal Title

      情報処理学会論文誌コンピューティングシステム(ACS)

      Volume: 7(1) Pages: 35-45

    • NAID

      110009687724

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] 動的再構成可能システムの仕様記述言語の提案およびその検証実験2013

    • Author(s)
      山田 英史, 中居 祐輝, 山根 智
    • Journal Title

      情報処理学会論文誌 プログラミング(PRO)

      Volume: 6(3) Pages: 1-19

    • NAID

      110009656443

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] Development of Model Checker of Dynamic Linear Hybrid Automata2013

    • Author(s)
      Ryo Yanase, T. Sakai, M. Sakai, S. Yamane
    • Journal Title

      IEEE 37th COMPSAC

      Volume: 37 Pages: 1-2

    • NAID

      120005418465

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] Hanoi: 複数レイヤーのトレースログを用いたHadoopのパフォーマンス解析2013

    • Author(s)
      清水 裕亮,櫻井 孝平,山根 智
    • Journal Title

      第25回 コンピュータシステム・シンポジウム (ComSys 2013)

      Volume: 25 Pages: 54-63

    • NAID

      170000079166

    • Related Report
      2013 Research-status Report
    • Peer Reviewed
  • [Journal Article] 確率時間CEGARの開発とその実証実験2012

    • Author(s)
      清水隆也,森下篤,山根 智
    • Journal Title

      情報処理学会論文誌 プログラミング(PRO)

      Volume: 5(2)

    • NAID

      40019257054

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] 確率線形ハイブリッドオートマトンの到達可能性検証2012

    • Author(s)
      畠中克也,山根 智
    • Journal Title

      情報処理学会論文誌

      Volume: 53(12) Pages: 2671-2681

    • NAID

      110009493416

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] Trace-mining Profile for Large-Scale Distributed Framework Hadoop2012

    • Author(s)
      Y.Shimizu, K.Sakurai, S.Yamane
    • Journal Title

      The 18th IEEE Pacific Rim International Symposium on Dependable Computing

      Volume: 18 Pages: 1-2

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] A New Approach to Specify and Verify Embedded Systems consisting of CPU and DRP2012

    • Author(s)
      R.Yanase, T.Sakai, M.Sakai, S.Yamane
    • Journal Title

      The 18th IEEE Pacific Rim International Symposium on Dependable Computing

      Volume: 18 Pages: 1-2

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] 組込みアセンブラのSMT検証の理論と実験2012

    • Author(s)
      竹下淳,小橋潤平,山根 智
    • Journal Title

      組込みシステムシンポジウム2012(ESS2012)

      Volume: 2012 Pages: 197-202

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] トレースを用いた大規模分散基盤 Hadoop 向けのプロファイル手法の提案2012

    • Author(s)
      清水 裕亮,櫻井 孝平,山根 智
    • Journal Title

      第24回 コンピュータシステム・シンポジウム (ComSys 2012)

      Volume: 24 Pages: 70-78

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] Javaによる確率時間CEGAR検証器の実装と検証実験2012

    • Author(s)
      長谷川 尭志, 小池 脩平, 清水 隆也, 山根 智
    • Journal Title

      第10回 ディペンダブルシステムワークショップ (DSW 2012)

      Volume: DSW 2012 Pages: 1-12

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Journal Article] 動的再構成可能組込みシステムのモデル化と仕様記述2012

    • Author(s)
      柳瀬 龍, 酒井 辰典, 酒井 誠, 山根 智
    • Journal Title

      第10回 ディペンダブルシステムワークショップ (DSW 2012)

      Volume: DSW 2012 Pages: 1-4

    • NAID

      110007099107

    • Related Report
      2012 Research-status Report
    • Peer Reviewed
  • [Presentation] 動的組込みシステムの仕様記述言語の開発2013

    • Author(s)
      山根 智,酒井誠
    • Organizer
      信学技報113(279)
    • Place of Presentation
      岩手県
    • Related Report
      2013 Research-status Report

URL: 

Published: 2013-05-31   Modified: 2019-07-29  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi