関数型言語系とグリッド環境上のプルーフチェッカを融合した超並列演算器の設計検証法

• 研究課題/領域番号: 20500130
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 知能情報学
• 研究機関: 信州大学
• 研究代表者: 和崎 克己 信州大学, 工学部, 教授 (70271492)
• 研究期間 (年度): 2008 – 2010
• 研究課題ステータス: 完了 (2010年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2010年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2009年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円); 2008年度: 2,080千円 (直接経費: 1,600千円、間接経費: 480千円)
• キーワード: 探索・論理・推論アルゴリズム / プルーフチェッカ / 形式検証 / 関数型言語系 / グリッド計算機 / 設計検証系 / 並列演算器

研究概要

プルーフチェッカ(Proof Checker)を,ネットワーク環境上へ実装し,並列システムの検証能力の向上を図る.対象回路の構成情報は,関数型言語系の上で記述し,コンパイラ出力として,プルーフチェッカへの証明式の列を得る.並列性実現のため「パイプライン機構」を説明する計算モデルとして,ペトリネット表現モデルを導入した.次に,関数型言語系上のハードウェアコンパイラを開発した.更に検証済み演算器の形式検証を実施した.

研究成果

• [雑誌論文] Development and Evaluation of a Long-range 300-m Leaky Coaxial Cab le in the 2.4-GHz Band for IEEE 802.11 b/g Wireless Network Access (2011)
  • 著者名/発表者名: Masayuki NAKAMURA, et al.
  • 雑誌名: IEEJ Transactions on Electrical and Electronic Engmeering 巻: 6(1) ページ: 37-45
  • 査読あり
• [雑誌論文] Development and evaluation of a large-scale agent-based system for coll ecting results of information literacy learning using electronic textbooks (2010)
  • 著者名/発表者名: Keiichi TANAKA, Katsumi WASAKI
  • 雑誌名: Proceedings of Society for Information Technology, Teacher Education Int'l Conference 2010 巻: 1 ページ: 3191-3196
  • NAID: 130007420833
  • 査読あり
• [雑誌論文] 静的解析によるマルウェアの分類と結果の検討 (2010)
  • 著者名/発表者名: 岩本一樹, 和崎克己
  • 雑誌名: 情報処理学会マルチメディア・分散・協調とモバイル(DICOMO2010)シンポジウム論文集 巻: 1(C-002) ページ: 371-374
  • 査読あり
• [雑誌論文] Quantum Circuits, Lots, Interference and Basis of Neuro-Computations (2009)
  • 著者名/発表者名: Hiroyuki MATSUURA, Masahiro NAKANO, Katsumi WASAKI
  • 雑誌名: ICIC Express Letters, ICIC International 3,(1) ページ: 7-14
  • 査読あり
• [雑誌論文] A Practice of Smart Sensing System for Buried Mines Detecting based on Active Infrared Thermography Approach (2009)
  • 著者名/発表者名: Katsumi WASAKI, Nobuhiro SHIMOI
  • 雑誌名: International Journal of Computational Intelligence : Theory and Practice 4(1) ページ: 29-37
  • 査読あり
• [雑誌論文] Development and evaluation of a large-scale agent-based system for collecting results of information literacy learning using electronic textbooks (2009)
  • 著者名/発表者名: Keiichi TANAKA, Katsumi WASAKI
  • 雑誌名: Proceedings of Society for Information Technology & Teacher Education International Conference SITE2010 ページ: 3191-3196
  • NAID: 130007420833
  • 査読あり
• [雑誌論文] 静的解析によるマルウェアのAPI推移の抽出とクラスタ解析 (2009)
  • 著者名/発表者名: 岩本一樹, 和崎克己
  • 雑誌名: コンピュータセキュリティシンポジウム2009 CSS2009 ページ: 361-366
  • NAID: 170000066076
• [雑誌論文] A Meta Hardware Description Language Melasy for Model-Checking Systems (2008)
  • 著者名/発表者名: Naoki IWASAKI, Katsumi WASAKI
  • 雑誌名: Proceedings of the 5th International Conference on Information Technology : New Generations (ITNG2008) ページ: 273-278
  • 査読あり
• [雑誌論文] Correctness of the Stability of the 4-2 Compressor Cell for Partial Product Reduction in Parallel Multiplier Circuits (2008)
  • 著者名/発表者名: Katsumi WASAKI
  • 雑誌名: Mechanized Mathematics and Its Applications 7,(2) ページ: 17-25
  • 査読あり
• [雑誌論文] Stability of the 4-2 Binary Addition Circuit Cells.Part I (2008)
  • 著者名/発表者名: Katsumi WASAKI
  • 雑誌名: Formalized Mathematics 16,(4) ページ: 377-387
  • 査読あり
• [雑誌論文] Stability of n-Bit Generalized Full Adder Circuits (GFAs). Part II (2008)
  • 著者名/発表者名: Katsumi WASAKI
  • 雑誌名: Formalized Mathematics 16,(1) ページ: 73-80
  • 査読あり
• [雑誌論文] A Meta Hardware Description Language Melasy for Model-Checking Systems (2008)
  • 著者名/発表者名: Naoki IWASAKI, Katsumi WASAKI
  • 雑誌名: Proc. of the 5th Int. Conf. on Info. Technology : New Generations (ITNG2008) MC1 ページ: 273-278
  • 査読あり
• [雑誌論文] Stability of n-bit Generalized Full Adder Circuits (GFAs). Part II (2008)
  • 著者名/発表者名: Katsumi WASAKI
  • 雑誌名: Formalized Mathematics 16(1) ページ: 73-78
  • 査読あり
• [雑誌論文] Stability of the 4-2 Binary Addition Circuit Cells (2008)
  • 著者名/発表者名: Katsumi WASAKI
  • 雑誌名: Formalized Mathematics 16(4) ページ: 385-395
  • 査読あり
• [学会発表] Automatic Code Generation and Integrated Testing for Model Checking and Hardware Implementation using A Meta Description Language : Melasy+ (2010)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: 平成22年度IEEE信越支部セッション講演論文集,(11B-4),206
  • 発表場所: 長岡技術科学大学
  • 年月日: 2010-10-02
• [学会発表] Upper Scalable Modeling of The Stream Processing Architecture by using A Specification Language : LOTOS (2010)
  • 著者名/発表者名: Pratima K.SHAH, Katsumi WASAKI
  • 学会等名: 平成22年度IEEE信越支部セッション講演論文集,(11B-2),204
  • 発表場所: 長岡技術科学大学
  • 年月日: 2010-10-02
• [学会発表] 上位ハードウェア設計言語Melasy+によるVHDLコード生成と動作検証 (2010)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: FIT2010(第9回情報科学技術フォーラム)講演論文集,1,(C-002),371-374
  • 発表場所: 九州大学伊都キヤンハス
  • 年月日: 2010-09-08
• [学会発表] 上位ハードウェア設計言語Melasy+によるVHDLコード生成と動作検証 (2010)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: FIT2010(第9回情報科学技術フォーラム)講演論文集
  • 発表場所: 九州大学伊都キャンパス
  • 年月日: 2010-09-08
• [学会発表] 上位言語Melasy+による自己テスト機能付バスアービタの設計とNuSMVを用いた検証 (2010)
  • 著者名/発表者名: 花里貴裕, 白鳥航亮, 和崎克己
  • 学会等名: 情報処理学会第72回全国大会講演論文集,1,(1M-4),151-152
  • 発表場所: 東京大学本郷キャンパス
  • 年月日: 2010-03-10
• [学会発表] 上位ハードウェア記述言語Melasy+に対する仕様パターン埋め込みと展開 (2010)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: 情報処理学会第72回全国大会講演論文集,1,(1M-3),149-150
  • 発表場所: 東京大学本郷キャンパス
  • 年月日: 2010-03-10
• [学会発表] 時間ペトリネットを用いた非同期論理ゲートのモデルと階層化同路合成 (2009)
  • 著者名/発表者名: 松山千尋, 和崎克己
  • 学会等名: 平成21年度電子情報通信学会信越支部大会講演論文集,(2D-3),38
  • 発表場所: 信州大学長野(工学)キャンパス
  • 年月日: 2009-10-03
• [学会発表] HDCamlハードウェア上位記述に対するLOTOSコード生成系について (2009)
  • 著者名/発表者名: 桑島芳朗, 和崎克己
  • 学会等名: 平成21年度電子情報通信学会信越支部大会講演論文集,(2B-4),29
  • 発表場所: 信州大学長野(工学)キャンパス
  • 年月日: 2009-10-03
• [学会発表] 上位記述言語Melasy+を用いたセル型FIFOメモリの自己同復性の検証 (2009)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: 平成21年度電子情報通信学会信越支部大会講演論文集,(2B-3),28
  • 発表場所: 信州大学長野(工学)キャンパス
  • 年月日: 2009-10-03
• [学会発表] Time-Petri Netを用いた非同期同路のモデル化と階層化設計 (2009)
  • 著者名/発表者名: 松山千尋, 和崎克己
  • 学会等名: FIT2009(第8回情報科学技術フォーラム)講演論文集,1,(C-038),523-526
  • 発表場所: 東北工業大学八木山キャンパス
  • 年月日: 2009-09-04
• [学会発表] 上位ハードウェア設計言語Melasy+による自己回復機能付きFIFOメモリの記述と検証 (2009)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: FIT2009(第8回情報科学技術フォーラム)講演論文集,1,(C-011),451-454
  • 発表場所: 東北工業大学八木山キャンパス
  • 年月日: 2009-09-03
• [学会発表] 上位ハードウェア設計言語Melasy+による自己回復機能付きFIFOメモリの記述と検証 (2009)
  • 著者名/発表者名: 白鳥航亮, 和崎克己
  • 学会等名: FIT2009(第8回情報科学技術フォーラム)
  • 発表場所: 東北工業大学
  • 年月日: 2009-09-02
• [学会発表] 整数有限列上の加算・乗算アルゴリズムの正当性証明に関する検討 (2009)
  • 著者名/発表者名: 伊藤比佐志, 和崎克己
  • 学会等名: 日本Mizar学会2009年春期総会予稿集(Proceedings of the Technical Symposium and General Assembly of Mizar JAPAN),4,(1),6pages
  • 発表場所: 信州大学長野(工学)キャンパス総合研究棟
  • 年月日: 2009-06-19
• [学会発表] モデル検査に対応する上位ハードウェア記述言語MelasyのVHDLコード生成 (2009)
  • 著者名/発表者名: 野村達雄, 岩崎直木, 和崎克己
  • 学会等名: 情報処理学会第71回全国大会講演論文集,1,(2L-2),171-172
  • 発表場所: 立命館大学びわこ・くさつキャンパス
  • 年月日: 2009-03-11
• [学会発表] モデル検査に対応する上位ハードウェア記述言語MelasyとXML中間表現 (2009)
  • 著者名/発表者名: 岩崎直木, 野村達雄, 和崎克己
  • 学会等名: 情報処理学会第71回全国大会講演論文集,1,(2L-1),169-170
  • 発表場所: 立命館大学びわこ・くさつキヤンパス
  • 年月日: 2009-03-11
• [学会発表] モデル検査に対応する上位ハードウェア記述言語MelasyとXML中間表現 (2009)
  • 著者名/発表者名: 岩崎直木, 野村達雄, 和崎克己
  • 学会等名: 情報処理学会第71回全国大会
  • 発表場所: 立命館大学くさつキャンパス
  • 年月日: 2009-03-10
• [備考] ホームページ等
• [備考] 信州大学研究者総覧
  • URL: http://soar-rd.shinshu-u.ac.jp/profile/ja.gCnejaTN.html#books_articles_etc
• [備考] Mizar Proof Checking System
  • URL: http://markup.cs.shinshu-u.ac.jp/mirror/mizar/
• [備考] Formalized Mathematics(論文誌)
  • URL: http://versita.metapress.com/content/121073/
• [備考]
  • URL: http://soar-rd.shinshu-u.ac.jp/profile.do?lng=ja&id=gcnejaTN#books_articles_etc
• [備考]
  • URL: http://soar-rd.shinshu-u.ac.jp/soar/profile.do?Ing=ja&id=gCnejaTN#books_articles_etc
• [備考]
  • URL: http://soar-rd.shinshu-u.ac.jp/soar/profile.do?lng=ja&id=gcnejaTN#books_articles_etc