ソフトウェア工学仕様の検証

レビュー（見直し：review）

レビューには大きく分けて以下2種類の方法があり、いずれも，主に仕様への準拠性を確認する。顧客の要求，特に非機能要求の充足を確認することは難しい。仕様（要求定義・設計）やプログラムコードを読み直すことで検証。仕様を見直し、誤りを早めに修正し、品質管理を行う。実践的には、プロジェクトの進捗把握と計画に利用される。

レビューのタイミングはウォーターフォール的でモデルの場合は、フェーズ毎に上流から渡される文書を対象とする。アジャイルなどの発展的開発では、くり返し開発をするたびに見直しをする（１～２週間程度のスパン）。

レビューとテストの技術は補完関係にあり、検証の対象・目的に応じて使い分けが必要となる。
検証の対象が要求仕様・設計などの文書であればレビューしかできない。
プログラムであれば、目的によってレビューでできることもあるが、テストの方が有利なことも多い。
開発プロセスであればレビューでしか検証できない。

レビューの前提

・何が「正しい」のか定義されていないといけない。正しさを検証するためのチェックリストなどを持ちいる。
・対象となる文書について，必要事項が定められた形式で構造や文法の正しいものが与えられている。対象の中身の正しさを検証できる状態であること
・開発の管理側（あるいは顧客側）が，レビューによる初期的なコスト増に合意している
・レビュー結果を対象文書の作成者に対する人事的な評価に使わない。（社内の余計な争いを避ける）

インスペクションとウォークスルー

いずれも欠陥を発見する目的で行う。

インスペクション（査閲：inspection）

文書を検査して欠陥を発見する。計画、概要提示、事前検討を受けて行うインスペクション会議を中心とした一連の作業。インスペクション会議は1-2時間で行い、修正に関しては話合わない。

インスペクションへの参加者と役割

 作者
– 対象となる文書を作成，あるいはその文書についての責任を持つ。インスペクション会議後、文章を修正する。
 読者
– インスペクション会議において文書を読み上げる
 インスペクタ
– 文書の欠陥や問題点を見つける
 書記
– インスペクション結果を記録する
 モデレータ
– インスペクションプロセスの進行を統括管理し，結果をチーフモデレ
ータに報告する
 チーフモデレータ
– インスペクションプロセスの改善を図る（チェックリストの更新など）

インスペクションのチェックリストを作成する

ありがちな欠陥のリスト
　– ドメイン知識に基づいて作成
　　• 当該ドメインにおいてなくてはならない要素・見落としがちな要素
　　• アーキテクチャ設計の妥当性
　　• システムモデル（構造・振舞い），モジュール設計，アルゴリズム等の常識的なパターン
　– プログラミング言語の知識に基づいて作成
　　• 型・データフロー・依存関係など
　　• ｃｆ．ホワイトボックステスト，静的解析

ウォークスルー（徒歩検査：walkthrough）

一定のパターンで文書を模擬（机上）実行する

モデル検査検証

システムの振舞い仕様が要求される性質を満たすかどうかを示す。

検証の対象となるシステム
– 通信プロトコル
– 並行・分散システム

　　↑これらは再現が難しいためテストによる検証が難しい。

振る舞い仕様の検証方法

振舞い仕様を状態遷移システムで記述する。

仕様の満たすべき性質を形式的に記述する。

仕様が性質を満たすことを示す
– 定理証明に基づく（c.f. 正当性証明）
– 状態空間の網羅的な探索に基づく➔モデル検査

モデル検査検証（model checking verification）

状態遷移システムで定まる振舞いから遷移
状況のグラフを作成する。並行性を持つシステムの場合，複数モデルの直積をとる。
あらゆるイベント系列に対して可能な遷移からグラフを作成していくと合成したシステム全体の状態空間となる。
検証したい性質を時相論理式により記述（時間の要素が入っていることが重要）
　– CTL（計算木論理），LTL（線形時相論理），など

状態空間グラフの経路探索により性質の充足・非充足を検査し、経路の確認を行う。

例：「哲学者の食事問題」