SpecForge早わかり

このセクションは、実際の例を通してSpecForgeの主な機能を素早く紹介します。Lilo言語で仕様を書く方法と、SpecForgeのVSCode拡張機能を使用して解析する方法を探ります。

Lilo言語：概要

Liloは、ハイブリッドシステム向けに設計された式ベースの時相仕様言語です。主な概念は次のとおりです：

基本型：Bool、Int、Float、およびString

演算子：標準的な算術演算子（+、-、*、/）、比較演算子（==、<、>など）、および論理演算子（&&、||、=>）

時相演算子：Liloの特徴的な機能は、豊富な時相論理演算子のセットです：

• always φ：φがすべての未来の時刻で真である
• eventually φ：φがある未来の時刻で真である
• past φ：φがある過去の時刻で真であった
• historically φ：φがすべての過去の時刻で真であった

これらの演算子は時間間隔で修飾することができます。例えば、eventually[0, 10] φは、φが10時間単位以内に真になることを意味します。その他の演算子はこちらをご覧ください。

システム：Lilo仕様はシステムに編成され、以下をグループ化します：

• signal：時間変動する入力値（例：signal temperature: Float）
• param：時間変動しない非時間パラメータ（例：param max_temp: Float）
• type：構造化データのためのカスタム型
• def：再利用可能な定義とヘルパー関数
• spec：システムが満たすべき要件

システムファイルはsystem temperature_controlのようなシステム宣言で始まり、そのシステムのすべての宣言が含まれます。

言語の包括的なガイドについては、Lilo言語の章を参照してください。

実行例

温度制御システムを実行例として使用します。このサンプルプロジェクトは、リリースで入手できます。このシステムは温度と湿度のセンサーを監視し、値が安全な範囲内に保たれることを保証する仕様を持っています：

system temperature_sensor

// Temperature Monitoring specifications
// This spec defines safety requirements for a temperature sensor system

import util use { in_bounds }

signal temperature: Float
signal humidity: Float

param min_temperature: Float
param max_temperature: Float

#[disable(redundancy)]
spec temperature_in_bounds = in_bounds(temperature, min_temperature, max_temperature)

spec always_in_bounds = always temperature_in_bounds

// Humidity should be reasonable when temperature is in normal range
spec humidity_correlation = always (
  (temperature >= 15.0 && temperature <= 35.0) =>
  (humidity >= 20.0 && humidity <= 80.0)
)

// Emergency condition - temperature exceeds critical thresholds
spec emergency_condition = temperature < 5.0 || temperature > 45.0

// Recovery specification - after emergency, system should stabilize
spec recovery_spec = always (
  emergency_condition =>
  eventually[0, 10] (temperature >= 15.0 && temperature <= 35.0)
)

VSCode拡張機能は、Liloコードの記述、構文強調表示、型検査、警告、仕様の充足可能性などをサポートします：

仕様の解析

システムの仕様を記述したら、SpecForge VSCode拡張機能はさまざまな解析機能を提供します：

• Monitor：記録されたシステムの動作が仕様を満たしているかチェック
• Exemplify：仕様を満たす例のトレースを生成
• Falsify：モデルに対して、仕様に違反する反例を検索
• Export：仕様を他の形式（.json、.liloなど）に変換
• Animate：仕様の動作を時間経過とともに視覚化

これはVSCode内から直接実行することも、Python SDKを使用してJupyterノートブック内から実行することもできます。ここではVSCode内で直接解析を実行します。VSCodeガイドでは、すべての機能についてさらに詳しく説明しています。

モニタリング

モニタリングは、データファイルに記録された実際のシステムの動作が仕様を満たしているかをチェックします。記録されたトレースデータを提供すると、SpecForgeがそれに対して仕様を評価します。

仕様選択画面に移動し、モニタリングしたい仕様のAnalyseボタンをクリックします。

ドロップダウンメニューからデータファイルを選択した後、Run Analysisをクリックします。結果は仕様の解析モニタリングツリーです：

仕様全体の結果が上部に表示されます。その下では、仕様のサブ式を掘り下げて、任意の時点で仕様が真または偽になる理由を理解できます。任意のシグナルにカーソルを合わせると、その時点での結果の説明を含むポップアップが表示され、サブ式の結果シグナルの関連するセグメントが強調表示されます。

解析は保存できます。保存するには、Save Analysisボタンをクリックし、解析を保存する場所を選択します。その後、この解析ファイルに移動して、VSCodeで再度開くことができます。解析は、関連する仕様の下にある仕様ステータスメニューにも表示されます。

実証化

Exemplify解析は、満足する動作を示す例のトレースを生成します。これは以下のような場合に便利です：

• 有効なシステムの動作がどのようなものかを理解する
• リアルなデータで他のコンポーネントをテストする
• アニメーションを作成する

実証化されたデータが期待どおりに動作しない場合、仕様が間違っている可能性があり、修正が必要です。実証化は、仕様を作成する際の補助として使用できます。

反証化

システムのモデルが利用可能な場合、反証化を使用して、モデルが期待どおり、つまり仕様に従って動作するかどうかを確認できます。

最初に、lilo.tomlに反証器を登録する必要があります。例：

name = "automatic-transmission"
source = "spec"

[[system_falsifier]]
name = "AT Falsifier"
system = "transmission"
script = "transmission.py"

これが完了すると、反証器がFalsify解析メニューに表示されます。反証化シグナルが見つかった場合、モニタリングツリーが表示され、モデルがどこで間違ったかを理解するのに役立ちます：

エクスポート

Exportは、仕様を他のツールで使用するために他の形式に変換します。たとえば、仕様をJSON形式にエクスポートする場合は、Export typeとして.jsonを選択します。

次のステップ

このツアーでは、SpecForgeができることの基本をカバーしました。以下の章では、より詳しく掘り下げます：

• 完全なLilo言語（Lilo言語）
• システムの定義と構成（システム）
• プログラムによるアクセスのためのPython SDK（Python SDK）