CPUと動的再構成可能プロセッサとの協調システムのモデル検査

摘要

CPUとDRPが協調動作するような動的再構成可能組込みシステムのモデル化，仕様記述とモデル検査手法を提案する．プリエンプションやデッドラインのあるCPUはリアルタイムシステムとして仕様記述し，動作周波数の変化が生じるDRPはハイブリッドシステムとして仕様記述する．CPUとDRPを同時に検証しようとすると状態爆発が生じるため，（1）CPUを仕様記述したオートマトンと，環境及びDRPを抽象化したオートマトンとの並列合成オートマトンの検証，（2）DRPを仕様記述したオートマトンと，CPUを抽象化したオートマトンとの並列合成オートマトンの検証の2つの手順を踏むことで，システム全体の安全性を悲観的に検証する．