2010 Fiscal Year Annual Research Report
リアルタイムソフトウェアのコンポジショナルな処理モデルとその構造検証
| Project/Area Number |
20500030
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小野 諭 工学院大学, 情報工学部, 教授 (90407164)
|
|---|
| Keywords | リアルタイムソフトウェア / 非同期処理 / 構造検証 / モデル検査 |
|---|
| Research Abstract |
研究代表者(小川)はリアルタイムソフトウェア構造検証のための基礎技術として、1.重み付プッシュダウンモデル検査の漸増的アルゴリズム、2.シングルCPU上のマルチスレッドの割込み処理モデル化について研究を進めた。前者はモデル検査の手法で問題になるメモリオーヴァーフローの抑制に大きな効果がある。漸増的アルゴリズムのアイデア・実装は昨年度に既に得ていたが、漸増的収束判定の正しさについて確信が得られなかった。今年度は数学的証明を与え、実装上のバグと思われていた不整合が本質的なバグであったことを示した。(査読付国際会議投稿準備中)後者は割込み処理の時間制約モデル記述としてcontroller automatonに注目し、時間制約を非対角制約に制限した場合の時間プッシュダウンオートマトンへの変換可能性を発見し、現在、その正しさの証明および実装を含めた検討を進めている。
研究分担者(小野)はソフトリアルタイムソフトウェア構想検証のためのアクセス制御の非同期処理および多段処理のケースタディとして、クラウド環境下におけるwebサーバを取り上げ、1.webアプリケーションにおけるロール(セキュリティレベル)に応じたアクセス制御モデルの構築と、アクセス競合環境下におけるモデル検査形Spinを用いた形式検証手法(研究会発表1)、2.クラウドコンピューティング環境において重要視されるアクセス制御の多段委任可能なSPKIという認証方式によるネットワーク間相互接続を行うための分散型オンデマンド仮想システム構築法(研究会発表2)についてケーススタディを行った。
|
