型システムとモデル検査の融合によるソフトウェア検証
| Project/Area Number |
16650004
|
|---|
| Research Category |
Grant-in-Aid for Exploratory Research
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Tohoku 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)
Research Products
(9 results)
