概要
船舶自動識別システム(AIS:Automatic Identification System)とは船舶の安全な
航海を目的とした通信システムのことである．AIS では同時に複数の船舶が情報
の送信を行うと，それらの情報が正しく他の船舶に届かないことがある．その問
題に対処するために，送信予約システムを用いて自分が他の船舶に対して情報を
送信する時間を予約し，同時に送信することがないようにしている．しかし，そ
の送信予約システムを用いても低い確率ではあるが船舶の情報が正しく送受信で
きない場合が存在する．

そこで，本研究ではどの程度の確率で安全性が保たれているかを調べるため，AIS 
の一部である送信予約システムのモデル化と検証を行った．作成したモデルは実
際の予約の取り方に近いものとそれに少し変更を加えたもの 4 つである．これら
に対して確率付きモデル検査器 PRISM を用いて解析と検証を行った．

また，作成した確率付きのモデルの状態遷移系に対して，Symmetry Redcution を
施すことによって大幅な状態数削減を行うことで，規模の大きなモデルに対して
の解析，検証も行った．これによって，規模の小さかった解析と検証では見えな
かった新たな性質が発見できたことも示す．

発表論文
 
``Probablistic Model Checking of an Automatic Identification System,''
The 13th IASTED International Conference on Software Engineering and
Applications, pp.45-52, November, 2009.


``AISにおける送信予約システムの PRISM を用いた解析と検証,''
第7回ディペンダブルシステムワークショップ, pp.1--11, July, 2009.

``Symmetry Reductionを使ったAISの確率付きモデル検査,''
電子情報通信学会技術研究報告: ソフトウェアサイエンス研究会, SS2009-63, pp.91-96, March, 2010.

``Probabilistic Symmetry Reduction for a System with Ring Buffer,"
IEICE Transactions on Information and Systems, to appear.