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

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

Research Project

Project/Area Number 16650004
Research Category

Grant-in-Aid for Exploratory Research

Allocation TypeSingle-year Grants
Research Field Software
Research InstitutionTohoku University

Principal Investigator

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

Project Period (FY) 2004 – 2006
Project Status Completed (Fiscal Year 2006)
Budget Amount *help
¥3,500,000 (Direct Cost: ¥3,500,000)
Fiscal Year 2006: ¥1,400,000 (Direct Cost: ¥1,400,000)
Fiscal Year 2005: ¥1,600,000 (Direct Cost: ¥1,600,000)
Fiscal Year 2004: ¥500,000 (Direct Cost: ¥500,000)
Keywords型システム / プログラム解析 / ソフトウェア検証 / モデル検査 / 並行プログラム / 資源使用法解析 / 情報流解析 / プログラム検証
Research Abstract

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

Report

(3 results)
  • 2006 Annual Research Report
  • 2005 Annual Research Report
  • 2004 Annual Research Report
  • Research Products

    (9 results)

All 2007 2006 2005 2004

All Journal Article (9 results)

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

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

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

      Pages: 48-61

    • Related Report
      2006 Annual Research Report
  • [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

    • Related Report
      2006 Annual Research Report
  • [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

    • Related Report
      2006 Annual Research Report
  • [Journal Article] Resource usage analysis for a functional language with exceptions2006

    • Author(s)
      Futoshi Iwama, Atsushi Igarashi, Naoki Kobayashi
    • Journal Title

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

      Pages: 38-47

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Resource usage analysis for the pi-calculus2006

    • Author(s)
      Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
    • Journal Title

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

      Pages: 298-312

    • Related Report
      2005 Annual Research Report
  • [Journal Article] Resource Usage Analysis2005

    • Author(s)
      Atsushi Igarashi, Naoki Kobayashi
    • Journal Title

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

    • Related Report
      2004 Annual Research Report
  • [Journal Article] 例外機構を備えた言語のための資源使用法解析2005

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

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

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Partial Order Reduction for Verification of Spatial Properties of Pi-Calculus Processes2004

    • Author(s)
      Reynald Affeldt, Naoki Kobayashi
    • Journal Title

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

      Pages: 113-127

    • Related Report
      2004 Annual Research Report
  • [Journal Article] Region-Based Memory Management for a Dynamically-Typed Language2004

    • Author(s)
      A.Nagata, N.Kobayashi, A.Yonezawa
    • Journal Title

      Proceedings of APLAS' 04, Springer LNCS 3302

      Pages: 229-245

    • NAID

      130004638815

    • Related Report
      2004 Annual Research Report

URL: 

Published: 2004-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi