Simulink Design Verifier

最新のリリースでは、このページがまだ翻訳されていません。 このページの最新版は英語でご覧になれます。

デバウンス時相プロパティ

この例では、Simulink Design Verifier™ の Temporal Operator ブロックを使用して、プロパティ実証およびテスト ケース生成の時相システム要件をモデル化する方法を示します。

時相演算子

Simulink Design Verifier™ ライブラリSimulink Design Verifier™ ライブラリには、時相プロパティのモデル化に使用できる 3 つの基本的な時相演算子ブロックが用意されています。時相演算子の目的は、モデル化されたプロパティと実際の要件の相関関係が近くなるように、時相要件の指定をサポートすることです。これらのブロックは、より複雑な時相プロパティを構築するための下位レベルの構成要素です。

デバウンス モデルおよび要件

固定数のタイム ステップの値を保持する入力に基づいて 0 と 1 の間をデバウンスするデバウンス ロジックについて考えます。

デバウンス機能は、含まれている Stateflow チャートにキャプチャされます。

open_system('sldvdemo_debounce_to')
open_system('sldvdemo_debounce_to/debounce')

検証するデバウンス モデルの 2 つの要件について考えます。

要件 1:

Whenever the input equals 1 for more than 6 steps, the output shall be equal to 2.

要件 2:

Whenever the input becomes 0 for more than 5 steps after the output was 2, the output shall equal 1 as long as the input stays at 0.

プロパティの指定

要件 1 を指定する際に、まず "input equals 1 for more than 6 steps" という制約を示します。これは、Temporal Operator ブロック ライブラリの Detector ブロックでキャプチャできます。7 (6 より上の) タイム ステップの間、入力値が 1 であること が検出された場合、検出後に入力が 1 のままであれば出力が 2 であることを確認するものとします。implies ブロックが後に続く Detector ブロックの Synchronized オプションを使用して、これをキャプチャします。

open_system('sldvdemo_debounce_to/Verify True Output1')

複数の時相演算子ブロックを組み合わせて、より複雑な時相プロパティを作成できます。要件 2 について考えます。

open_system('sldvdemo_debounce_to/Verify True Output2')

わかりやすくするため、この要件を大きく次の 3 つに分けます。

  1. After the output was 2: これはプロパティの有効化条件です。残りの制約をチェックしている間に、過去のいずれかの時点でこの条件が true であったかを確認するものとします。一般的にこの種の有効化条件の後には Extender (Finite または Infinite) が続きます。これは、別の制約と組み合わせて、意図する内容に対する最初の入力を形成します。

  2. The input becomes 0 for more than 5 steps およびチェック期間としての as long as input stays 0:最初のプロパティと同じ理由で、Synchronized の出力をもつ Detector を使用します ([Time steps for input detection] は 6 に指定)。

  3. The output shall equal 1: これは、最初の 2 つの制約が有効なときに検証する条件です。これは、論理 implies ブロックを介してキャプチャされます。ここでは、Within Implies は使用できません。

プロパティ実証

時相要件がモデル化された後、これらに対し Simulink Design Verifier を使用したプロパティ実証が実行できます。

クリーン アップ

例を完了するには、開いているモデルをすべて閉じます。

close_system('sldvdemo_TOBlocks',0);
close_system('sldvdemo_debounce_to',0);