【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット|形式検証とは

形式検証とは、数理論理学を用いてソフトウェアの品質向上を図る手法である形式手法を用いて、ソフトウェアの正しさを検証する作業です。要求や仕様を厳密に記述(形式仕様記述)したり、満たしてほしい性質が必ず満たされているか網羅的に検証(モデル検査)できます。本記事では「モデル検査」について紹介します。

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット|曖昧な記述(自然言語、暗黙知など)※要求や仕様の場合→変換→厳密な記述(形式仕様記述/
モデル検査)→利用→網羅的な検証(モデル検査)

モデル検査では、システムの取り得る状態と遷移をモデル化した「状態モデル」と、状態モデルが満たしてほしい論理的な条件「検査式」を作成し、状態モデルが検査式を満たすかツールで検証することで不具合の有無を確認します。例えば「望ましい状態に必ず到達する」ことや「危険な状態には絶対に到達しない」ことを網羅的に調べ、違反する遷移の例を確認できます。

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット|検証対象の成果物→状態モデル|検査式→ツール→検証結果OK/NG

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット|メリットとデメリット

モデル検査のメリットは、システムの取り得る全ての状態に対して網羅的に検証できる点です。例えば、不具合の原因が分からないシステムをモデル化して検証すると、不具合の状態に至る遷移を突き止められます。複数の状態モデルが相互に影響し合うような、人の目では分析の難しい複雑なシステムで特に効果的で、要求定義から実装まであらゆる工程で利用できます。レビューでの検証が中心となってきた要求定義にも適用できるのが特徴的で、今回の説明対象としています。

デメリットとしては、状態数が多すぎると組合せの数も膨大となり、検証用のツールが動かなかったり検証に非常に時間がかかったりして検証が難しくなる「状態爆発」が起こりやすい点が挙げられます。

以降、要求の形式検証の手順を説明します。

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM形式検証の概要とメリット、デメリット|pagetop