2001 Fiscal Year Annual Research Report
| Project/Area Number |
12133206
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
二木 厚吉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
飯田 周作 専修大学, ネットワーク情報学部, 専任講師 (80338590)
緒方 和博 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30272991)
森 彰 産業技術総合研究所, サイバーアシスト研究センター, 主任研究員 (30311682)
|
|---|
| Keywords | 振舞モデル検査 / 安全性 / 自動証明器PigNose / UNITY / CadeOBJ / 認証プロトコル / Java仮想機械 / 検証 |
|---|
| Research Abstract |
本年度は、以下のことを行った。
・振舞モデル検査:移動コードの安全性を保証するための基礎技術として昨年度から研究を行っている振舞仕様を用いたモデル検査(振舞モデル検査)についての研究の一環として,モデル検査をインターネット上で並列処理をするシステムの設計と簡単な実装を行った.具体的には,モデル検査の収束判定に対応する含意式の証明を先読みしていくつかの計算機に割り当て,証明が成功した時点で不要な証明作業の枝刈りとそれに伴う再計算処理を行っている.この際,個々の証明は,代数仕様言語システムCafeOBJ上で開発された自動定理証明器PigNoseを用いて各計算機上で行われる.
・CafeOBJによる認証プロトコルの検証:UNITYとともに用いることで,並行・分散システムおよび実時間システムをCafeOBJで記述・検証してきた.こうした手法が,修正版NSPK(Needham-Schroeder Public-Key)認証プロトコルを例として,セキュリティプロトコルにも適用できることを示すことができた.このことは,CafeOBJとUNITYの組合わせで,広範囲のシステムを扱うことができることを意味しており,本手法の利点である.
・Java仮想機械のCafeOBJ仕様の開発:Java仮想機械のCafeOBJ仕様を作成するにあたって,基本的なデータ構造等の設計をやり直し,より洗練されたモジュール化となった.これらのモジュールは,Javaバイトコード検証器と共通のものであり,ライブラリとして整備することにより,一般的な仮想機械と検証器の仕様記述に応用可能であり,よりモジュール化され再利用性の高い仮想機械の仕様の開発が可能になる.
|
-
[Publications] K.Futatsugi, K.Ogata: "Rewriting can verify distributed real-time systems -How to specify and verify in CafeOBJ"Proc. of the Int 1 Workshop on Rewriting in Proof and Computation(RPS 01). 60-79 (2001)
-
[Publications] 飯田周作, 二木厚吉: "振舞仕様に基づく仕様コンポーネント化技術の発展可能ソフトウェアへの応用"日本ソフトウェア科学会学会誌 コンピュータソフトウェア. 18・0. 30-45 (2001)
-
[Publications] A.Mon, T.Sawada, K.Futatsugi, A.Seo, M.Ishiguro: "Software component search based on behavioral specification"Proc. of Int 1 Symposium on Future Software Technology(ISFST 2001). (2001)
-
[Publications] T.Seino, K.Ogata, K.Futatsugi: "Specification and verification of a single-track railroad signaling in CafeOBJ"IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences. E84-A・6. 1471-1478 (2001)
-
[Publications] R.Diaconescu, K.Futatsugi, S.Iida: "CafeOBJ jewels"CAF : An industrial-Strength Algebraic Formal Method. 33-60 (2001)
-
[Publications] K.Ogata, K.Futatsugi: "Formally modeling and verifying Ricart&Agrawala distributed mutual exclusion algorithm"APAQS 2001 Conference Proceedings. 357-366 (2001)
