UPPAALを深掘りする

「時間」を検証できるモデル検査器 — 時間オートマトンの理論から産業事例、AI時代の発展まで

UPPAALとは

UPPAALは、実時間システム（リアルタイムシステム）のためのモデル検査ツールです。1995年の初リリース以来、スウェーデンのウプサラ大学とデンマークのオールボー大学が共同開発しており、名前は両大学（UPPsala + AALborg）に由来します。開発を主導した Kim G. Larsen、Paul Pettersson、Wang Yi の3氏は、この業績により検証分野で最も権威ある賞のひとつ CAV Award を2013年に受賞しています。

現行の安定版は UPPAAL 5.0（2023年リリース）。グラフィカルなモデルエディタ・シミュレータ・検証器が一体になったGUIと、バッチ検証用のコマンドラインツール verifyta で構成されます。学位授与機関での学術利用は無料（登録制）、企業利用や国立研究機関を含む非学術利用は VeriAal 社経由の商用ライセンスが必要です。

何が特別か：「時間」そのものを検証できる

多くのモデル検査器は「イベントの順序」を検証します。UPPAALが特別なのは、そこに「時刻」を加えられることです。理論的基盤は Alur と Dill が1994年に定式化した時間オートマトン（timed automata）。有限オートマトンに実数値の時計（クロック）を持たせ、「この状態には3秒以上とどまれない」「受信から5ミリ秒以内に応答する」といった制約を、モデルの一部として書けるようにした形式です。

UPPAALはこれを実用向けに拡張し、複数の時間オートマトンをチャネル同期や共有変数で結んだ「ネットワーク」として並行システムを表現します。時間を凍結する urgent/committed ロケーション、有界整数やC風の関数定義など、現実のプロトコルやコントローラを書きやすくする仕掛けが揃っています。「タイムアウト値の選び方ひとつで正しさが変わる」種類のシステム、たとえば通信プロトコルや組込み制御は、この形式でなければ検証できません。

GUIで描く：信号機の例

UPPAALのもうひとつの際立った特徴は、モデルをテキストではなくGUI上のグラフとして直接描くことです。ロケーション（状態）を丸として置き、エッジ（遷移）を矢印で結び、ガード・同期・更新・不変条件をその場に書き込みます。エディタで描いたグラフはそのままシミュレータで手動実行でき、検証器が返した反例も同じグラフ上でステップ再生できます。「描く→動かす→検証する→反例を眺める」が1つの画面で完結する、この一体感が入門しやすさの理由です。

例として信号機を1灯、時間オートマトンで描いてみます。UPPAALのGUIの慣例に合わせて、不変条件を紫、ガードを緑、更新（クロックのリセット）を青で示します。

信号機の時間オートマトン。丸がロケーション（二重丸は初期状態）、紫がそのロケーションに「居られる上限」を定める不変条件、緑がエッジを「渡れる条件」を定めるガード、青がクロックのリセット。たとえば Green には最大45秒しか居られず（x ≤ 45）、40秒を過ぎると（x ≥ 40）いつでも Yellow へ遷移できる。つまり「緑は40〜45秒のどこかで黄に変わる」という非決定性を、2つの制約の組で表現しています。

形式的には

この図は見た目のためのお絵描きではなく、厳密な数学的対象の視覚表現です。時間オートマトンは次の6つ組として定義されます：

\mathcal{A} \;=\; (L,\; \ell_0,\; C,\; A,\; E,\; I), \qquad E \subseteq L \times \mathcal{B}(C) \times A \times 2^{C} \times L, \qquad I : L \to \mathcal{B}(C)

L はロケーション集合、ℓ₀ は初期ロケーション、C はクロック集合、A はアクション集合、E がエッジの集合（出発ロケーション、ガード、アクション、リセットするクロック集合、到着ロケーション）、I が各ロケーションへの不変条件の割り当てです。ガードと不変条件に使えるのは、クロック制約 B(C)（x ⋈ c や x − y ⋈ c の形、⋈ は比較演算子）に限られます。この制限が、無限の実数時間を有限のゾーンに畳み込める（＝検証が停止する）理由です。

ネットワーク化して検証する

1灯だけでは検証する性質もささやかですが、UPPAALの本領はここからです。この信号機をテンプレートとして、南北方向（NS）と東西方向（EW）の2インスタンスを生成し、コントローラとチャネル同期でつなぐと、交差点全体がネットワークになります。そこで初めて意味のある性質が書けます：

安全性：交差する2方向が同時に青になることは、どの実行のどの時点でも起きない。UPPAALでは A[] not (NS.Green && EW.Green) と書きます。

\forall\Box\;\lnot\,\bigl(\mathit{NS.Green} \;\land\; \mathit{EW.Green}\bigr)

応答性（leads-to）：赤になった方向は、いつか必ず青に戻る。UPPAALでは NS.Red --> NS.Green と書きます。全称記号で展開すると次の形です：

\mathit{NS.Red} \;\rightsquigarrow\; \mathit{NS.Green} \;\;\equiv\;\; \forall\Box\,\bigl(\mathit{NS.Red} \;\Rightarrow\; \forall\Diamond\,\mathit{NS.Green}\bigr)

5つの質問形式：仕様の書き方

検証したい性質は、時相論理 TCTL のサブセットである質問（クエリ）言語で書きます。基本は次の5形式＋デッドロック述語だけで、覚えることは驚くほど少なくて済みます。

形式	TCTL記法	読み方	意味
`A[] p`	$\forall\Box\, p$	不変（invariantly）	すべての実行のすべての状態で p が成り立つ（安全性）
`E<> p`	$\exists\Diamond\, p$	到達可能（possibly）	p を満たす状態に到達する実行が存在する
`A<> p`	$\forall\Diamond\, p$	必然（eventually）	どの実行でもいずれ p に到達する（活性）
`E[] p`	$\exists\Box\, p$	潜在的恒常	すべての状態で p が成り立つ実行が存在する
`p --> q`	$p \rightsquigarrow q$	leads-to	p が成り立てば、その後必ず q に到達する（応答性）

例：「A[] not deadlock」（デッドロックしない）、「A[] Train.crossing imply Gate.closed」のように書きます。なお質問のネスト（入れ子）はサポートされず、完全な TCTL より表現力は制限されています。検証が失敗すると反例（エラートレース）が返り、シミュレータ上で再生してシーケンス図として眺められます。

内部の仕組み：ゾーンとDBM

クロックは実数値なので、状態は本来無限にあります。UPPAALは連続的なクロック値の集合を「ゾーン」（x ≦ 5、x - y ≦ 3 のような差分制約で定義される凸多面体）としてまとめ、DBM（差分上界行列）というデータ構造で効率的に表現します。探索は on-the-fly（必要な状態だけ展開）で、それでも本質的な制約である状態爆発に対しては、探索順序の選択・状態空間の圧縮表現・凸包による過大近似などの緩和手段が用意されています。DBMライブラリはオープンソース（GPL-3.0）として公開されています。

産業での実績

UPPAALの事例には「テストでは何年も見つからなかったバグを、モデル検査が特定した」という型の話が多くあります。代表例を挙げます。

同社のオーディオ/ビデオ機器で10年以上使われていたリンクプロトコル（約2,800行のアセンブラ）は、まれにメッセージを失うことが知られていたのに、テストでは原因を特定できませんでした。UPPAALがエラートレースを自動生成してバグの位置を特定し、修正が正しいことも自動証明されました。モデル検査の産業適用を代表する事例です。

有界再送プロトコル（BRP）の検証では、プロトコルの正しさがタイムアウト値の選び方に依存することが示されました。「時間の検証」が飾りではなく本質であることを示した古典です。

ESA の Herschel/Planck 衛星ソフトウェア（Terma社開発）のタスクスケジューリング解析に適用。後続研究では統計的モデル検査（SMC）により、23時間かかっていた解析が23秒になり、従来は手に負えなかったケースも検査可能になりました。

Mecel社のギアボックスコントローラ（試作機）では要求から導いた46性質を自動証明（1998）。ペースメーカーの安全性検証（ペンシルベニア大、Boston Scientific仕様ベース）や、デンマークの分散連動装置の検証など、鉄道・医療でも使われています。2025年の系統的レビュー（188論文）では、鉄道・サイバーセキュリティ・組込み・医療など18分野超で現役の適用が確認されています。

日本での状況

日本にも確かな足跡があります。JAXA は2003年頃、月周回衛星 SELENE と超高速インターネット衛星 WINDS の姿勢制御ソフトウェアの独立検証（IV&V）に UPPAAL を適用しました。要求がデータフロー図と時間制約で書かれており、時間オートマトンのネットワークがちょうど適合したためです。

教材としては、NII のトップエスイー実践講座から日本初の解説書『UPPAALによる性能モデル検証』（長谷川哲夫・田原康之・磯部祥尚、近代科学社、2012）が出ており、公式チュートリアルの日本語版PDFも公開されています。商用面では NTTデータオートモビリジェンス研究所（旧キャッツ/ZIPC）が国内代理店を務めています。一方で Qiita・Zenn などの草の根記事はごく少なく、日本語の実践情報はまだ薄いのが現状です。

ツールファミリーとAI時代の発展

UPPAALには長年の拡張ファミリーがあります：SMC（統計的モデル検査：確率・性能をシミュレーションで推定）、Tiga（時間付きゲームによるコントローラ合成）、Stratego（ゲーム＋機械学習による最適戦略の合成）、TRON（実機のオンライン適合性テスト）など。このうち SMC・Tiga・Stratego の機能は UPPAAL 5 で本体に統合されました（TRON は独立ツールのままです）。

特に Stratego は「学習と検証の融合」の最前線です。強化学習に安全シールド（危険な行動を形式的に遮断する層）を合成して組み合わせる研究や、デンマークの実交差点データで信号制御を学習し時間損失を22%以上削減した事例があります。LLM との接続はまだ萌芽期で、自然言語要求を UPPAAL SMC の質問へ形式化するエージェントパイプライン（精度77.8%）が2026年に報告された段階です。

他の形式手法との使い分け

モデル検査・仕様記述のツールはそれぞれ得意分野が異なります。一行で整理すると：

ツール	こういうときに
UPPAAL	タイミング・デッドライン・タイムアウトが正しさを左右する（組込み制御、通信プロトコル）
SPIN	時間なしの並行プロトコル・デッドロック・競合状態
TLA+	分散システムの設計（レプリケーション、合意、障害時の振る舞い）
VDM / B	データと操作の契約（事前・事後条件、不変条件）を中心とした仕様記述
Alloy	構造的な制約（データモデル、設定、権限）の探索と小さな反例

本サイトの主軸である VDM とは補完関係にあります。VDM が「データが何であり、操作は何を保証するか」を書く言語だとすれば、UPPAAL は「それがいつ起きるか、間に合うか」を検証する道具です。エージェント間の契約は VDM で、時間制約が本質になる部分（タイムアウト、リトライ、スケジューリング）はUPPAALで、という組み合わせが自然です。

限界も正直に

扱えるデータは有界のみ。整数は既定で -32768〜32767 の範囲で、無限・無界のデータ構造は表現できません。豊富なデータ型の仕様記述は VDM 等の領域です。

検証するのはモデルであって実装コードそのものではありません。モデルと実装の対応づけは人間の仕事として残ります（テスト生成やTRONによる適合性テストが橋渡しになります）。

状態爆発は本質的な制約です。クロックや並行プロセスが増えるとメモリと時間が急増します。近似・削減オプションはありますが、モデルの抽象化スキルが求められます。

質問言語はネストできず、完全な TCTL より表現力が制限されています。

まずは触ってみる

UPPAALはGUI一体型で、モデル検査器の中では入門しやすい部類です。公式チュートリアルの定番例題は「踏切（train-gate crossing）」と「Fischer の相互排除」。エディタでオートマトンを描き、シミュレータで手で動かし、検証器に質問を投げて反例をシーケンス図で眺める、という一巡を1日で体験できます。学術利用なら無料でライセンスを取得できます。