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

2006 Fiscal Year Annual Research Report

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

Research Project

Project/Area Number 16650004
Research InstitutionTohoku University

Principal Investigator

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

Keywords型システム / プログラム解析 / ソフトウェア検証 / モデル検査 / 並行プログラム / 資源使用法解析 / 情報流解析
Research Abstract

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

  • Research Products

    (3 results)

All 2007 2006

All Journal Article (3 results)

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

    • Author(s)
      岩間 太, 五十嵐 淳, 小林直樹
    • Journal Title

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

      Pages: 48-61

  • [Journal Article] A New Type System for Deadlock-Free Processes2006

    • Author(s)
      Naoki Kobayashi
    • Journal Title

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

      Pages: 233-247

  • [Journal Article] Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference2006

    • Author(s)
      Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
    • Journal Title

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

      Pages: 17-26

URL: 

Published: 2008-05-08   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi