抄録

◎後藤亮馬・和崎克己（信州大）

上流工程において，モデル記述からモデル検査器用のプロセスに変換する手法は広く研究されており，UML-PROMELA変換器もそのひとつである．
本研究ではUML-PROMELA変換器を用いて，RPL(IPv6 Routing Protocol for Low-Power and Lossy Networks)のモデル化，検証を行った．
モデル化の際には，UMLのコミュニケーション図を用いてノードの通信接続状況を記述し，ステートマシン図でノードの振る舞いを記述した．
上位設計向けの準形式化されたこれらの図を使用してモデルを記述することで，検証したいノード数や通信状況の変化に応じて自動コード生成が行われるため，スケーラブルな対応を迅速に行うことができる．
今回作成したモデル，PROMELAコードを用いてRFC6550のノード探査部分を中心にデットロック検証を行い，エラーが無いことを確認した．