付録 A — 用語集
本書で使う用語を、分野ごとにまとめます。右の列は、その用語を説明している本書の節です。仕様書の用語集は、本書で使わない用語も含めて用語集にあります。
A.1 SoS の概念
| 用語 | 意味 | 本書の節 |
|---|---|---|
| SoS（System of Systems） | それぞれが独立して運用される複数のシステムが集まって、どのシステムも単独では果たせない目的を果たしている状態 | 1.1、1.2 |
| Maier の 5 条件 | ある対象を SoS と呼べるかを判定する 5 つの条件：運用上の独立性、管理上の独立性、地理的分散、創発的振る舞い、進化的発展 [1] | 1.3 |
| 運用上の独立性 | SoS 全体が止まっていても、各構成要素が単独で動くこと。Maier の条件 (1) | 1.3 |
| 管理上の独立性 | 各構成要素が、別の所有者や意思決定者を持つこと。Maier の条件 (2) | 1.3 |
| 創発的振る舞い | 全体が、どの構成要素にも単独ではできないことをすること。Maier の条件 (4) | 1.3 |
| SoS の類型 | 中央の指揮権の強さによる 4 つの分類（Directed、Acknowledged、Collaborative、Virtual）[2] [3]。CADL ファイルでは type: に書く | 1.4、3.3 |
| Directed（統率型） | 強いトップダウンで集中的に管理する SoS | 1.4 |
| Acknowledged（認知型） | SoS 全体の指揮権が定まっているが、各構成システムが所有権と独自の管理を保つ SoS。本書のロボット配送はこの類型としてモデル化する | 1.4 |
| Collaborative（協調型） | 単一の指揮権がなく、共通の取り決めを介して自発的に協力する SoS | 1.4 |
| Virtual（仮想型） | 中央の管理も合意された目的もなく、調整が自然に生じる SoS | 1.4 |
ディスパッチャ（DISPATCHER） | 本書のロボット配送で、配送をロボットに割り当てる中央の管制 | 1.1、3.4 |
A.2 CADL の構造の層
| 用語 | 意味 | 本書の節 |
|---|---|---|
| CADL（Contract Architecture Description Language） | 複数のシステムが守るべき決まりを、実装コードとは別の 1 つのファイルに書くための記述言語。YAML の形式で書く | 1.6 |
| 構造の層 | SoS に何が存在するかを書く部分。actors:、contracts:、protocols: | 1.6、3.2 |
アクター（actors:） | SoS を構成する主体。ROBOT[1..N] のように範囲を付けると、同じ種類のアクターの集まりを表す | 3.4 |
ROBOT[*] / ROBOT[i] | アクターの集まり全体と、そのうちの 1 つを指す書き方。ROBOT[i].battery はその属性 | 3.4 |
自律性（autonomy） | アクターの自律性の程度（low / medium / high）。説明のためのラベルで、ツールは検査しない | 3.4 |
契約（contracts:） | アクターの間の合意。この種類の合意を結ぶ、というクラスの記述 | 3.5 |
当事者（parties） | 契約に加わるアクター | 3.5 |
| assume-guarantee 形式 | 前提（assume）が満たされている限り、当事者が保証（guarantee）を守る、という契約の書き方。前提が崩れれば保証の義務はない | 3.5 |
インセンティブ（incentives:） | 報酬と罰則。lambda（λ）はその強さ、rules は誰に何をどういうときに与えるか | 3.5 |
authority: / beta（β） | 誰が決めるか、決定がどれだけ中央に集まっているか。本書の題材では使わない | 3.5 |
information: / alpha（α） | 情報をどれだけ共有するか。本書の題材では使わない | 3.5 |
プロトコル（protocols:） | アクターの間のやり取りの手順。trigger、precondition、steps、postcondition で書く | 3.6 |
| ステップ | プロトコルの 1 つの手順。A -> B : m はメッセージの送信、A : f(x) は A 自身の計算 | 3.6 |
| 運用モード（regime） | SoS の運用のしかたの切り替え（例：集中と分散）。切り替える条件は最上位の transitions: に書く。本書では使わない | 3.3 |
A.3 規範の層（SoS-DSL 拡張）
| 用語 | 意味 | 本書の節 |
|---|---|---|
| 規範の層 | SoS で何が起こるべきかを書く部分。契約の中の lifecycle: と monitors: | 1.6、3.2 |
| SoS-DSL 拡張 | CADL に lifecycle: と monitors: を加える拡張。使うファイルは extensions: に sos-dsl: 0.1 と書く | 1.6、3.3 |
| 契約インスタンス | 注文 1 件ごとに作られる、契約の 1 つの実体。ライフサイクルに従って状態を移る。作るのは契約を動かす側のアプリケーション | 3.7 |
ライフサイクル（lifecycle:） | 契約インスタンスがたどる状態機械 | 3.7、5.3 |
初期状態 / 終わりの状態（initial / terminal） | インスタンスが作られたときの状態と、それ以上移らない状態 | 3.7 |
遷移（transitions） | インスタンスが from の状態にあり、on: のイベントが起き、when: が成り立つと、to の状態へ移る規則 | 3.7 |
イベント（on:） | 遷移を起こすきっかけ。"A -> B : m" の形はメッセージが送られたとき、条件式はそれが成り立ったときに起きる | 3.7 |
期限（deadline:） | インスタンスが from の状態に入った時刻から数えた時間の上限。5s のように整数と単位で書く | 3.7 |
on_violation: | 期限に間に合わなかったときの扱い。transition: は移り先の状態の名前（遷移の id ではない）、severity: は違反の重さ | 3.7 |
| 違反 | 期限切れ、または監視ルールの条件が成り立ったこと。記録され、指定があればインスタンスが強制的に状態を移る | 3.7、3.8 |
重さ（severity） | 違反の重さ。Minor、Major、Critical のどれかで、省略すると Major | 3.7 |
監視ルール（monitors:） | 契約インスタンスが動いている間に見張る規則 | 3.8、5.3 |
observe | 監視ルールが読む値。宣言したアクターの属性、メッセージの名前、time、state のどれか | 3.8 |
sampling | 監視ルールを評価する時。periodic(500ms) は一定の間隔、event はイベントが届くたび（省略時） | 3.8 |
rule | 違反とみなす条件。式を文字列で書く | 3.8 |
on_match: | 監視ルールの条件が成り立ったときの扱い。violation: は記録する違反の名前、transition: は移り先の状態 | 3.8 |
予約語 state / now / request | 条件式の中で、インスタンスの現在の状態、現在時刻、インスタンスを作った要求を表す名前 | 3.8 |
A.4 ツールチェイン
| 用語 | 意味 | 本書の節 |
|---|---|---|
| ツールチェイン | CADL ファイルから検査結果、IR、図、コード、実行結果を作る一連のツール | 2.1 |
cadl check | 構文、型、SoS-DSL の静的な規則を検査するコマンド。誤りはエラー、推奨に反する書き方は警告として報告する | 3.9 |
cadl verify | cadl check に加え、SMT ソルバで前提と保証の矛盾や、プロトコルのデッドロックを検査するコマンド | 3.9 |
| SMT ソルバ / Z3 | 論理式が同時に成り立つかを判定するプログラム。cadl verify は Z3 [8] を使う | 2.1、3.9 |
| IR（中間表現、Sim-IR） | CADL ファイルの内容を 3 層（institution / protocol / algorithm）の JSON にしたもの。cadl sim-ir が出力し、以降のツールはこれを読む | 2.1、7.6 |
コード生成（cadl codegen） | IR から実行可能なコードを作ること。--target で生成先（python、solidity、opa、unity-csharp）を選ぶ | 7.3、7.6 |
| e2e スクリプト | cadl_repo/scripts/sos_dsl_handson_e2e.sh。検査、IR の出力、C# の生成、Unity プロジェクトへの配置をまとめて行う | 7.3 |
| Python 参照ランタイム | IR を直接読み込み、契約インスタンスの状態の移り変わりを再現する手書きのインタプリタ（engine.py）。生成された C# の答え合わせに使う | 7.5、7.6 |
multi_robot_demo | 参照ランタイムで 5 台のロボットを決まった筋書きで動かすデモ。--summary で終わりの状態の表、--log で NDJSON のトレース、--ir で自分の IR を使う | 7.2、7.9 |
| NDJSON トレース | 1 行に 1 つの JSON オブジェクトを書いたイベントの記録 | 7.9 |
| cadl-explorer | CADL の編集と検査、状態機械の図の描画をする Streamlit のアプリ | 6.3 |
| Lifecycle View | cadl-explorer の Contract Lifecycle ページが描く、ライフサイクルの図 | 6.2、6.4 |
A.5 シミュレータ
| 用語 | 意味 | 本書の節 |
|---|---|---|
cadl-raspimouse-simulator | Unity プロジェクト、Go の arbitrator、Python 参照ランタイムをまとめたシミュレータのリポジトリ | 2.2 |
| ContractRuntime | 生成された C# の契約ランタイム。インスタンスの登録、イベントの配送、期限と監視ルールの評価をする | 7.6 |
ContractRuntimeHost | シーンに 1 つ置く部品。ランタイムを保持し、毎フレーム評価させ、イベントを Console に書き出す | 8.2、8.4 |
ブリッジ（PilotContractBridge） | ロボットごとに 1 つ付ける部品（Unity の MonoBehaviour）。ロボットの状態の変化を観測し、契約のイベントに変換する | 8.2、8.4 |
Pilot_CSoS | ロボットの制御コード。経路の追従、配送の申し出、配達をする。契約のことは何も知らない | 2.1、8.4 |
| arbitrator | Go で書いた配送の割り当て役。NATS で配送を配り、申し出の早い順にロボットに任せる | 8.2、8.4 |
| NATS | ロボットと arbitrator の間のメッセージをやり取りする仕組み（メッセージブローカ） | 8.2 |
| C-SoS | シミュレータの動作モードの名前（Collaborative SoS の略）。CADL ファイルの type: とは関係しない | 2.2 |
cadl_config.json | 道路網（11 ノード、17 エッジ）、ロボット台数、NATS の設定。arbitrator と Unity の両方が読む | 8.4 |
番号付きの文献は付録 Dにあります。