| 研究課題/領域番号 |
17H01719
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| 研究分担者 |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| キーワード | 仕様記述・検証 / ソフトウェアモデル検査 |
|---|
| 研究実績の概要 |
研究実施計画に従って実績を述べる．
(1)のフォールトインジェクションに関しては，予定通りにリファクタリングを行った．これによって，モデリングの際にコードを再利用することが容易になった．
(2)のmodbat量的モデリングに関しては，研究計画を変更して，仮想時間を導入することとなり，その設計及び実装を行った．長い待ち時間を有するアプリケーションをテストする際には，効率的なテスト実現のために，待ち時間の短縮が必須である．従来の手法では，指定された実際の待ち時間に対して，一定の割合で時間を短縮するほかに方法はなく，その効果は限定的であった．これに対して新たに導入した仮想時間では，イベント発生がおこらないことを検知することによって安全に時間を進めることができるので，原理的には余分な待ち時間を0にすることが可能となり，多くのモデルにおいて性能向上が期待される．設計の過程では，Modbat の中心となる制御機構に大幅な変更を加える必要があることが判明したため，いくつかの候補を比較検討して，採用するアルゴリズムを決定した．また，実時間での実行速度が無視できないコードの実行と，仮想時間による待ちが両立できるように配慮した設計を行うよう留意し，これを実現した．実装の過程では，Acca scheduler の機能を利用することによって，工数の削減を図ることができた．
(3)の検証用MQTTアプリケーションに関しては，前年度に作成した，Smart Houseアプリケーションに対する改良を行った．前項目で導入した仮想時間を用いてアプリケーションを書き直すことにより，実際に大幅なテスト時間短縮効果が得られることを確認した．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
状態分布の実装を効率化する必要が生じたため，2020年度に研究計画の変更を行い，MQTTサーバとMQTTクライアント間の通信の仮想化を実施することとした．変更後の計画にしたがって実装を進めており，現在までに仮想化のコードの記述はほぼ終了した．簡単な動作確認テストを実施したほか，仮想化による性能向上を確認する実験も実施している．これによって計画の残りの部分を実施するための障害は取り除かれたため，おおむね順調な進展であると評価する．
|
| 今後の研究の推進方策 |
上述したように，2020年度に変更した計画に従って研究を進めていく．2019年度まで実装を担当していた研究協力者が2020年度は継続できないことになったが，新たな研究協力者を得ることができた．新旧両担当者の間で引き継ぎも順調に行えたので，問題は無いと判断している．現時点では，これ以上の研究計画の変更が必要になるとは考えていない．
|
