空間の概念を持つコスト付き確率時間オートマトンの記号的検証手法

摘要

Recently, wireless sensor networks attracts attention in various fields. Moreover, with the making of the embedded system high performance, the demand for the verification method for those systems has risen. Then, we model the wireless sensor network with priced probabilistic timed automaton with spaces (SP~2TA), and develop the reachability analysis technique in SP~2TA.%近年，無線センサネットワークがさまざまな分野において注目を集めている．また，組込みシステムの高機能化に伴い，それらのシステムに対する検証手法の需要が高まっている．本研究では，空間の概念を持つコスト付き確率時間オートマトン（SP~2TA）を用いて，無線センサネットワークをモデル化し，SP~2TAにおける到達可能性解析手法を開発する．