| 研究課題/領域番号 |
17H01719
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
萩谷 昌己 東京大学, 大学院情報理工学系研究科, 教授 (30156252)
|
|---|
| 研究分担者 |
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2020-03-31
|
| キーワード | 仕様記述・検証 / ソフトウェアモデル検査 |
|---|
| 研究実績の概要 |
平成29年度には，研究実施計画にしたがい，3項目(1)フォールトインジェクション， (2a) Modbatにおける量的モデリング手法の理論，および(4a)Modbatテストオラクル生成手法の改良，を実施した．項目(1)については，パケットフォワーダを設計，実装した．これを用いることにより，テスト対象ソフトウェアから見て，通信の遮断や遅延が発生しているように見せることができる．実際に，IoTのプロトコルであるMQTTで通信を行うプログラムのクライアント側にパケットフォワーダを組み込むことによって，モデルベーステストシステムの配下でフォールトインジェクションを行うことができることを確認した．項目(2a)については，従来Modbatで記述できる状態遷移系よりも上位のレイヤで，ネットワーク遅延や故障率などの量的関心事を表現する枠組みの開発を行った．時間オートマトン等を参考にしつつも，モデルベーステストに適した，階層的な記法となっている．項目(4a)では，クラウドコンピューティングに用いられる分散協調ソフトウェアであるZookeeperをテスト対象と設定し，テストオラクルの中で用いられるアルゴリズムとして，ヒューリスティックに基づく種々の探索手法を考案・実装し，従来の実装よりも高速に判定が行えることを確認した．さらに，特定の対象に依存せずに一般的なオラクル記述が可能になる枠組みをめざし，SMTソルバを用いた判定手法も考案，実装を行った．以上の成果について，第20回プログラミングおよびプログラミング言語ワークショップにおいて発表した．この際のフィードバックも踏まえ，2本の論文の執筆を行い，現在国際会議に投稿中 (1本は準備中) である．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
上述の通り，計画にあげた3項目につき，いずれの項目についても概ね当初予定した内容は実行されている．(2a)については，ややアドホックな記法となっているために，まだ洗練が必要であると考えているが，逆に(4a)については当初予定していなかったSMTソルバの利用までできたため，全体としては概ね順調と評価している．
|
| 今後の研究の推進方策 |
現時点では研究推進上大きな問題点があるとは考えていない．研究実施項目にしたがって，進めていく．実装については，昨年度の担当者から変更が行われることになるが，資料・ソースなどの引継ぎは行われており，影響は限定的であると判断している．
|
