確率時間ゲーム理論による組込みシステムのモデル化,仕様記述及び検証

山根 智  林 将志  

誌名
電子情報通信学会論文誌 D   Vol.J93-D   No.7   pp.1214-1225
発行日: 2010/07/01
Online ISSN: 1881-0225
DOI: 
Print ISSN: 1880-4535
論文種別: 論文
専門分野: ディペンダブルコンピューティング
キーワード: 
確率時間ゲーム理論,  確率時間システム,  組込みソフトウェア,  仕様記述,  検証,  

本文: PDF(345.7KB)
>>論文を購入


あらまし: 
オープンな確率時間システムに対する検証手法として,確率時間ゲーム理論を提案する.オープンなシステムのリアクティブ性を2人のプレイヤーが行うゲームとしてとらえ,システムが勝利する戦略を探る.A. Pnueliらの時間ゲームをもとに確率的な拡張を行った確率時間ゲームを構築することで,オープンな確率時間システムに対する検証を行うことを可能とする.本論文では,仕様記述言語である確率時間ゲームオートマトンを定義し,そのオートマトンに対する検証手法を提案する.検証は到達ゲームに関する検証であり,システムがゲームの結果,望ましい状態への到達可能性を検証するものである.