| 大会名称 |
|---|
| 2014年 情報科学技術フォーラム(FIT) |
| 大会コ－ド |
| F |
| 開催年 |
| 2014 |
| 発行日 |
| 2014/8/19 |
| セッション番号 |
| 7B |
| セッション名 |
| モデル・形式手法 |
| 講演日 |
| 2014/9/5 |
| 講演場所(会議室等) |
| 3B棟4F 3B402 |
| 講演番号 |
| B-019 |
| タイトル |
| UML-PROMELA変換器を用いたZigBeeIP/RPLプロトコルにおけるノード探索仕様の検証 |
| 著者名 |
| 後藤 亮馬, 和崎 克己, |
| キーワード |
| 上流工程, モデル検査, UML, SPIN, ZigBeeIP, 自動コード生成 |
| 抄録 |
|
上流工程において，モデル記述からモデル検査器用のプロセスに変換する手法は広く研究されており，UML-PROMELA変換器もそのひとつである． 本研究ではUML-PROMELA変換器を用いて，RPL(IPv6 Routing Protocol for Low-Power and Lossy Networks)のモデル化，検証を行った． モデル化の際には，UMLのコミュニケーション図を用いてノードの通信接続状況を記述し，ステートマシン図でノードの振る舞いを記述した． 上位設計向けの準形式化されたこれらの図を使用してモデルを記述することで，検証したいノード数や通信状況の変化に応じて自動コード生成が行われるため，スケーラブルな対応を迅速に行うことができる． 今回作成したモデル，PROMELAコードを用いてRFC6550のノード探査部分を中心にデットロック検証を行い，エラーが無いことを確認した． |
| 本文pdf |
| PDF download (918.8KB) |