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

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

時相演算子

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

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

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

このデバウンス機能は、それを含む Stateflow® チャートでキャプチャします。

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

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

要件 1:

入力が 6 ステップを超えて 1 である場合は、出力は必ず 2 となる。

要件 2:

出力が 2 になってから入力が 5 ステップを超えて 0 である場合は、入力が 0 であり続ける限り、出力は必ず 1 となる。

プロパティの指定

要件 1 を指定するには、まず、入力が 6 ステップを超えて 1 という制約を表現します。これは、Temporal Operator ブロックライブラリの Detector ブロックでキャプチャできます。7 (6 より上の) タイムステップの間、入力値が 1 であることが検出された場合、検出後に入力が 1 のままであれば出力が 2 であることを確認するものとします。Detector ブロックの [同期済み] オプションを使用し、その後に Implies ブロックを使用してこれをキャプチャします。

open_system('sldvdemo_debounce_to/Verify True Output1')

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

open_system('sldvdemo_debounce_to/Verify True Output2')

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

出力が 2 になった後: これはプロパティの有効化条件です。残りの制約をチェックしている間に、過去のいずれかの時点でこの条件が true であったかを確認するものとします。一般的に、このような有効化条件の後には、他の制約を組み合わせて、論理包含における最初の入力を形成し得るような Extender ([有限] または [無限大] を設定) が続きます。
入力が 5 ステップを超えて 0 になり、入力が 0 である限りチェック処理を行う: 最初のプロパティと同じ理由で、[同期済み] 出力設定の Detector を使用します ([入力検出のタイムステップ] は 6)。
出力が 1 になる: 最初の 2 つの制約が真の場合に検証される条件です。これは、論理 Implies ブロックによってキャプチャされます。ここでは、Within Implies ブロックを使用できない点に留意してください。

プロパティ証明

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

クリーンアップ

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

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