| 研究分担者 |
北道 淳司 大阪大学, サイバーメディアセンター, 講師 (20234271)
岡野 浩三 大阪大学, 大学院・基礎工学研究科, 講師 (70252632)
東野 輝夫 大阪大学, 大学院・基礎工学研究科, 教授 (80173144)
山口 弘純 大阪大学, 大学院・基礎工学研究科, 助手 (80314409)
北嶋 暁 大阪大学, 大学院・基礎工学研究科, 助手 (00304030)
|
|---|
| 研究概要 |
(1)昨年に引き続き,拡張有限状態機械(EFSM)の動的性質(望みどおりの要求性質を満たす状態にいつかは必ずたどりつける,デッドロック状態に陥ることはない,など)を自動検証できるように,単体のEFSMに対する動的性質の検証アルゴリズムの検討をおこなった.考案した検証法では,自動検証を可能にするため回路に対する十分条件を定めた.そのもとで,検証では,整数を直接扱えるようプレスブルガー文真偽判定ルーチンを有効に使う工夫も行った.
(2)引き続き,EFSMを複数個に拡張したモデルに対する動的性質の検証アルゴリズムを考案し,そのアルゴリズムの実装と評価実験を行った.この手法において自動検証を可能にするためのモデルを定めた.そのモデルでは,各EFSM間の同期,非同期が自由に指定できる.評価のための例題としてオークションシステムをとりあげ,「いつかはいずれかのバイヤーが落札する」,「複数のバイヤーが共に落札することはない」などの諸性質をPC上で数分以内で検証可能であることを確かめた.
(3)CPU高位設計の自動検証作業を経験させるために,学部学生のCPU設計実験において,本研究室で開発した自動検証ツールを3年前より導入している.
この学生実験では,CPUの高位の要求記述から始めて,最終的には,複数の順序回路で表現されたCPU制御部を作成する.
学生の作業履歴や設計CPUを調べた結果,検証ツールが誤りのない設計を行うのには特に有効であることを確認し,その結果を今年度,論文2編にまとめた.
(4)昨年,時間制約付きで複数の並行動作回路を記述できるモデルとして,Alurの時間オートマトンを大域変数付きに拡張したモデルTASVを提案し,そのモデル上でのデッドロックフリー性を効率よく判定する判定手法を考案した.
今年度はそれを理論的に整理して論文としてまとめ,論文誌に投稿した.
|
