文献

J-GLOBAL ID：201702274270317659   整理番号：17A0870008

ソフトウェア工学の最前線~ソフトウェアが社会のすべてを定義する時代~未来に向かって 不確かさを考慮したソフトウェア・テスティングおよび形式検証

著者 (3件)： 石川冬樹 (国立情報学研) ,  來間啓伸 (日立) ,  中島震 (国立情報学研)
資料名： 情報処理  (IPSJ Magazine)
巻： 58  号： 8  ページ： 693-695  発行年： 2017年07月15日 
JST資料番号： G0427A  ISSN： 0447-8053  資料種別： 逐次刊行物 (A)
記事区分： 解説  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： ビッグデータ分析や機械学習,乱択アルゴリズム,IoT(Internet of Things)といった不確かさのあるソフトウェアではディペンダビリティを達成するために不確かさを扱う必要がある。本論文では,プログラムが欠陥を含むことの確認を目的とするソフトウェア・テスティングと,正しさが既知であることを前提とする形式検証で不確かさを扱う研究動向を紹介した。まず,前者では定めたテストの妥当性を判断する基準(オラクル)を利用するが,各入力に対する絶対的な正解が不明な場合に相対的な正解(疑似オラクル)を生成する方法としてNバージョン・プログラミングや,メタモルフィック・テスティングについて述べた。また,プログラム実行が確率分布に従う変数に依存する場合に利用する統計的オラクルや,テスティング効率を向上させるために扱いが難しい入力データを生成する方法を示した。次に,形式手法としてEvent-Bの標準的枠組みの中で形式検証を可能にするために,非決定的選択に確率を与える方法を示した。さらに,状態遷移をマルコフ連鎖やマルコフ決定過程で表現する確率的モデル検査,及び離散シミュレーションを用いて仮説検定を行う統計的モデル検査について述べた。最後に,環境への不確かさに対応する検証手段として,実行時検証を紹介した。

シソーラス用語： *ソフトウェア工学 ,  *ソフトウェア ,  不確実性 ,  *プログラム検査 ,  *相互接続 ,  *インターネット ,  信頼性 ,  *形式的手法【計算機】 ,  プログラム検証 ,  *確率モデル
準シソーラス用語： *IoT ,  ディペンダビリティ

分類 (4件)： 計算機システム開発  (JD02010R) ,  その他の情報処理  (JE15050M) ,  計算理論  (JB02000A) ,  システム・制御理論一般  (IA02010H)

引用文献 (6件)：

• Weyuker, E. J. : On Testing Non-testable Programs, Computer Journal, Vol.25, No.4, pp.465-470 (1982).
• 中島 震:共通理解フレームワークとしてのサイバー・フィジカル・システム,情報処理学会ソフトウェア工学研究会第190回(2015).
• Nakajima, S. and Bui, H. N. : Dataset Coverage for Testing Machine Learning Computer Programs, APSEC 2016, pp.297-304 (2016).
• 中島 震,來間啓伸:Event-B-リファインメントに基づく形式手法,近代科学社(2015).
• Hallerstede, S. and Hoang, T. S. : Qualitative Probabilistic Modelling in Event-B, iFM2007, pp.293-312, Springer (2007).

タイトルに関連する用語 (7件)： ソフトウェア工学 ,  ソフトウェア ,  社会 ,  定義 ,  未来 ,  不確かさ ,  形式検証