セキュアシステム構築のための計算論理的基盤技術の研究

2011 年度 研究成果報告書

• 研究課題/領域番号: 21500136
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 知能情報学
• 研究機関: 名古屋工業大学
• 研究代表者: 世木 博久 名古屋工業大学, 大学院・工学研究科, 教授 (90242908)
• 研究期間 (年度): 2009 – 2011
• キーワード: 計算論理 / 推論アルゴリズム / システム検証 / プログラム変換

研究概要

本研究はシステムやソフトウェアを対象にして,その設計や開発の正当性,妥当性の形式的検証を可能とする計算論理的基盤技術の確立を目的とする.そのための計算論理に基づく方法として,論理プログラムによって対象システムの記述し,プログラム変換技術を用いてその性質を検証するという方法論をとる.次のような3つの研究成果を得た.(1)層状論理プログラムに対する変換において,従来の負の展開規則の条件が誤っていること反例を挙げて示し,これを解決するための新しい負の展開規則を与えた.(2)拡張された負の展開規則を与え,その結果プログラム変換による検証法の適用可能性を拡大させた.(3)余論理プログラ(co-logic programs)に対するプログラム変換規則を与えた.従来知られている検証方法より簡明な検証ができることを示した

研究成果

• [雑誌論文] Proving Properties of Co-ogic Programs by Unfold/Fold Transformations (2012)
  • 著者名/発表者名: H. Seki
  • 雑誌名: Revised Selected Papers, Lecture Notes in Computer Science 巻: LNCS 7225(印刷中) ページ: 205-220
  • 査読あり
• [雑誌論文] On Inductive Proofs by Extended Unfold/fold Transformation Rules (2011)
  • 著者名/発表者名: H. Seki
  • 雑誌名: Revised Selected Papers, Lecture Notes in Computer Science 巻: LNCS 6564 ページ: 117-132
  • 査読あり
• [雑誌論文] On Inductive and Coinductive Proofs via Unfold/fold Transformations (2010)
  • 著者名/発表者名: H. Seki
  • 雑誌名: Revised Selected Papers, Lecture Notes in Computer Science 巻: LNCS 6037 ページ: 82-96
  • 査読あり
• [雑誌論文] On Negative Unfolding in the Answer Set Semantics (2009)
  • 著者名/発表者名: H. Seki
  • 雑誌名: Revised Selected Papers, Lecture Notes in Computer Science 巻: LNCS 5438 ページ: 168-184
  • 査読あり
• [学会発表] Proving Properties of Co-logic Programs by Unfold/fold Transformations (2011)
  • 著者名/発表者名: H. Seki
  • 学会等名: Pre-Proc. of 21st Int' l. Symp. on Logic-Based Program Synthesis and Transformation(LOPSTR2011)
  • 発表場所: Univ. of Southern Denmark
  • 年月日: 2011-07-19
• [学会発表] On Inductive Proofs by Extended Unfold/fold Transformation Rules (2010)
  • 著者名/発表者名: H. Seki
  • 学会等名: Pre-Proc. of the 20th Int' l. Symp. on Logic-Based Program Synthesis and Transformation(LOPSTR2010)
  • 発表場所: RISC-Linz, Report Series
  • 年月日: 2010-07-25
• [学会発表] On Inductive and Coinductive Proofs via Unfold/fold Transformations (2009)
  • 著者名/発表者名: H. Seki
  • 学会等名: Pre-Proc. of 19th Int' l. Symp. on Logic-Based Program Synthesis and Transformation(LOPSTR2009)
  • 発表場所: Univ. of Coimbra
  • 年月日: 2009-09-10