2004 Fiscal Year Annual Research Report
型システムとモデル検査の融合によるソフトウェア検証
| Project/Area Number |
16650004
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
|
|---|
| Keywords | 型システム / プログラム検証 / プログラム解析 / モデル検査 |
|---|
| Research Abstract |
本研究では、プログラム検証のための代表的な手法である型システム、モデル検査の技術を融合して新しいプログラム検証手法を確立することを目指している.本年度の研究成果は以下のとおり.
1.並行プログラムの解析器TyPiCalの実装
従来から研究をすすめてきた並行プログラムのための型システムに基づくプログラム検証器TyPiCalを実装した.その際、実装の一部に実現にBDD (Boolean decision diagram)に基づくモデル検査が有用であることが確かめられた。
2.計算資源使用法解析の拡張
従来から研究をすすめてきたファイルやメモリ、ネットワークなどの計算資源の使用法を型システムを用いて解析する手法の研究を発展させた.未解決のままとなっていた、推論された使用方法がプログラマの仕様に適合しているかどうかを判定する問題について検討し、正規表現で表される仕様法については一種のモデル検査の問題に還元できることを発見した,さらに、解析の対象言語をこれまでの純粋な関数型言語から例外処理機構を備えた言語へと拡張し、それにあわせて解析のための型システムの拡張を行った.
3.並行プログラムの検証手法の研究
並行プログラムがspatial logicで記述された仕様を満たすことをモデル検査のような状態探索によって検証する際に、探索スペースを減少させるためのpartial order reductionと呼ばれる手法の研究を行った.partial order reductionはモデル検査でよく用いられる手法であるが、それが適用可能であるための十分条件を型を用いて検証できるという見通しが得られた.
|
Research Products
(4 results)
