有界モデル検査を用いた逐次Ｃプログラムのモジュラー検証に関する研究

橋本, 祐介; ハシモト, ユウスケ; HASHIMOTO, Yusuke

WEKO3

lat lon distance

[[sub_check.contents]]

[[sub_radio.contents]]

Field does not validate

[[sub_attr.contents]]　

インデックスツリー

アイテム

有界モデル検査を用いた逐次Ｃプログラムのモジュラー検証に関する研究

https://ir.soken.ac.jp/records/3141

名前 / ファイル	ライセンス	アクション
要旨・審査要旨 (388.0 kB)
本文 (1.3 MB)

Item type

学位論文 / Thesis or Dissertation(1)

公開日

2012-09-14

タイトル

有界モデル検査を用いた逐次Ｃプログラムのモジュラー検証に関する研究

言語

jpn

資源タイプ

資源タイプ識別子

http://purl.org/coar/resource_type/c_46ec

資源タイプ

thesis

著者名

橋本, 祐介

フリガナ

ハシモト, ユウスケ

著者

HASHIMOTO, Yusuke

学位授与機関

学位授与機関名

総合研究大学院大学

学位名

博士（情報学）

学位記番号

内容記述タイプ

Other

内容記述

総研大甲第1514号

研究科

値

複合科学研究科

専攻

値

17 情報学専攻

学位授与年月日

2012-03-23

学位授与年度

値

2011

要旨

内容記述タイプ

Other

内容記述

  近年，身の回りの消費者向け製品や社会基盤システムでは，多くの機能がソフトウェアで実現されている．製品やシステムの障害が社会的関心事となり，ソフトウェアにも高い品質が求められている．産業界ではソフトウェアの品質確保をプログラム・テスティングで行っており，開発期間の半分以上を費やすこともある．ソフトウェア品質向上の新しい技術が求められている．
  自動検証の技術にロジック・モデル検査の方法がある．有限遷移状態系として表現された検証対象と時相論理で表した検証性質を与えると，有限状態空間上の実行可能な全経路を網羅探索して，検証性質が満たされることを調べる．モデル検査には，「状態爆発」と呼ばれる，検証対象の規模に関して指数的に計算資源を消費するスケーラビリティの問題がある．有界モデル検査（BMC）は，探索範囲を限定して状態爆発を緩和し，効率的に不具合を発見する手法である．プログラムを対象とするソフトウェアモデル検査は，プログラムを有限状態遷移系に変換してモデル検査を行う．自動検証かつ網羅性が高いことから，産業界に導入しやすい品質向上手段といえる．しかし，実用的なプログラムではBMCでも状態爆発が起こる．従来のプログラム・テスティングとの関係も明らかでない．ソフトウェアモデル検査の実用化では，これらの問題を解決する必要がある．
  プログラム検証の考え方にモジュラー検証がある．Cプログラムの場合，関数に事前・事後条件を，大域変数に不変条件を付記し，事前・不変条件を満たす状態から関数を実行し，実行後の状態が事後・不変条件を満たすことを静的に調べる．個々の関数を検証単位とするので，大規模なプログラムも扱える．しかし，関数に閉じて検証するので，コールシーケンスに関わる情報の不足から，不具合の見逃しや誤警告が起こりうる．
  本研究では，逐次C プログラムの新しい品質向上手段として，BMCとモジュラー検証を組み合わせたソフトウェアモデル検査技術を提案する．モジュラー検証の導入によりBMCのスケーラビリティを向上する．このBMCを用いたモジュラー検証を本研究の基本的な技術として，さらにモジュラー検証の課題とBMCの課題についてそれぞれ解決方法を提案し，その有効性を実験により確認する．
   BMCを用いたモジュラー検証では，事前・事後・不変条件を，assertやassumeといったBMCの検証プリミティブに変換して対象プログラムに埋め込む．そして，事前・不変条件を満たす初期状態から到達可能な状態が事後・不変条件を満たすことを，BMCの方法で調べる．産業界の製品プログラムを用いた実験を行い，別途実施した単体テストで見つかった不具合を再発見することで提案方法の基本的な有効性を確認した．
   Cプログラムでは，モジュールへの再入や関数ポインタを用いた間接呼び出しといった従来の静的なモジュラー検証では不具合を見逃す状況が発生する．
  特定の機能を実現する関数の集まりをモジュールと呼ぶとき，あるモジュールから呼ばれたモジュールが，呼び出し元モジュールを呼び返すことを，モジュール再入と呼ぶ．モジュール再入はコールバック型プログラムでは頻繁に起こる．再入箇所で不変条件違反が起きる場合に，関数を検証単位とするモジュラー検証では不具合を見逃す．本研究では，ファイルをモジュールとみなし，あるファイルに定義された不変条件をそのファイルに限定して検証するための記法と，ファイル限定の不変条件から検証プリミティブへの変換方法を考案した．これを用いて，検証単位をコールシーケンスに拡張するBMCのインライン展開機能と組み合わせた検証方法を提案する．提案方法の実験を行い，モジュール再入箇所において，ファイル限定不変条件への違反を精度良く発見できることを示した．
  関数ポインタを用いた間接呼出しでは，実際に呼ばれる関数は，そのアドレスを関数ポインタに実行時に代入することで決まるので，静的に特定することが難しい．また，間接呼び出し側と実際に呼ばれる側が独立に開発されることもあり，前者の検査を行う際に後者のコードや事前・事後条件を利用できないことも多い．本研究では，関数ポインタ変数に事前・事後条件を定義する記法を導入したモジュラー検証と，関数ポインタと実際に呼ばれる関数の置換可能性検査との2段階からなる検証方法を提案する．置換可能性検査には，オブジェクト指向プログラミングにおけるスーパー・サブタイプの置換可能性の考え方を応用した．オープンソースのOSであるMINIXを用いて提案方法の実験を行い，関数ポインタの事前・事後条件によって誤警告を減少できることを確認し，間接呼び出しに関わる未発見バグの検出に成功した．
   BMCは，プログラムを有限状態遷移系に変換する際に，抽象化を行わず，精度の高い検証を行う．しかし，変換時の過小近似によって，有限状態空間上の経路が少なくなり，元のプログラムに存在する不具合を見逃すことがある．そこで探索しない過小近似箇所を見つけて，別の手段で検査する必要がある．本研究では，BMCの過小近似箇所を自動検知する方法を考案し，検知した場合に，事前・事後条件からテストケースを自動生成して，単体テストで補う方法を提案する．過小近似検知の網羅度と単体テスト実行の網羅度は，産業界で高信頼ソフトウェアのテスティングに用いるMCDC基準にしたがって測定する．MINIXを用いて提案方法の実験を行い，BMCの過小近似箇所をMCDC基準で検知できることと，BMCと自動生成した少数のテストケースによる単体テストを合わせてMCDC基準を100%達成できることを示した．
  プログラムの事前・事後条件は入力データと期待結果と見なせるので，事前・事後条件の定義は単体テストの計画に相当する．また，BMCを用いたモジュラー検証は，単体テスト実施の自動化を実現する．さらに，単体テストと共通のカバレッジ基準を用いたBMCの過小近似検知と，BMCを事前・事後条件から生成したテストケースによる単体テストで補完する方法は，従来の単体テスト評価に相当する．本研究の提案方法は全体として，従来の単体テスト作業（計画・実施・評価）を効率化する．形式検証技術の産業界への移転を容易にする方法といえる．

所蔵

値

有

フォーマット

内容記述タイプ

Other

内容記述

application/pdf

戻る

views

See details

	Views

Versions

Ver.1

2023-06-20 15:37:42.149968

Show All versions

Cite as

エクスポート

OAI-PMH

JPCOAR 2.0
JPCOAR 1.0
DublinCore
DDI

Other Formats

JSON
BIBTEX

インデックスリンク

インデックスツリー

アイテム

有界モデル検査を用いた逐次Ｃプログラムのモジュラー検証に関する研究

× 橋本, 祐介

× ハシモト, ユウスケ

× HASHIMOTO, Yusuke

Versions

Share

Cite as

エクスポート