| 研究課題/領域番号 |
23240003
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
|
|---|
| 研究分担者 |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
Artho Cyrille 国立研究開発法人産業技術総合研究所, 情報セキュリティセンター, 研究員 (30462831)
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2016-03-31
|
| キーワード | 仕様記述・仕様検証 / ソフトウェアモデル検査 / クラウドコンピューティング |
|---|
| 研究実績の概要 |
(1) net-iocache v2．(モデル検査器Java PathFinderでネットワークアプリケーションの検査を可能にする機構) 平成26年度に行った再設計に基づき，既存の部分的な実装をベースに，全体の実装を行った．v1に比較して，SUT (検証対象プログラム) に対する暗黙の仮定を減らすことが実現でき，また，粒度の異なる状態探索の方法が選択可能となった．v1との性能比較を実施し，多くの探索方式において，v1を上回る速度で検証が可能となることを確認した．事例研究の一環として，IoTで用いられるプロトコルであるMQTTクライアントに対してv2を利用したモデル検査を実施することで障害を検出した．MQTTプロトコルによる通信に関しても本手法が有効であることが確認できた．また，早期にバグを発見する手法であるSAMCの考え方をnet-iocacheに導入する実験にも成功した．本ライブラリの公開に関しては，すでに研究者・開発者に利用可能としていたが，文書やサンプルプログラムなどを整備することで，いっそう利用しやすくした．
(2) Modbat．(モデルベーステストツール) Hadoopにおけるプロセス協調実現機構であるZookeeperへのModbatの適用に取り組んだ．クライアントが非同期的な要求を行うことに伴う非決定性を扱うために，Modbatにモデル検査器を組み込むこととした．この機構により，すべての出力の可能性を扱うことが可能となり，妥当なモデルを構築することができた．
(3) UDP検証．平成26年度に，UDP通信を行うプログラムをJPFでモデル検査する方式を開発して得られた知見に基づき，UDPが許容する不確実性を分類し，各々の発現の程度に関する過程に応じてパケット数の評価を行った．すべてのパケットの組み合わせを生成する健全かつ完全なアルゴリズムを考案した．
|
| 現在までの達成度 (段落) |
27年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
27年度が最終年度であるため、記入しない。
|
