Simulink Design Verifier の「網羅的解析を実行」と「デッド ロジック (一部)」は何が違うのですか？

Simulink Design Verifier の設計エラー検出オプション「網羅的解析を実行」はどのような機能でしょうか。

「デッド ロジック (一部)」 との違いを教えてください。

Answer 1

[MathWorks Support Team]

Simulink Design Verifier における「網羅的解析を実行」 は、デッド ロジック解析を より広い範囲・深いレベルで実施するための追加オプションです。

このオプションは 「デッド ロジック (一部)」が有効な場合にのみ使用可能です。

両者の違いは、レポートされるオブジェクティブの範囲と解析で近似を使用するかどうかにあります。

​

例：解析対象モデル

以下のモデルを例に説明します。

​

・Logical Operator ブロック

第 2 入力ポートが Constant ブロックに接続されており、デッド ロジック

​

・Discrete State-Space ブロック

Simulink Design Verifier では 未サポートのブロック

​

​

「デッド ロジック (一部)」が有効／「網羅的解析を実行」が無効の場合

​

この場合、Simulink Design Verifier は、解析時間内に デッド ロジックであることが確定できたもののみ をレポートします。

アクティブ ロジック（到達可能なロジック）や未判定のオブジェクティブについては レポートされません。

また、この解析では 近似を行わない／限定的な解析が行われるため、一部のデッド ロジックが検出されない可能性があります。

​上記モデルの場合、Logical Operatoreブロックのデッドロジックのオブジェクティブのみがレポートされます。

​

​

​

「デッド ロジック (一部)」が有効／「網羅的解析を実行」が有効の場合

​

この場合、Simulink Design Verifier は、

• ​デッド ロジック
• アクティブ ロジック（デッドではないことが証明されたもの）
• 未判定のオブジェクティブ​

を含めて すべてレポートします。

この解析では、必要に応じて 有理近似などの近似手法を使用し、より網羅的に解析を行うため、

追加のデッド ロジックが検出される場合がある解析時間は長くなる傾向がある

という特徴があります。

​

上記モデルでは、Logical Operatorブロックに対して、デッド ロジックのオブジェクティブだけでなく、

デッドではないことが証明されたアクティブ ロジック、

また、スタブ（未サポートブロック）の影響により未判定となったオブジェクティブがレポートされます。