1. はじめに

1.1 本文書の目的と範囲

CADL（Contract Architecture Description Language）は，System of Systems（SoS）における制度設計を形式的に記述・検証・配備するためのドメイン固有言語（DSL）である。本文書は，CADLの言語仕様（Version 0.2，ドラフト）として，言語の目的，要求仕様，構文・意味論の定義，処理系の設計方針を示す。

本文書は，ERTLにおけるSoS研究の調査およびSoSアーキテクチャ設計論の検討に基づき，CADLの実装に向けた仕様を整理したものである。

第1章と第2章は言語の目標を述べるものである。リファレンス実装が現時点で提供する範囲は，第10章と付録AのA.12節に示す。

1.2 背景: SoSにおける制度設計の課題

SoSは，独立に運用される複数のシステムが相互に連携し，単独のシステムでは実現できない能力を発現するシステム構成である [Maier, 1998]。[ISO/IEC/IEEE 21841:2019] では，SoSをDirected（統率型），Acknowledged（認知型），Collaborative（協調型），Virtual（仮想型）の4種に分類している。

従来のSoS研究は制御・協調アルゴリズムや技術的最適化に焦点を当ててきたが，ガバナンス・制度設計がシステム全体の振る舞いを構造的に規定する上位層の設計変数として注目されている。しかし，現在のSoS制度設計は自然言語の契約・合意書に依存しており，以下の課題が存在する。

• 曖昧性・矛盾の検出が困難: 自然言語による制度記述では，形式的な無矛盾性検証ができない。
• 制度更新の整合性保証の欠如: 構成システムの追加・離脱に伴う制度更新が手動であり，整合性チェックの工学的手段がない。
• 設計と実装の乖離: 制度の設計意図が実装に正確に反映されているかの検証手段がない。
• 制度のパラメータ化の不在: ガバナンス構造を定量的に操作可能な変数として扱うフレームワークが存在しない。
• 3層統合記述の欠如: 制度（権限構造），プロトコル（協調手順），アルゴリズム（計算手法）を統一的に記述できる言語がない。
• 専門家以外の関与困難: 既存の形式手法やアーキテクチャ記述言語は高度な専門知識を前提としており，学生・企業の実務者・自治体職員・市民が制度設計に主体的に参加することが困難である。

上記の課題に加え，CADLの設計動機として，SoS制度設計を「計算の対象」として扱うことへの根本的な要請がある。以下の3つの目的が，CADLという言語を新たに設計する直接的な動機となっている。

目的1: SoS制度設計を計算機で扱えるようにする

現実世界のSoSでは，制度の多くが人間の暗黙知・慣習・経験則として存在しており，明文化すらされていない場合が多い。例えば，家庭内の家事分担のルール，地域コミュニティの暗黙の合意，組織間の非公式な協力関係などは，関係者の頭の中にのみ存在し，外部から観察・分析することが極めて困難である。

CADLは，こうした暗黙のルールや習慣を含む現実のSoS制度を「モデル化・言語化」し，計算機上のオブジェクトとして操作可能にすることを第一の目的とする。制度が計算機上のデータとして存在することで，以下の操作が可能になる。

• コピー・再利用: ある文脈で有効だった制度設計を別の文脈にコピーし，適応させることができる。例えば，ある家庭の家事分担ルールを別の家庭に移植し，家族構成に合わせて調整する。
• 統合・合成: 複数の部分的な制度記述を統合して，より大きなSoSの制度を構成できる。例えば，配送ロボットの経路制度とデータ共有の制度を統合して，配送データ連携制度を構成する。
• バージョン管理・差分比較: 制度の変更履歴を追跡し，任意の時点の制度に戻すことができる。制度の変更箇所を差分として可視化し，変更の影響範囲を特定する。
• 検索・分類: 蓄積された制度記述のリポジトリから，類似の制度パターンを検索し，再利用候補を推薦する。
• 暗黙知の顕在化: 人間へのインタビューやAIによる観察データの分析を通じて，暗黙のルールをCADL記述として明文化する。これにより，制度の共有・議論・改善のための共通基盤が生まれる。

目的2: SoSの制度違反や矛盾を計算できるようにする

制度が形式的に記述されていれば，その無矛盾性の検証や，実行時の違反検出を計算によって行えるようになる。現状では，制度間の矛盾（例: ある契約では情報共有が義務付けられているが，別の契約ではプライバシー保護のため共有が禁止されている）は，人間が逐一確認するしかなく，SoSの規模が大きくなると見落としが不可避である。

CADLは，制度の矛盾検出と違反監視を計算機の力で自動化することを第二の目的とする。これは以下の2つの側面を含む。

• AIとの融合による設計支援: LLM等のAIが，CADL記述を入力として受け取り，矛盾の検出・修正提案・制度の改善案を自動生成する。自然言語で「このルールとあのルールは矛盾していませんか？」と問いかけると，AIがCADLの形式意味論に基づいて回答する。将来的には，自然言語の要望からCADL記述を自動生成し，形式検証を経て配備するワークフローを実現する。
• 人間の意思決定支援: 制度の矛盾や潜在的な問題を可視化し，人間の制度設計者が情報に基づいた判断を行えるようにする。矛盾の深刻度や影響範囲を定量的に提示し，修正の優先順位付けを支援する。制度変更のシミュレーション（what-if分析）により，変更の影響を事前に把握する。

目的3: SoS制度設計から制御への自動変換・最適化・コード生成

制度設計が形式言語で記述され，検証が完了したならば，その次のステップとして，制度記述から制御ロジック・実行コードを自動生成することが自然な帰結となる。現状では，制度の設計（ポリシー文書）と実装（コード）の間に大きなギャップがあり，設計意図が実装に正しく反映されているかの保証がない。

CADLは，制度記述から実行可能な成果物への変換パイプラインを提供することを第三の目的とする。具体的には以下の変換を想定する。

• 制度から制御ロジックへの自動変換: CADL記述の契約・プロトコル定義から，各アクターの制御ロジック（状態機械，イベントハンドラ，協調プロトコルの実装）を自動生成する。例えば，ロボット配送システムの制度記述から，DISPATCHERの割当アルゴリズムとROBOTの経路追従ロジックのスケルトンコードを生成する。
• 制度パラメータの最適化: 制度パラメータ（α, β, λ等）の値を，シミュレーションまたは数理最適化によって自動チューニングする。環境条件の変化に対して最適な制度パラメータの組み合わせを探索し，モードマップを自動構築する。
• ランタイムコードの生成: 契約の監視コード（assume/guaranteeの充足チェック），プロトコルの実行エンジン，メトリクス収集コードをターゲット言語（Python, TypeScript, Solidity等）で自動生成する。
• アシュアランスケースとの連動: 制度の検証結果をアシュアランスケース（安全性論証）の証拠として自動組み込みし，IEC 62853の合意記述データベースへのエクスポートを行う。

横断的特徴: 誰でも理解できる制度記述言語

上記3つの目的を貫く横断的な特徴として，CADLは「学生から企業の実務者，自治体職員，地域の住民まで，誰でも制度記述の意図を理解し，制度設計に参加できる」ことを重視する。SoSの制度設計は，技術者だけでなく多様なステークホルダが関与するプロセスであり，制度を記述する言語がごく一部の専門家にしか読めないのであれば，制度設計の民主化は実現しない。

この万人理解性を実現するため，CADLは以下のアプローチを採る。

• YAMLベースの宣言的構文: プログラミング経験がなくても構造を直感的に把握できるインデントベースの記述を採用する。JSON/XMLに比べて「読める」構文を優先する。
• 自然言語に近い語彙: authority（権限），responsibility（責任），incentive（インセンティブ）など，制度の概念をそのまま反映した語彙を用いる。専門的な形式手法の記法を極力隠蔽する。
• 段階的記述レベル: (1) 概要レベル（自然言語に近い記述，AIによる自動生成の入口），(2) 設計レベル（パラメータと制約の定義），(3) 検証レベル（形式的なassume-guarantee記述）の3段階を設け，利用者の専門性に応じた参加を可能にする。
• ビジュアライゼーション: CADL記述からダイアグラム（権限構造図，プロトコルシーケンス図，モードマップ）を自動生成し，非技術者でも制度の全体像を視覚的に把握できるようにする。
• AI支援による敷居の低減: LLMを介した自然言語でのCADL記述生成・修正・説明機能により，「CADLの構文を知らなくても，やりたいことを自然言語で伝えれば制度が記述される」環境を提供する。

これら3つの目的と万人理解性の横断的特徴を統合すると，CADLが目指すビジョンは「現実世界の制度を誰でも理解できる形で言語化し，計算によって検証・改善し，自動的に実行可能な形に変換する」という，制度設計のエンジニアリングサイクルの確立である。これは，ソフトウェア工学におけるモデル駆動開発（MDD）の考え方を，SoSの制度設計領域に拡張し，同時にその参加者を専門家から社会全体へ広げたものと位置づけることができる。

1.3 用語集

本文書では多くの専門用語を使用する。以下に，主要な用語を分野別に整理し，専門知識を持たない読者にも理解できるよう，平易な説明と具体例を添えて解説する。このほかの用語（ρ，κ，IR，ライフサイクル，シミュレータにおけるα/β/λの意味）は，用語集のページを参照されたい。

1.3.1 基本概念

用語	説明	具体例
SoS（System of Systems）	それぞれ独立に動いている複数のシステムが連携して，1つのシステムだけでは実現できない大きな目的を達成する仕組み。	複数の宅配会社のロボットが互いに連携して街全体の配送を効率化するシステム。各ロボットは独立に動くが，全体として最適な配送網を実現する。
CADL（Contract Architecture Description Language）	本文書で定義する制度記述言語。SoSにおける「誰が何の権限を持ち，どう協力し，どんなルールに従うか」を，コンピュータが理解できる形で書き下すための言語。	家庭の家事分担ルールから大規模な都市交通システムのガバナンスまで，幅広い「制度」をCADLの記述対象とする。
制度（Institution）	人やシステムの間の「ルール・権限・役割分担・報酬の仕組み」の総称。法律や契約のような明文化されたものから，家庭内の暗黙のルールまで含む。CADLでは，制度を権限構造・情報共有・インセンティブの3つの側面で記述する。	「子どもは夕食前に家事を終える」「完了したら100円もらえる」というルールは，家庭内の制度の一例。
アクター（Actor）	SoSに参加する主体（人間，ロボット，AIシステム，組織など）。それぞれが役割と能力を持ち，制度のルールに従って行動する。	配送システムでは，ロボット・配車係・お客さんがそれぞれアクター。
ステークホルダ（Stakeholder）	制度設計に関心を持つすべての関係者。制度に直接参加するアクターだけでなく，制度の影響を受ける人々や，制度を監督する立場の人も含む。	配送システムでは，利用者・配送会社・自治体・周辺住民などがステークホルダ。

1.3.2 制度設計の用語

用語	説明	具体例
契約（Contract）	アクター間の「約束事」を形式的に書いたもの。誰が何を保証し，どんな前提条件のもとで有効かを明確にする。CADLではassume-guarantee形式で記述する。	「ロボットが正常に動いている限り（前提），配送は約束時間の1.2倍以内に届く（保証）」
Assume-Guarantee（前提-保証）	契約の基本構造。「もしこの前提条件（assume）が満たされるなら，この保証（guarantee）を約束する」という形式。前提が崩れた場合，保証は免除される。	assume: 「道路が80%以上通行可能」 / guarantee: 「配送成功率95%以上」
権限構造（Authority Structure）	「誰が何を決める権限を持つか」の構造。集中的（1人が決定）から分散的（全員で合議）まで，beta（β）パラメータで程度を表す。	β=0.8: 配車係がほぼ全て決定 / β=0.2: 各ロボットが自律的に判断
インセンティブ（Incentive）	アクターの行動を促すための「報酬と罰則の仕組み」。良い行動には報酬を，悪い行動には罰則を与えることで，全体として望ましい結果を実現する。lambda（λ）パラメータでその強さを表す。	「時間通り配達: +ボーナス」「遅配: -基本料金の50%」。λが大きいほど報酬/罰則の影響が強い。
プロトコル（Protocol）	アクター間の「やりとりの手順」を時間的な制約付きで定めたもの。誰が誰に何を送り，どんな順番で処理するかを記述する。	(1)顧客が注文→(2)配車係がロボットを割当→(3)ロボットが配達→(4)顧客に通知，という一連の手順。
SLA（Service Level Agreement）	サービス品質保証契約。サービスの提供者と利用者の間で「どの程度の品質を保証するか」を数値で取り決めたもの。	「データの遅延は5秒以内」「稼働率99.9%以上」「配送時間は約束の1.2倍以内」
義務（Obligation）	アクターが「必ずやらなければならないこと」。契約上の責任であり，違反すると罰則が発生する場合がある。	「データ提供者は精度95%以上のデータを維持する義務がある」

1.3.3 制度パラメータ

CADLでは，制度の特性を定量的なパラメータとして表現する。これにより，制度の「程度」を数値で調整・最適化できるようになる。

パラメータ	意味	具体例
α（アルファ） 情報共有度	情報をどの程度共有するかを表す。0に近いと情報を制限（プライバシー重視），1に近いと全員に公開。	α=1.0: 家族全員がスケジュールを閲覧可能 / α=0.4: IoTデータはメタデータのみ共有
β（ベータ） 意思決定の集中度	意思決定がどの程度集中しているかを表す。1に近いと1人（中央）が決定，0に近いと全員で分散的に決定。	β=0.8: 配車係が集中的に経路を決定 / β=0.2: 各データ提供者が自分のデータ公開を自律的に決定
λ（ラムダ） インセンティブ強度	報酬・罰則がどの程度行動に影響するかを表す。0に近いとインセンティブの影響が弱く，1に近いと強い。	λ=0.6: お小遣いが行動にそこそこ影響 / λ=0.9: 市場メカニズムで強く制御

1.3.4 制度の動態に関する用語

用語	説明	具体例
運用モード（Regime）	ある時点で有効な「制度の設定一式」のこと。環境条件が変わると，最適なモードも変わる。	平常時モード: 配車係が集中管理 / 障害時モード: 各ロボットが自律判断
モードマップ（Regime Map）	「どの環境条件のときに，どのモード（制度設定）が最適か」を表す地図のようなもの。環境パラメータの空間を領域に分割し，各領域に最適な制度を対応付ける。このパラメータ空間上の地図は概念であり，その構築支援は計画段階である。cadl regime-map コマンドが報告するのはこれより狭く，モード名と遷移からなるグラフである。	障害率が低く通信遅延が小さい→集中管理モード / 障害率が高いか通信遅延が大きい→分散自律モード
制度遷移（Regime Transition）	環境条件の変化に応じて，あるモードから別のモードへ切り替えること。切替中も安全性（衝突回避など）を保証する必要がある。	通信遅延が300msを超えたら，集中管理から分散自律に切り替える。切替中も「衝突なし・注文紛失なし」を維持。
安全不変条件（Safety Invariant）	どのような状況でも「絶対に破ってはならない条件」。制度が切り替わる途中でも，この条件は常に満たされなければならない。	「ロボット同士は衝突しない」「注文データは紛失しない」

1.3.5 検証・コード生成の用語

用語	説明	具体例
形式検証（Formal Verification）	コンピュータを使って，制度記述について，定めた性質（矛盾がないことなど）が成り立つかどうかを数学的に検査すること。人間のレビューだけでは見逃しがちな矛盾を自動的に発見できる。	「2つの契約の条件が矛盾していないか」（契約の無矛盾性）はSMTソルバで検査し，「プロトコルがデッドロックしないか」は構造解析で検査する（6.3節を参照）。
矛盾検出（Contradiction Detection）	制度記述の中に互いに矛盾するルールが含まれていないかを検出すること。例えば，ある契約ではAさんに権限があるのに，別の契約ではBさんに同じ権限がある，といった矛盾。	「同じ時間帯に2つの家事が割り当てられている」「プライバシー制約とデータ公開要件が矛盾」
モデル検査（Model Checking）	システムの取りうる全ての状態を網羅的に調べて，望ましくない状態に到達しないかを検証する手法。	「制度遷移中に，ロボットが衝突する状態に到達する可能性がないか」を全パターン確認。
コード生成（Code Generation）	CADLの制度記述から，実際に動くプログラムコード（Python, TypeScript等）を自動的に生成すること。制度の「設計図」から「実装」を自動的に作る。	配送SLAの契約記述から，配車アルゴリズムのスケルトンコードと，SLA違反を監視するモニターコードを自動生成。
反応型合成（Reactive Synthesis）	仕様（「こう振る舞ってほしい」という要求）から，その仕様を満たす制御プログラムを自動的に合成する手法。	AI安全契約の仕様から，「有害な行動を必ず防ぎ，不確実な場合は人間にエスカレーションする」制御器を自動合成。
ランタイム監視（Runtime Monitoring）	制度が実際に運用されている間，契約の条件が守られているかをリアルタイムで監視すること。違反を検出したら警告や対策を実行する。	配送中に「配送時間 <= 約束時間×1.2」を常時チェックし，超過しそうなら再割当を実行。

1.3.6 SoS分類と関連規格

ISO/IEC/IEEE 21841:2019では，SoSを管理構造の違いにより以下の4種に分類している。CADLはこれら4類型のいずれも記述対象とする。

用語	説明	具体例
D-SoS（Directed SoS / 統率型）	中央の管理者が全体を統率するSoS。各構成システムは管理者の指示に従う。最も集中的な管理構造。	軍の指揮命令系統。司令部が全部隊の行動を統制する。
A-SoS（Acknowledged SoS / 認知型）	中央の管理者は存在するが，各構成システムにもある程度の自律性がある。管理者と構成システムが協議しながら運用する。	ロボット配送システム。配車係が全体を管理するが，各ロボットも局所的な障害回避は自律的に行う。
C-SoS（Collaborative SoS / 協調型）	中央の管理者はおらず，対等な立場の構成システムが自発的に協力する。合意形成で意思決定する。	家族のルール作り。家族会議で話し合って決める。マンション管理組合の運営。
V-SoS（Virtual SoS / 仮想型）	明確な管理構造がなく，構成システムが偶発的に連携するSoS。全体としての目的が明示されていないこともある。	インターネット全体。個々のサービスは独立に運営されるが，結果として巨大なエコシステムを形成。
五層フレームワーク	SoS設計を5つの階層に分類する枠組み[Shimoyama & Matsubara, 2026]。(1) 目的（Policy），(2) 制度・ガバナンス（Governance），(3) 制御・協調（Control），(4) 実行・運用（Execution），(5) 環境・外乱（Environment）からなる。CADLは主に第2層と第3層を記述する。CADL自身の3層との対応は2.2節に示す。	Policy: 「安全最優先」 → Governance: 「衝突回避ルール」 → Control: 「経路計画」 → Execution: 「モーター制御」
IEC 62853	オープンシステムディペンダビリティの国際規格 [IEC 62853:2018]。システムのディペンダビリティを継続的に確保するための合意形成・説明責任・変化対応のプロセスを定義する。CADLはこの規格との連携を考慮している。	制度変更時の合意形成プロセスや，障害対応時の説明責任の仕組みをCADLで記述する。