反例探索
反例探索とは、与えられた仕様に違反するシステムへの入力を発見することです。一般に、反例探索問題は以下の要素から構成されます。
- コンテキスト：システムモデル（入力信号と出力信号の関係）
- 入力：システムの入出力信号に関する仕様
- 出力：仕様違反を引き起こす入力信号
反例探索ツールは以下のように分類されます。
- System-Dependent（システム依存型）： 特定のシステムモデルに対して使用できる falsifier。
- System-Independent（システム非依存型）： 任意のシステムモデルで使用できる falsifier。つまり、ユーザーがモデルを選択できます。
- Black-box（ブラックボックス型）： falsifier がモデルの入出力のみを通じてモデルを理解するシステム非依存型の falsifier。
- Glass-box（グラスボックス型）： falsifier がモデルの実行ハンドルではなくモデルの記述を受け取るシステム非依存型の falsifier。
SpecForge は現在、System-Dependent 型の falsifier とのインターフェースのみをサポートしています。つまり、ユーザーはモデルを固定し、そのモデルに特化した falsifier を提供するスクリプトを用意する必要があります。
以下では、このような falsifier を SpecForge と連携させるためのセットアップ方法の詳細を説明します。完全な例については、SpecForge releases ページに含まれている 反例探索のサンプルプロジェクトを参照してください。
- F16 航空機モデル：16 個の連続変数と区分的非線形微分方程式を用いてモデル化された F16 航空機 のモデルで、中核部分は地面衝突回避システムです。
- オートマチックトランスミッション（MATLABが必要）：2つの入力（スロットルとブレーキ）を持つ車両のギア選択モデルです。モデルの他の要素には速度や回転数が含まれます。このモデルは MATLAB ドキュメントの例 に一般的に含まれるものにインスパイアされており、Simulink を用いて実装されています。
反例探索スクリプトの準備
反例探索スクリプトは以下の引数を受け取れる必要があります。
--project-dir： SpecForge プロジェクトディレクトリのパス（lilo.tomlファイルが置かれている場所）--system： falsify するシステムの名前--spec： falsify する仕様の名前--params： JSON 形式のシステムのparamの値--options： スクリプトへの追加オプション
したがって、コマンドは以下のように呼び出されます。
sh scripts/automatic_transmission.sh --system 'automatic_transmission' --spec 'AT6a' --options '{}' --params '{}' --project-dir './spec/'
反例探索スクリプトの出力は以下のいずれかである必要があります。
{ "tag": "Err", "contents": err}{ "tag": "Ok", "contents": { "signal": signal}}
ここで、err は文字列（例：「Couldn’t Falsify」）であり、signal は JSON 形式の 反例探索の結果です。pandas データフレームを使用している場合、これは SpecForge SDK の converters.python_to_api_timeseries 関数を使って取得できます。
Falsifier の登録
lilo.toml ファイルに、falsifier を以下のように登録します。
[[system_falsifier]]
name = "Automatic Transmission Falsifier"
system = "automatic_transmission"
script = "scripts/automatic_transmission.sh"
これにより、システム automatic_transmission に関連付けられた falsifier がスクリプト scripts/automatic_transmission.sh の実行により呼び出せることを SpecForge に伝えます。
反例探索ワークフローの実行
反例探索スクリプトの準備と登録が完了したら、VSCode 拡張機能の easy analysis オプションを使って実行できます。以下のスクリーンショットを参照してください。
