• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

型システムとモデル検査の融合によるソフトウェア検証

研究課題

研究課題/領域番号 16650004
研究種目

萌芽研究

配分区分補助金
研究分野 ソフトウエア
研究機関東北大学

研究代表者

小林 直樹  東北大学, 大学院情報科学研究科, 教授 (00262155)

研究期間 (年度) 2004 – 2006
研究課題ステータス 完了 (2006年度)
配分額 *注記
3,500千円 (直接経費: 3,500千円)
2006年度: 1,400千円 (直接経費: 1,400千円)
2005年度: 1,600千円 (直接経費: 1,600千円)
2004年度: 500千円 (直接経費: 500千円)
キーワード型システム / プログラム解析 / ソフトウェア検証 / モデル検査 / 並行プログラム / 資源使用法解析 / 情報流解析 / プログラム検証
研究概要

本研究では,プログラム検証のための代表的な手法である型システム,モデル検査の技術を融合して新しいプログラム検証手法を確立することを目指している.本年度の研究成果は以下のとおり.
・並行プログラムの解析器TyPiCalの改良
従来から研究をすすめてきた,型システムとモデル検査技術を組み合わせた並行プログラムのための検証器TyPiCalを改良し,デッドロックの有無を検証する能力を向上させた.これにより,従来うまく扱えなかった再帰を用いたプロセスのデッドロックフリーダムを自動で検証できるようになった.
・計算資源使用法検証の改良
従来から研究をすすめてきたファイルやメモリ,ネットワークなどの計算資源の使用法を型システムを用いて解析する手法の研究を発展させた.未解決のままとなっていた,型を用いて推論された資源のアクセス順序が,プログラマの宣言した資源の使用法に適合しているかどうかを判定するためのアルゴリズムを考案し,その健全性および完全性を証明した.これにより,計算資源の使用法の検証が全自動で行えるようになった.また,この成果に基づいて,計算資源使用法検証器のプロトタイプを実装し,検証手法の有効性を実証した.
・型とモデル検査の組み合わせによる情報流解析の手法の研究
プログラムが機密情報を漏洩していないことを検証するための新しい手法として,まず型を用いてプログラムを粗く高速に解析し,その解析情報を利用してモデル検査を効率的に行う手法を考案した.これにより,モデル検査のみを使うよりも高速で,型のみによる手法と異なり,情報が漏れる場合の具体例を生成することができる.

報告書

(3件)
  • 2006 実績報告書
  • 2005 実績報告書
  • 2004 実績報告書
  • 研究成果

    (9件)

すべて 2007 2006 2005 2004

すべて 雑誌論文 (9件)

  • [雑誌論文] 計算資源使用法検証における計算資源の仕様と実際の使用法の間の適合性検証アルゴリズム2007

    • 著者名/発表者名
      岩間 太, 五十嵐 淳, 小林直樹
    • 雑誌名

      情報処理学会プログラミング研究会論文誌 48・SIG4

      ページ: 48-61

    • 関連する報告書
      2006 実績報告書
  • [雑誌論文] A New Type System for Deadlock-Free Processes2006

    • 著者名/発表者名
      Naoki Kobayashi
    • 雑誌名

      Proceedings of CONCUR 2006, Springer Lecture Notes in Computer Science 4137

      ページ: 233-247

    • 関連する報告書
      2006 実績報告書
  • [雑誌論文] Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference2006

    • 著者名/発表者名
      Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
    • 雑誌名

      Proceedings of ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS 2006)

      ページ: 17-26

    • 関連する報告書
      2006 実績報告書
  • [雑誌論文] Resource usage analysis for a functional language with exceptions2006

    • 著者名/発表者名
      Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi
    • 雑誌名

      Proceedings of ACM SIGPLAN 2006 Workshop on Partial Evaluation and Program Manipulation (PEPM 2006)

      ページ: 38-47

    • 関連する報告書
      2005 実績報告書
  • [雑誌論文] Resource usage analysis for the pi-calculus2006

    • 著者名/発表者名
      Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
    • 雑誌名

      Verification, Model Checking, and Abstract Interpretation (Proceedings of VMCAI'06) 3855

      ページ: 298-312

    • 関連する報告書
      2005 実績報告書
  • [雑誌論文] Resource Usage Analysis2005

    • 著者名/発表者名
      Atsushi Igarashi, Naoki Kobayashi
    • 雑誌名

      ACM Transactions on Programming Languages and Systems 27・2(出版予定)

    • 関連する報告書
      2004 実績報告書
  • [雑誌論文] 例外機構を備えた言語のための資源使用法解析2005

    • 著者名/発表者名
      岩間 太, 五十嵐 淳, 小林 直樹
    • 雑誌名

      第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)論文集 (印刷中)

    • 関連する報告書
      2004 実績報告書
  • [雑誌論文] Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes2004

    • 著者名/発表者名
      Reynald Affeldt, Naoki Kobayashi
    • 雑誌名

      Proceedings of 11^<th> International Workshop on Expressiveness in Concurrency (EXPRESS 2004)

      ページ: 113-127

    • 関連する報告書
      2004 実績報告書
  • [雑誌論文] Region-Based Memory Management for a Dynamically-Typed Language2004

    • 著者名/発表者名
      A.Nagata, N.Kobayashi, A.Yonezawa
    • 雑誌名

      Proceedings of APLAS' 04, Springer LNCS 3302

      ページ: 229-245

    • NAID

      130004638815

    • 関連する報告書
      2004 実績報告書

URL: 

公開日: 2004-04-01   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi