6. 設計
本章ではCADL処理系の設計を述べる。各節では，公開中のリファレンス実装（cadl 0.3）が提供する範囲と，設計意図にとどまり計画段階にある範囲とを分けて記す。フェーズごとの状況は第10章に示す。
6.1 アーキテクチャ
CADL処理系は以下の4つの主要コンポーネントから構成されるよう設計している。
パーサ・型検査器 (Frontend):
CADL記述を解析し，抽象構文木（AST）を生成する。静的型検査により，アクター参照の解決，契約当事者の整合性，パラメータの値域を検査する。cadl 0.3で利用できる。
検証エンジン (Verifier):
AST上で形式検証を実行する。cadl 0.3は，SMTソルバ（Z3 [de Moura & Bjørner, 2008]）による無矛盾性検証，プロトコルのデッドロック検出，モード遷移のグラフ解析を提供する。モデル検査と連続ダイナミクスの到達可能性解析は計画段階である。
コード生成器 (Code Generator):
CADL記述からコードを生成する。cadl 0.3は，Python（ランタイム），Solidity [Solidity Documentation]，OPA/Rego [Open Policy Agent]，Unity C#（SoS-DSL拡張向け，付録E）を対象とし，シミュレータ向けの設定も出力する。ターゲットは付録Dに一覧する。TypeScriptの生成と，SysMLv2 [OMG, 2025] やAADL [Feiler & Gluch, 2012] への変換は計画段階である。
ランタイムモニター (Runtime Monitor):
配備された制度の実行を監視し，契約違反の検出，制度遷移の実行，ログ記録を行う。cadl 0.3はこれらを，独立した監視サービスとしてではなく，生成したランタイムコード内のクラスとして提供する。
以下のパイプラインは，cadl 0.3が提供する段階を示す。
処理パイプライン:
CADL記述 (.cadl)
│
▼
┌──────────────────┐
│ パーサ │ ─── 構文エラー報告
│ 型検査器 │ ─── 型エラー報告
└────────┬─────────┘
│ AST
▼
┌──────────────────┐
│ 検証エンジン │ ─── 検証結果（OK / 反例）
│ - SMT (Z3) │
│ - デッドロック │
│ - モードグラフ │
└────────┬─────────┘
│ AST
▼
┌──────────────────┐ ┌──────────────┐
│ コード生成器 │───▶│ ランタイム │
│ - Python │ │ モニター │
│ - Solidity │ │ - 契約監視 │
│ - OPA / Unity C#│ │ - 遷移制御 │
└──────────────────┘ └──────────────┘
この図は，想定する利用の順序を示す。cadl codegen 自体は型検査を実行するが，検証エンジンは実行しない。したがって，コードを生成する前に，cadl verify を別途実行する必要がある。
6.2 処理系の構成
6.2.1 パーサ
YAMLベースの構文を解析し，CADL固有の制約式・プロトコルステップを追加的に解析する。cadl 0.3では，YAMLローダーが文書構造を読み，Lark [Shinan+] の文法が式の部分言語を解析する。パース結果は型付きASTとして出力される。解析は最初のエラーで停止し，パーサが知らないキーは診断を出さずに読み飛ばす。エラー回復機能を持つPEGベースのパーサは設計意図であり，未実装である。
6.2.2 型検査器
型検査は以下の項目を検査する: (1) アクター参照の存在確認，(2) 契約当事者の重複・不在検出，(3) プロトコルステップの送受信者がアクター定義に一致すること，(4) 情報共有宣言が定義済みのアクターを参照していること，(5) 制度パラメータの値域制約（0 ≤ α, β, λ ≤ 1），(6) cadl 0.3.10からは，SoS-DSL拡張の静的意味論（付録EのE.4節），(7) idと値に関するその他の検査（重複したid，識別子，sharing: の要素，autonomy:，severity:，deadline: / sampling: の値。付録AのA.12節に示す）。情報共有宣言と実際のメッセージ交換との整合性の検査は計画段階である。
6.2.3 その他のコマンド
リファレンス実装は，cadl verify と cadl codegen のほかに，次のコマンドを提供する。
cadl parseはパーサだけを，cadl checkはパーサと型検査器だけを実行する。cadl regime-mapは，6.3節のモードグラフの解析を報告として出力する（テキスト，DOT，JSON）。cadl iec62853は，構文解析した定義からディペンダビリティの要約を作成する。cadl sim-validate，cadl sim-ir，cadl sim-genは，定義を三層のIRに変換し，シミュレータ向けの設定を生成する（付録D）。cadl aiは，LLMのAPIを通じて自然言語の記述からCADLファイルの草案を作成し，それを構文解析して型検査する。
6.3 検証エンジン
検証エンジンは4つの検証手法を統合するよう設計している。リファレンス実装の検証器が実装する検証手法はsmtだけである。各手法についてcadl 0.3が提供する範囲を最右列に示す。
| 検証手法 | 検証対象 | ツール基盤（設計） | リファレンス実装（cadl 0.3） |
|---|---|---|---|
| SMTベース検証 | 契約間の無矛盾性。guaranteeの論理的整合性。 | Z3 [de Moura & Bjørner, 2008], CVC5 [Barbosa+, 2022] | Z3で利用できる: 各契約内および当事者を共有する契約間の無矛盾性，各契約のassumeの充足可能性，遷移条件の排他性。assumeからguaranteeが導かれるかどうかは，情報としてのみ報告する。CVC5は統合していない。 |
| モデル検査 | プロトコルのデッドロック，ライブロック検出。到達可能状態の網羅的探索。 | UPPAAL [Larsen+, 1997], NuSMV [Cimatti+, 2002] | 統合していない。デッドロック検出は構造解析（parallelブロックの分岐間での相互送信，バリアへの到達可能性，フォールバックの循環）で代替している。逐次に書かれたステップは順序付けられており，循環待ちとしては扱わない。ライブロック検出は計画段階である。 |
| 到達可能性解析 | 制度遷移時の安全不変条件の保持。Hamilton-Jacobi到達可能性解析 [Bansal+, 2017]。 | hj_reachability [Stanford ASL] | 統合していない。代わりに，モード遷移グラフ上の到達可能性・行き止まり状態・閉路の解析と，Z3による各安全不変条件の充足可能性検査を利用できる。初期モードは遷移から推定し，出ていく遷移のないモードは失敗として報告する。 |
| 構成的検証 | アクター追加・離脱時の差分検証。既存契約への影響分析。 | 独自実装 | 計画段階である。 |
6.4 ランタイムシステム
ランタイムシステムは，CADL記述から生成されたランタイムコードを実行環境上で監視・制御する。主な機能は以下のとおりである。断りのない記述は設計意図を表す。
契約監視:
各契約のassume/guaranteeの充足を実行時に監視し，違反を検出した場合は定義されたviolationアクションを実行する。cadl 0.3は，assume/guaranteeを検査して違反を記録するモニタークラスを契約ごとに生成する。
制度遷移制御:
モードマップに基づき，環境パラメータの変化に応じた制度遷移を安全に実行する。遷移プロトコルの各ステップを管理し，ロールバック機能を提供する。cadl 0.3は，遷移条件を評価し，切替時に安全不変条件を表明（assert）するモードコントローラを生成する。遷移ステップの管理とロールバックの実行は計画段階である。
メトリクス収集:
定義された評価指標（パフォーマンス，公平性，レジリエンス等）をリアルタイムで計算し，ダッシュボードに表示する。cadl 0.3は，値を記録して目標値と照合するメトリクス収集器を生成する。ダッシュボードは提供していない。
ログ・監査:
全てのプロトコル実行，契約違反，制度遷移をタイムスタンプ付きで記録し，事後分析・説明責任の履行に資する。cadl 0.3のランタイムは，プロトコル実行，違反，モード遷移のタイムスタンプ付きログをメモリ上に保持する。IEC 62853 [IEC 62853:2018] の合意記述データベースとの連携は計画段階である。