Profile | 池田愛大

振る舞いを形式検証可能なワイヤレスセンサネットワークプログラムの開発環境の構築

ワイヤレスセンサネットワーク(WSN)はフィールドにセンサノードと呼ばれる小型の機器を配置することによって、温度や湿度などの情報を収集するものです。

センサノードは各種センサによって自分が存在する位置の温度、湿度、照度などの物理現象の観測ができ、無線通信によって他のノード等に取得したデータを送信ができます。また、計算資源(CPU、メモリ等)を持ち情報を処理することもできます。

WSN卒論図6_オリジナルセンサノード(左:ワイヤレスセンサネットワーク 右:センサノード)

これらは近年注目の集まっているIoT技術の一部です。ユーザはプログラムを各センサノードにインストールしてWSNを構築しますが、この時プログラムにバグが有るとWSN全体が落ちたり不安定になったりすることがあります。

これらを回避しようとテストやデバッグをするのですが、実機で確認するのは困難で特定条件などでしか発生しないバグが見逃される事が往々にしてあります。そこで実機以外の確認の仕方として、シミュレーションと形式検証があります。

シミュレーションでは、特定の動作の確認や途中経過の確認などを行うことは容易ですが、1つのプログラムで起こりうる全ての動作を行うようなテストパターンを作成するのが困難です。一方、形式検証ではモデル検査ツールを使うことによってユーザがテストパターンを作成することなく全ての動作を検査していくことにより、対象となるプログラムを検証することができます。

私たちの研究ではセンサノードが頻繁に回収されるものではないこと、WSNが災害時やその他緊急時などに人が出入りできないような場所の観測などを考慮し、不測の事態がないようにあるプログラムの全ての振る舞い(全状態)を検査できる形式検証を採用し、WSNのプログラムへ簡単に適用できる開発環境の構築を目指しています。

 

学会発表等:

☆査読付き投稿論文

Akihiro Ikeda, Naoki Akiyama, Toshiaki Miyazaki, “Formal  Verification  for  Wireless  Sensor  Network   in Consideration of Communication Errors ,” IEEE ICOIN2018, Chaing-mai, Thai, January 10-12, 2018.

☆口頭発表

池田愛大,秋山直輝,宮崎敏明,”無線センサネットワークにおけるデッドロック検出のための形式手法 (Formal Approach to Detecting Deadlocks in Wireless Sensor Networks),” 情報処理学会第79回全国大会(名古屋大学), 1U-03, March 2017.

*池田 愛大, 園家 俊, 佐藤 慎也, 竹渕 宥仁, 矢口 勇一, 奥平 恭子, 出村 裕英, たんぽぽ計画チーム, ”モルフォロジー演算を用いたエアロゲルの貫入孔画像に対する形状推定と体積計算及びその評価(The shape estimation for images of impact holes in aerogel by morphology operation and volume computation and evaluation for the shape),” 情報処理学会第78回全国大会(慶應義塾大学), 1M-05, March 2016.

*研究室とは関係有りません

共著:

☆口頭発表

N. Akiyama, A. Ikeda and T. Miyazaki, “Deadlock-free Behavior Definition for Wireless Sensor Nodes Using Formal Verification, ” IEEE student session in 2016 Tohoku-Section Joint Convention of Institutes of Electrical and Information Engineers, Japan (平成28年度電気関係学会東北支部連合大会), 2A08, Sendai, Aug. 2016.

秋山直輝,池田愛大,宮崎敏明,”C言語で記述した無線センサネットワーク動作の形式式検証法の提案,” 情報処理学会第80回全国大会(早稲田大学), 7S-01, March 2018.