研究紹介詳細表示

～バグのないセキュアなシステム開発を目指して～

計算論理に基づくプログラム推論方式の研究

研究分野分類：1204 知能情報学
産業分類：その他の製造業
キーワード：探索・論理・推論アルゴリズム，プログラム理論，仕様記述・検証，プログラム推論，プログラム変換
情報学
人間情報学
世木博久（情報工学専攻 ）
研究概要
　ソフトウェアは様々なシステムを運用する社会基盤であり、その正当性を保証することが不可欠です。プログラムの持つ性質を推論できれば、その仕様との違いを分析して誤り(バグ)が発見できます。このようなソフトウェアの形式的検証を可能にする計算論理技術に基づいたソフトウェア検証の方法論を構築することを目的にしています。		 特徴
　特に、リアクティブ・システムを対象として、従来の有限項のみならず無限項を扱うプログラム変換技術を用いた検証方式を研究しています。
背景・従来技術
　従来のシステム検証の方式としてはモデル検査がありますが、無限状態システムの扱いや仕様表現が本質的に命題論理式に制限されており、システムの構造的性質などの自然な表現が難しいことがあります。		 実用化イメージ
「プログラム推論の理論」を研究しており、プログラミング言語や推論における数理的方法について理解することを目的としています。一方で、 プログラム推論理論を基盤として、誤りのないプログラミングを実現するというような実用的な貢献につながります。

企業等への提案

研究者からのメッセージ
　システムにはソフトウェアが必ず組み込まれ運用されており、その信頼性、安全性を保証することはますます重要になっています。計算論理のような情報科学で蓄積された知見をこの分野に適用することを目指しています。

文献・特許
・H. Seki, Proving Properties of Co-logic Programs by Unfold/Fold Transformations, Lecture Notes in Computer Science, 7225, Springer, pp. 205-220, 2012.
・H. Seki, Extending Co-logic Programs for Branching-Time Model Checking, Proc. 23rd Int’l. Symp. on Logic-based
・Program Synthesis and Transformation (LOPSTR 2013), 採録決定．

試作品状況 無し 掲示可 提供可

 

利用可能な設備・装置
形式的手法を用いたソフトウェア開発技法		 共同研究を希望するテーマ
研究者データベースとのリンク（名前をクリックしてください）
研究者名：世木博久
ＰＤＦ表示と印刷