このページの内容は最新ではありません。最新版の英語を参照するには、ここをクリックします。

パワー ウィンドウ コントローラー時相プロパティ

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

時相演算子

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

パワー ウィンドウ コントローラー

パワー ウィンドウ コントローラーは、運転席と助手席の命令に対し、ウィンドウを上下に動かすコマンドを発することで応答します。また、障害物やウィンドウ フレームのいずれかの終端への到達にも応答します。

パワー ウィンドウ コントローラーの次の 2 つの要件について考えます。

要件 1 (障害物応答)

障害物が検出されたら、コントローラーは 1 秒間 down コマンドを出す。

要件 2 (オートダウン機能)

運転席の down ボタンが押された時間が 1 秒未満の場合、コントローラーは、終端に達するか運転席の up ボタンが押されるまで down コマンドを出し続ける。

%Model of the power window controller
open_system('sldvdemo_powerwindowController')
open_system('sldvdemo_powerwindowController/control')

プロパティの指定

パワー ウィンドウ検証システムは、コントローラーの動作およびモデル化された要件を指定するパワー ウィンドウ コントローラー モデルへのモデル参照を含む最上位モデルです。

%Model of the top-level verification system
open_system('sldvdemo_powerwindow_vs')

全体的な前提条件: パワー ウィンドウ コントローラーは開放型システムです。そのため、環境制御される入力 obstacle と endstop (ウィンドウ フレームの終端) が任意に発生します。環境を制約するには、コントローラー モデルに 2 つの全体的な前提条件を追加します。

1) obstacle と endstop の入力が同時に true になることはない。

2) obstacle が直後の 1 秒以内に複数回発生することはない。

obstacle の時相の前提には、Detector ブロックを [一定の期間で遅延] の出力タイプ設定で使用し、固定期間 1 秒間 (0.2 サンプル時間で 5 タイム ステップ) をキャプチャします。

% Global Assumptions
open_system('sldvdemo_powerwindow_vs/Global Assumptions')

ここで、障害物応答についての最初のコントローラー要件について考えます。

% Obstacle Response
open_system('sldvdemo_powerwindow_vs/Verification Subsystem2')

ここでは、プロパティの指定に、出力タイプの設定が [一定の期間で遅延] の Detector ブロックを使用します。obstacle を検出したら、4 ステップの固定区間を作成します。Detector の出力タイプが [一定の期間で遅延] の場合、出力作成段階では入力が観測されません。前提がなく obstacle が任意に発生し得る場合、obstacle の中間発生状況すべての観測が必要になる場合があります。これは、拡張時間が [有限] に設定された 4 タイム ステップの Extender ブロックによって実現できます。

ここで、パワー ウィンドウ コントローラーのオートダウン機能について考えます。

わかりやすくするため、このプロパティの指定をより小さく分けて考えます。

1. 最初に考察する時相期間である "運転席の down ボタンが押された時間が 1 秒未満" は、Detector1 でキャプチャしています。0.2 のサンプルレートでは、1 秒の間隔は 5 タイム ステップに分割されます。down 信号が検出されると、Detector1 は、その出力で 5 ステップの固定時相期間を構築します。これは、後で他の制約と組み合わせて使用します。

2. オートダウン機能では、down 信号は 1 秒 (5 タイム ステップ) より長く押すことはできません。したがって、down ボタンが押されてから 5 ステップに達する前に、DriverUp と DriverDown の両方が "true" になるか、両方が "false" になるようにする必要があります。この運転席 neutral と Detector 出力の AND を取ることにより、連続タイム ステップ数が 5 未満まで運転席の down を押すことができるという制約を強制します。

3. また、この期間内に obstacle、EndStop および DriverUp など他の信号が true にならないようにする必要もあります。そうでないと、down ボタンが押されたときにコントローラーが反応できなくなります。これは、NOT(HaltDown) が 5 タイム ステップの間 true になるよう強制することで Detector2 を使用してキャプチャします。Detector2 の出力タイプは [一定の期間で遅延] です。また、[入力検出のタイム ステップ] は 5、[出力持続期間のタイム ステップ] は 1 となっています。

4. 構築したこれらの期間の AND を取ります。

5. オートダウン機能については、コントローラーが down コマンドを与えるタイム ステップ数を制限することは望ましくありません。運転席で再度 up または down コマンドを押したり、障害物やウィンドウ フレームの物理的な終端に到達したりしない限り、コントローラーは down コマンドを与え続けなければなりません。この動作は、[無限大] の延長期間をもつ Extender ブロックと、延長を終了する条件をエンコードする外部リセット信号を使用してキャプチャできます。

6. 最後の Implies ブロックは、上記で構築した時相期間を使用して、この期間中の各タイム ステップでコントローラーの down コマンドが true であるかどうかをチェックします。

この初期プロパティを指定すると、Simulink Design Verifier でのプロパティ証明に利用できます。このプロパティの反例が表示されます。反例では、コントローラーが先に検出した障害物に応答して緊急の down 状態になったときに down コマンドが与えられるシナリオを示します。これを回避するための制約を追加すると、もう 1 つの反例が表示されます。up コマンドが与えられていたときに down ボタンが押されると、オートダウン機能は無効になり、down ボタンが押されている間のみ down コマンドが与えられるようになります。これらの反例を考察してモデルを観測すると、オートダウン機能が有効になるのは、コントローラーが neutral 状態のときに運転手が down ボタンを押したときのみであるというパターンを確認できます。

この制約を取り入れるため、コントローラーの出力を強制的に neutral (up コマンドも down コマンドも true でない) にする状態をオートダウン プロパティの前提条件とします。このプロパティは有効なことが証明されています。

% Valid AutoDown
open_system('sldvdemo_powerwindow_vs/Verification Subsystem3')

プロパティ検証用テスト ケースの生成

プロパティが指定されると、プロパティの証明のほかに、Simulink Design Verifier を実行してプロパティのさまざまな状態を確認するテスト ケースを自動的に生成できます。これは、プロパティの適切な位置にカスタムの Test Objective ブロックを配置して実行します。

たとえば、(上記プロパティに示されるように) Implies ブロックの最初の入力に接続されている信号上に Test Objective ブロックを ("true" の値で) 配置します。テスト生成を実行すると、この Test Objective が満たされ、プロパティにエンコードされたさまざまな制約を確認するテスト ケースを得られます。Simulink Design Verifier は、このテスト ケースをシミュレートするテスト ハーネスも作成できます。ここで、2 つの Detector ブロックの入出力値と No_Cmd を表示するスコープを配置してこのテスト ケースのシミュレーションを行い、プロパティに時相期間が構築される様子を確認できます。

テスト ケースの値を手動で検査すると、指定されたプロパティが意図したように動作するかどうかを確認できます。

この Test Objective ブロックは、プロパティが有効であっても Implies ブロックが true であることが自明ではないシナリオを特定するのに役立ちます。Implies ブロックが true であることが自明なのは、その最初の入力が false であったために出力が true となる場合です。この Test Objective を達成するテスト ケースが得られると、Implies ブロックへの最初の入力が true になるケースが少なくとも 1 つあることがわかります。

この演習では、Simulink Design Verifier で自動生成されたテスト ケースを手動で検査することで、プロパティの指定を検証できます。

クリーン アップ

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

close_system('sldvdemo_TOBlocks',0);
close_system('sldvdemo_powerwindowController',0);
close_system('sldvdemo_powerwindow_vs',0);