【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順|検証の目的を決める

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

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順|状態と遷移の条件を抽出し、状態モデルの形に整理する

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

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

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順|検査式を作る

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

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順|ツール用の記述に変換し検証を実行する

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

【研究室】USDMによる要求の定義と仕様化~USDM要求の形式検証~USDM要求の形式検証の手順|pagetop