2002 Fiscal Year Annual Research Report
| Project/Area Number |
13558028
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
谷口 健一 大阪大学, 大学院・情報科学研究科, 教授 (00029513)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
岡野 浩三 大阪大学, 大学院・情報科学研究科, 助教授 (70252632)
北道 淳司 会津大学, コンピュータ理工学部, 助教授 (20234271)
東野 輝夫 大阪大学, 大学院・情報科学研究科, 教授 (80173144)
森岡 澄夫 日本アイ・ビー・エム, (株)・基礎研究所, 副主任研究員
山口 弘純 大阪大学, 大学院・情報科学研究科, 助手 (80314409)
|
|---|
| Keywords | 並列同期システム / 実時間システム / 自動検証 / 時相論理式 / モデルチェッカー |
|---|
| Research Abstract |
本研究は,同期式順序回路を対象にハードウェアの高位設計検証の自動化を目指すものである.昨年度に引き続き,設計法,検証法について検討し,支援システムの作成を行ってきたが,今年度は特に,動作に時間制約が付いた実時間システムの仕様記述およびその検証について検討した.実時間システムの各モジュールを拡張時間オートマトンにより記述し,各オートマトン間の同期遷移を指定することにより,全体システムを記述する.時間制約付きシステムの検証には,既存のリアルタイムモデルチェッカーUppaalを利用することも考えるので,今回,検証はUppaalを用いて行った.検討のための例題として動画像デコードシステムを取り上げ,時間制約付きオートマトン群で全体記述を行う.システム全体の安全性や負荷に応じフレームバッファ制御が行われているかなどの機能実現性の検証のために,検証用のオートマトンを追加し,もとの記述も一部変更して,記述全体がそれらの性質を満たすことを保証する時相論理式を与える.Uppaalの検証式は時相演算子が先頭に1個のみという制約を持つが,安全性や機能実現性に関する検証はそのもとで自動で行えた.例題の5個程度の有限状態をもつ10個程度のモジュールからなるシステムに対して,それらの検証式の真偽判定は20秒程度で行えた.結果は電子情報通信学会の研究会で発表した.どのようなクラスや検証性質であれば,記述の変形の正しさを保証しつつ,Uppaalの検証式で検証可能であるか等が残された課題である.我々が考案開発した整数あるいは有理数のプレスブルガー文真偽判定ルーチンを用いた実時間システムの検証法の検討も今後の課題である.
|
Research Products
(1 results)
