1. HOME
  2. コラム
  3. コラム
  4. 要求の形式検証~USDMによる要求の定義と仕様化

要求の形式検証~USDMによる要求の定義と仕様化

  • LINEで送る
  • このエントリーをはてなブックマークに追加
要求の形式検証~USDMによる要求の定義と仕様化

要求定義の段階で不具合を修正すれば手戻り工数を大幅に削減できますが、その手段はレビューが中心であり、レビューアのスキルに依存し指摘漏れのリスクが高いことが問題です。これを解決するため、属人的な要素を減らし網羅的に要求を検証する手法として形式手法による検証、すなわち形式検証が注目されています。 

1、USDM形式検証の概要とメリット、デメリット

形式検証とは

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

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

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

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

メリットとデメリット

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

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

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

2、要求の形式検証の手順

検証の目的を決める

まず、検証対象のシステムと、検証の目的を明確にします。これは、モデル化する範囲を絞り込んで状態爆発を防ぐためです。初めて取り組む場合、要求不備が原因で不具合が発生したシステムを選択すれば、その検出が目的となって取り組みやすく、要求段階での形式検証の有効性を実感できるでしょう。 もちろん、未知の不具合の検出を目的としても構いません。既存成果物の中に上位の機能要求や安全目標、不具合リストなどがあれば、そのまま目的として検査式のベースにできます。

状態と遷移の条件を抽出し、状態モデルの形に整理する

次に、目的に関連した要求(下位要求など)から状態(例:システム起動状態OFF)、遷移の条件(例:システム起動終了スイッチON)を抽出して整理し状態モデルを作ります。状態マシン図があれば少しの加工で作れますが、文章の場合は「Aの場合はBする」など原因(入力)と結果(出力)が明確になっていることが必要です。整理の際は、検証に無関係な状態を削除して状態爆発を防止します。表記のブレに気付き統一するなど、この作業を通じて要求記述自体の質が向上するメリットもあります。

USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順|既存成果物→【状態モデル】下位要求を状態モデルの形に整理する※状態と遷移が明記されていれば表形式も可/上位要求を検証の目的として検査式を作る<検査式>ツール用の記述に変換して検証

検査式を作る

状態同士が何の条件を満たしてほしいか、検証の目的に沿って、先ほど整理した状態名を用いた論理学の式で記述します。例えば「『降車したらいつか必ず車両状態Bになる』が常に成立する」は「□(降車⇒◇車両状態B)」となります。既知の不具合の原因を調べたい場合は、あえて「不具合の状態に決して至らない」という意味の検査式を作り、ツールにその反例として不具合に至る遷移を出力させます。

ツール用の記述に変換し検証を実行する

モデル検査のツールには様々なものがありますが、SPINやNuSMVなど無料のツールでも十分に検証できます。整理した状態モデル、検査式をツール用の記述に変換し、検証を実行します。

サービスに関するご相談は
こちらからお願いします

コンサルタントが教える成功の秘訣

コンサルタント 前田 佑希子

大規模化・複雑化したシステムに対して網羅的な検証を行えることから注目されている形式手法ですが、どのように適用すればよいか分からないという声が聞かれます。

エクスモーションでは、検証そのものを行うだけでなく、お客様ご自身でも実施できるよう、対象システム、検証の目的、既存の成果物に応じた作業手順をガイドラインとして提供し、より取り組みやすくする活動も実施しています。

エクスモーションでは、検証そのものを行うだけでなく、お客様ご自身でも実施できるよう、対象システム、検証の目的、既存の成果物に応じた作業手順をガイドラインとして提供し、より取り組みやすくする活動も実施しています。

前田佑希子
  • LINEで送る
  • このエントリーをはてなブックマークに追加