SpecForge – フォーマル仕様作成プラットフォーム

駆け足ツアー このセクションでは、実践的な例を通してSpecForgeの主な機能について簡単に紹介します。Lilo言語で仕様を記述し、SpecForgeのVSCode拡張機能を使用して分析する方法を探ります。 Lilo言語：簡単な紹介 Liloは、ハイブリッドシステム向けに設計された、式ベースの時相仕様言語です。主な概念は以下の通りです。 プリミティブ型：Bool、Int、Float、String 演算子：標準的な算術演算（+、-、*、/）、比較演算（==、<、>など）、論理演算子（&&、||、=>） 時相演算子：Liloの際立った特徴は、豊富な時相論理演算子です。 always φ：φはすべての未来の時点で真である eventually φ：φはある未来の時点で真である past φ：φはある過去の時点で真であった historically φ：φはすべての過去の時点で真であった これらの演算子は時間間隔で修飾できます。例えば、eventually[0, 10] φは、φが10時間単位以内に真になることを意味します。さらに多くの演算子が利用可能です。 システム： Lilo仕様はシステムに整理され、以下のものをグループ化します。 signals：時間変化する入力値（例：signal temperature: Float） params：時間変化しない非時相パラメータ（例：param max_temp: Float） types：構造化データ定義のためのカスタム型 definitions：再利用可能な定義とヘルパー関数 specifications：システムに対して満たされるべき要件 システムファイルは、system temperature_control のようなシステム宣言で始まり、そのシステムすべての宣言を含みます。言語の詳細については、Lilo言語の章を参照してください。 実行例 温度制御システムを実行例として使用します。この例のプロジェクトはリリースで入手可能です。このシステムは温度と湿度センサーを監視し、値が安全な範囲内に収まることを保証する仕様を備えています。 system temperature_sensor // 温度監視 specifications // この仕様は温度センサーシステムの安全要件を定義します 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 // 温度が正常範囲内の場合に湿度が妥当であるべき spec humidity_correlation = always ( (temperature >= 15.0 && temperature <= 35.0) => (humidity >= 20.0 && humidity <= 80.0) ) // 緊急状態 - 温度がクリティカルしきい値を超える spec emergency_condition = temperature < 5.0 || temperature > 45.0 // 回復仕様 - 緊急状態の後、システムは安定すべき 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 Notebook内から行うことができます。ここではVSCode内で直接分析を実行します。VSCodeガイドでは、すべての機能をより詳細に説明しています。 監視（Monitoring） 監視は、データファイルに記録された実際のシステム挙動が仕様を満たしているかを確認します。記録されたトレースデータを提供すると、SpecForgeはそのデータに対して仕様を評価します。仕様選択画面に移動し、監視したい仕様の「Analyse」ボタンをクリックします。ドロップダウンメニューからデータファイルを選択し、「Run Analysis」をクリックします。結果は仕様の分析監視ツリーになります。 結果は仕様全体として一番上に表示されます。その下で、仕様のサブ式の詳細にドリルダウンして、任意の時点で仕様を真または偽にしているものを理解できます。信号にカーソルを合わせると、その時点での結果の説明が表示され、関連するサブ式結果信号のセグメントがハイライトされます。分析は保存できます。「Save Analysis」ボタンをクリックし、保存場所を選択します。その後、この分析ファイルに移動してVSCodeで再度開くことができます。分析は、関連する仕様の下の仕様ステータスメニューにも表示されます。 例示（Exemplification） 例示分析は、満たす挙動を示す例のトレースを生成します。これは以下に役立ちます。 有効なシステム挙動がどのようなものかを理解する 現実的なデータで他のコンポーネントをテストする アニメーションを作成する 例示されたデータが期待通りに動作しない場合、仕様が間違っている可能性があり、修正が必要になることがあります。したがって、例示は仕様作成の補助として使用できます。 反例探索（Falsification） システムのモデルが利用可能な場合、反例探索を使用して、モデルが仕様に従って期待通りに動作するかどうかを確認できます。まず、specforge.toml にファルシファイアを登録する必要があります。例： [project] name = "automatic-transmission" source = "spec" [[system_falsifier]] name = "AT Falsifier" system = "transmission" script = "transmission.py" これが完了すると、ファルシファイアは「Falsify」分析メニューに表示されます。反例となる信号が見つかった場合、監視ツリーが表示され、モデルがどのように間違ったかを理解するのに役立ちます。 エクスポート（Export） エクスポートは、仕様を他のツールで使用できるように他のフォーマットに変換します。例えば、仕様をJSONフォーマットにエクスポートしたい場合は、エクスポートタイプとして.jsonを選択します。 次のステップ このツアーではSpecForgeができることの基本をカバーしました。次の章では、以下についてさらに詳しく説明します。 Lilo言語の完全な説明（Lilo Language） システム定義と構成（Systems） プログラムアクセス用のPython SDK（Python SDK）