社団法人 電子情報通信学会
THE INSTITUTE OF ELECTRONICS,INFORMATION AND COMMUNICATION ENGINEERS

信学技報
TECHNICAL REPORT OF IEICE.

UPPAAL 拡張時間オートマトンの反例に基づく抽象化改良ループによるモデル抽象化手法
長岡 武志†

岡野浩三†

楠本真二†

† 大阪大学大学院情報科学研究科〒 560–8531 大阪府豊中市待兼山 1–3
あらまし

近年，情報システムの高信頼設計においてモデル検査は重要な役割を果たすようになってきている．実時間システムのモデル検査では，モデルの状態数が状態変数やクロック変数に対して指数的に増加し，スケーラビリティに厳しい制限が生じる．本稿では，時間モデル検査ツールである UPPAAL で用いられる拡張時間オートマトンに対する具体的なモデル抽象化手法を提案する．モデル抽象化技法はこのスケーラビリティ改善のための主要な手法として注目を浴びている．本手法では，Clarke らが提案した反例に基づいた抽象化改良ループ CEGAR を適用しており，抽象化から検査までの全ての工程を自動的に行うことが可能である．また，反例によるモデルの再抽象化においては時間オートマトンの検証で用いられるデータ構造 DBM を活用する工夫を行なっている．
キーワード

モデル検査，時間オートマトン，モデル抽象化，CEGAR，UPPAAL

Abstraction of Extended Timed Automata for UPPAAL Based on
Counterexample-Guided Abstraction Refinement LoopTakeshi NAGAOKA† , Kozo OKANO† , and Shinji KUSUMOTO†† Graduate School of Information Science and Technology, Osaka University
Machikane-yama 1–3, Toyonaka City, Osaka, 560–8531 Japan
Abstract In the model checking of the realtime systems, the number of states of models increases exponentlly with the number of the state variables and the clock variables. Such explosion severely limits the scalability of model checking. This paper
proposes a concrete model abstraction technique for extended timed automata used in UPPAAL, a famous model checking tool
for realtime systems. In the proposed technique, the abstraction refinement loop based on the counterexample that Clarke et al.
proposed is applied, and all the processes from the abstraction can be performed automatically. We gives concrete proceduresfor the abstraction loop with utilization of DBM.
Key words Model Checking, Timed Automata, Model Abstraction , CEGAR, UPPAAL

1. ま え が きルが用いられる．時間オートマトンでは， 有限のロケーションと呼ばれる状態に，実数値をとるクロック変数を用いた制約が近年，情報システムの高信頼設計にモデル検査を活用するこ付加されるため，時間オートマトンは無限の状態空間を持つことが強く望まれている．モデル検査手法はシステムを有限の状とになる．モデル抽象化を行わない従来の時間モデル検査では態遷移系として記述し，状態遷移系の全状態を探索することで，時間領域が実質，有限個に押さえられることを利用し有限状態システムが仕様を満たすかどうかを証明する手法である．しのモデルに対し検査を行う．しかし，この状態数はロケーショかし，大規模なシステムに対しては状態数爆発を起こすなど，ンやクロックの個数に対して指数的に増加するため，状態数をスケーラビリティの弱さが課題となっている．モデル検査のス適切に縮小するモデル抽象化手法が必要となる．

ケーラビリティの弱さを改善する手法として，検査する性質ご

本稿では，時間モデル検査ツール UPPAAL [6] で用いられるとに，モデルの状態数を適切に削減するモデル抽象化手法が注

拡張時間オートマトンに対する具体的なモデル抽象化手法を提目されている [1], [2], [7]．

案する．抽象化には有限モデルやハイブリッドオートマトンな一方，実時間システムの動作検証には，有限の状態遷移系にどの抽象化に用いられている「反例に基づいた抽象化改良ルー

実時間制約を付加した時間オートマトン [4], [5] と呼ばれるモデ

プ [1], [3]」を適用しており，抽象化から検査までの全ての工程—1—を自動的に行うことが可能である．
「反例に基づいた抽象化改良•(l, u) −→ (l0 , u0 )∃e = (l, a, g, r, l0 ) ∈ E s.t u ∈ g, u0 =a

ループ」では，抽象化を行ったモデル (抽象モデル) に対してモ[r 7→ 0]u, u0 ∈ I(l0 )デル検査を適用し，検査の結果生じた反例が抽象化を行う前のu ∈ g は u ∈ RC がガード g を満たすことを示している．同様

モデル (具象モデル) 上で再現できるかどうかを調べ，具象モデに，u ∈ I(l) は u ∈ RC がロケーション l でのインバリアントル上で再現不可能な反例 (見せかけの反例) を検出した場合は，を満たすことを示している．また，[r 7→ 0]u は u において rそのような反例が発生しないように抽象モデルを改良する，とに含まれる全てのクロックを 0 にリセットすることを意味していう操作を繰り返すことで適切な抽象モデルを生成する手法でいる．

ある．本提案手法では，時間オートマトンの状態空間の表現手法である DBM (Difference Bound Matrix) [6] に関するアルゴリズムを利用して抽象モデル上で発生した反例の再現を実現している．抽象モデルの改良には，見せかけの反例が生じた原因である抽象状態を分割，遷移の除去を行うことによって見せかけの反例が発生しないように改良を行う．
関連研究としては，文献 [7] では SAT ソルバによるモデル検査をベースとした時間オートマトンの抽象化手法を提案している．この手法では，反例が再現可能かどうかの判定にも SAT ソルバを利用し，抽象モデルの改良では，見せかけの反例が発生しないように，モデルを表現している命題論理を改良している．
しかし，時間変数が残ったままであるので純粋な SAT ソルバを適用できないなどの問題点がある．
以降，2. では準備として時間オートマトンについて説明する．
次に 3. でモデル抽象化に関する定理を与える．4. で「反例に基づいた抽象化改良ループ」の具体的なアルゴリズムについて述
べ，5. では提案した抽象化手法を適用した例を挙げる．6. で考察を与え，最後に，7. でまとめる．

2. 時間オートマトン
時間オートマトンは有限状態のオートマトンに時間経過を表現するクロック変数を付加したオートマトンである．本節では，標準的な時間オートマトンの構成要素や意味，更に時間モデル検査器 UPPAAL で扱っている拡張時間オートマトンについて簡単に紹介する．

2. 1 標準的な時間オートマトン
標準的な時間オートマトンは以下のように与えられる [6]．

2. 2 時間オートマトンの状態空間の表現
UPPAAL などのツールでは，時間オートマトンの無限の状態空間の表現方法として，ゾーンと呼ばれる表現を用いている [5]．ゾーンはクロックに関する制約の集合であり，ゾーンが持つ制約を満たす全ての状態を表現する．時間オートマトンが持つ状態空間は有限個のゾーンから構成されるゾーングラフで表現することができる．また，ゾーンが持つ制約の集合は，DBM(Difference Bound Matrix) とよばれる行列として表現することができる．DBM では，時間制約が一般に 2 クロック変数の差分不等式の集合で表されることを利用し，時間オートマトンが持つ n 個のクロックに対して (n + 1) × (n + 1) の行列として全ての制約を表現する．DBM のクロック制約を満たす全ての解の空間を D とすると，時間オートマトンの状態集合としSて (l, D) = u∈D (l, u) として表現することとする．また，全Sての l ∈ L に対して Dlinv = u∈I(l) u と表現する．

2. 3 UPPAAL における時間オートマトンの拡張
UPPAAL では，標準的な時間オートマトンに対して拡張を行った拡張時間オートマトンを検証モデルとしている [6]．標準的な時間オートマトンに対して UPPAAL 拡張時間オートマトンが追加している主な特徴を以下に示す．

bounded integer variable インバリアントやガード制約，変数の代入文に含めることが可能な整数変数．とり得る値の範囲の指定が可能．

urgent synchronisation この同期が可能な状態では時間経過が不可能となる同期．

urgent location ロケーション上での時間経過が不可能であるロケーション．

定義 2.1 (時間オートマトン). 時間オートマトン T A は 6 項組

commited location ロケーション上での時間経過が不可能であ(L, l0 , C, A, E, I) である．ここで L はロケーションの集合であり，次の瞬間にこのロケーションから抜け出す必要のあるロり，l0 ∈ L は初期ロケーションである．C はクロックの集合，ケーション．

A はアクションの集合である．アクションは他のプロセスと同

これらの拡張点のうち，整数変数については抽象化による状期を取るアクションと 1 つのプロセス内だけの τ -アクションか態数の削減が可能であると考えられる．しかし，以降で述べるら構成される．E ⊂L × A × B(C) × 2C × L はロケーション間=の状態遷移の集合であり，アクション，ガード，リセットする

抽象化手法は標準的な時間オートマトンが持つクロック変数のクロックの集合を持つ．B(C) はクロックに関する条件式の論理積の集合である．I : L → B(C) は各ロケーションに対してインバリアントを割り当てる．
定義 2.2 (時間オートマトンの意味). 時間オートマトン TA は次のような遷移システム (S, s0 , →) として定義される．S ⊂L×RC=は状態の集合であり，s0 = (l0 , u0 ) は初期状態である．また，→ は次のような遷移関係を表現する．
d00• (l, u) −→ (l, u + d)if∀d0 : 0 <=d <= d ⇒ u+d ∈ I(l)抽象化であり，整数変数の抽象化は 6. の考察で述べている．

3. モデル抽象化
この節では時間オートマトン T A によって生成される状態遷移系 M = (S, s0 , →) の抽象モデル M̂ = (Ŝ, sˆ0 , →)
ˆ を与える．
なお，簡単化のため，ここでは標準的な時間オートマトンを対象とする．抽象化関数 h : S → Ŝ は S に含まれる具体的な状態から Ŝ に含まれる抽象状態 へのマッピングである．文献 [2]より M に対する抽象化関数 h は定義 3.1 のように与えられる．

—2—

定義 3.1 (抽象化関数 h). 状態遷移系 M = (S, s0 , →) を抽象化
関数 h によって抽象化されたモデル M̂ = (Ŝ, sˆ0 , →)
ˆ は以下のように与えられる．
（ 1 ） Ŝ = {ŝ|∃s.s ∈ S ∧ h(s) = ŝ}（ 2 ） sˆ0 = h(s0 )（3） →ˆ = {(sˆ1 , sˆ2 )|∃s1 ∈ S.∃s2 ∈ S.(s1 → s2 ) ∧ h(s1 ) =sˆ1 ∧ h(s2 ) = sˆ2 }また，h−1 : Ŝ → 2S を h の逆関数として与える．
本稿で提案する抽象化手法では，システムの異常な状態を表
図 1 抽象化改良ループ

すロケーション e ∈ L に対して，AG¬e を検査する．これは eへの遷移は存在しないということを表す検査式である．この検4. 1 初期抽象化

査式に対する反例は必ずループを含まない．
文献 [2] では，命題論理 p に対し検査式 AGp を検査するための状態縮約にともなう意味変化をなるべく起さないという意
味で保守的な抽象化についての定理が与えられている．与えら

初期抽象化は，具体的な状態遷移システム M = (S, s0 , →)に対して適用する最初の抽象化である．提案手法では，時間オートマトンのクロック変数を全て省略するという方法で初期抽象化を行う．したがって初期抽象化関数 h は以下のように定れた定理から以下の定理を導くことができる．

義できる．
定理 3.1. 時間オートマトン T A = (L, l0 , C, A, E, I) によって•∀l ∈ L, ∀u1 ∈ I(l), ∀u2 ∈ I(l).h((l, u1 )) = h((l, u2 )) = l

生成される状態遷移系 M = (S, s0 , →) に対し，抽象化関数•∀(l1 , u1 ) ∈ S, ∀(l2 , u2 ) ∈ S. h(l1 , u1 ) = h(l2 , u2 ) ⇐⇒h を用いて抽象化された抽象モデルを M̂ = (Ŝ, sˆ0 , →)ˆ ，シス

l1 = l2

テムの異常な状態を表すロケーションを e ∈ L，抽象モデル
ˆ = S(h(e, u)) とする ．
におけるエラー状態の集合を Erたす．また，提案手法の初期抽象化では，２つの異なるロケーˆ とした時，全ての s ∈ S に対して
h(s) |= ¬e ⇐⇒ h(s) ∈/ Erションに属する状態を１つの抽象状態にマッピングする抽象化u∈I(e)ˆ ⇒s∈h(s) ∈/ Er/[(e, u)(1)u∈I(e)このとき，初期抽象化関数 h による抽象モデルは式 (1) を満は行っていない．したがって，以下で述べる改良を施した抽象モデルにおいても，全ての抽象状態は１つのロケーション上の状態を縮約した状態である．なお，後述の改良ステップにより，

ならば，M̂ |= AG¬e ⇒ M |= AG¬e．

必要なら，抽象オートマトンの状態の細分化が時間領域の情報Proof. 文献 [2] の定理 1 より，命題論理 p に対して，抽象化関を用いて行なわれることとなる．

4. 2 モデル検査

数 h が全ての s ∈ S について

モデル検査では，抽象モデル M̂ に対してモデル検査を行う．

h(s) |= p ⇒ s |= p(2)を満たすならば，状態遷移系 M を h によって抽象化したモデ
ルを M̂ とすると，M̂ |= AGp ⇒ M |= AGp である．s |= ¬p
Sはs∈/ u∈I(e) (e, u) であり，式 1 と式 2 は同値である．従って
文献 [2] の定理 1 より，定理 3.1 を証明できる．
定理 3.1 より，抽象モデルに対して AG¬Wˆ ê を示すこê∈Erとができれば，具象モデルでも AG¬e を示すことができる．

定理 3.1 より，抽象モデルを生成する抽象化関数 h が式 1 を満たすならば，抽象モデル M̂ 上で性質を満たせば具象モデル M上でも性質を満たすことは保障される．しかし，M̂ 上で反例が発生した場合は，反例が具象モデル M で再現できるものかどうかを確かめる必要がある．

4. 3 シミュレーション
抽象モデル上で発生した反例が具象モデル上で再現できるかどうかの検査を行う．抽象モデル上で発生した反例を4. 反例に基づいた抽象化改良ループ

T̂ = hsˆ0 , . . . , sˆk i とする．このとき，反例 T̂ はロケーション
V
遷移 T = hl0 , . . . , lk i( ki=0 ∃u ∈ RC .(li .u) ∈ h−1 (si )) に対応

モデル抽象化では，過剰な抽象化や誤った抽象化によって本する．

来のモデルでは発生するはずのない見せかけの反例が発生して提案手法では，具象モデル上でロケーション遷移 T を再現しまう場合がある．文献 [1] では，最初に十分な抽象化を行い，し，ロケーション lk へ到達可能性を調べることで反例が再現可抽象モデル上で見せかけの反例が発生すればその反例が発生し能かどうかを調べている．ロケーション lk へ到達可能性についないように抽象化されたモデルを改良する，反例に基づいた抽ては，ロケーション遷移 T = hl1 , . . . , lk i に対して，具象モデ象化改良ループを提案している．抽象化改良ループを図 1 にル上において初期状態から到達可能なゾーンを求めることで実示す．本節では，時間オートマトン T A が生成する状態遷移系現する．各ロケーション li 上で到達可能なゾーンを Direach とM = (S, s0 , →) に対する具体的な抽象化改良ループを与える．

すると，Direach = ∅ となる i <= k が存在すれば，反例 T̂ は再現不可能であると判断できる．逆に Dkreach 6= ∅ であれば反例—3—

図 3 状態の複製
図 2 反例パスの再現

T̂ は再現可能であり，ループは終了する．
文献 [5] ではゾーンを表現する DBM に対するアルゴリズムが紹介されており，これらのアルゴリズムを用いることで Direachを求めることが可能である．なお，T に現れる制約 (各ロケーションのインバリアント，各遷移におけるガード) の個数を mとすると，反例の再現は O(mn2 ) の時間計算量で実現できる．

4. 4 抽象化改良
抽象モデル上で発生した見せかけの反例 T̂ = hsˆ0 , . . . , sˆk i が

図 4 改良した抽象モデル発生しないように，抽象モデルの改良を行う．本手法では，文献 [1], [3] で提案されている，抽象状態の分割，遷移の除去による改良手法を応用する．
見せかけの反例が生じる原因は，反例を具象モデル上で再現した際に，反例の初期状態から到達可能な状態集合 (Reach) と次状態へ遷移可能な状態集合 (Succ) の積集合が ∅ となるような抽象状態が存在するからである．このとき，Reach に含まれる状態からは反例上の次状態への遷移は存在しないため具象モデル上では反例を再現できないが，Succ に含まれる状態からは次状態へ遷移可能であり，抽象モデル上では次状態への遷移が生じてしまうのである．図 2 では抽象モデル上の反例

hŝ0 , ŝ1 , ŝ2 , ŝ3 i を具象モデル上で再現した例を示している．図の各抽象状態 ŝi の下の図は状態集合 h−1 (ŝi ) を表している．図では抽象状態 ĉ において，Reach ∩ Succ = ∅ となっており，反例は再現不可能であることがわかる．
文献 [1], [3] では，見せかけの反例を除去するために，抽象状態を分割し，Reach と Succ を別の抽象状態にマッピングする改良を行っている．
時間オートマトンにおいて，抽象状態を Reach と Succ に分割するには，クロックによる状態空間を分割する必要がある．
しかし，状態空間の分割を行った場合，虫食い状の空間を形成してしまうなど，分割後の状態空間の処理が複雑化してしまうという問題が発生する．そこで本稿では，初期状態から到達可能な状態空間を複製することによって，反例の除去を行う手法を提案している．ここからは，到達可能な状態空間の複製による反例の除去を行う手法について，1) 状態の複製，2) 遷移の除去の２つの工程に分けて説明する．

1) 状態の複製整数 f を反例 T̂ において Dfreach = ∅ となるような最小の整数とする (図 2 では f = 3)．このとき，抽象状態 ŝf −1 は初態である．状態の複製では，ŝf −1 に対して，初期状態から到達可能な状態集合 Reach を縮約する抽象状態として sˆ0 f −1 を生成する (図 3 参照)．時間オートマトンでは，到達可能な状態集合 Reach はデータ構造 DBM を利用することによって求めることができる．なお，ŝf −1 ，sˆ0 f −1 への遷移については，

h−1 (ŝf −1 ) \ h−1 (sˆ0 f −1 ) への遷移が可能な状態のみ ŝf −1 への遷移が可能であるとし，このとき sˆ0 f −1 への遷移は不可能であるとする．

2) 遷移の除去
まず，sˆ0 f −1 から ŝf への遷移は不可能であるため，遷移(sˆ0 f −1 , ŝf −1 ) は除去することができる．さらに，ŝf −2 からŝf −1 への遷移が不可能であれば，遷移 (ŝf −2 , ŝf −1 ) を除去することができ，このとき，反例 T̂ を除去することができる．しかし，遷移を除去できない場合は反例 T̂ を除去することができな
い．この場合は，さらに反例 T̂ の１つ前の状態 ŝf −2 に対して状態の複製，遷移の除去を行う，という操作を繰り返すことによって反例を除去することができる．これは，最終的に ŝ1 の複製を行った場合，ŝ0 から ŝ1 への遷移は不可能であり，(ŝ0 , ŝ1 )は除去可能であるため，反例を除去することができるのである．
図 3 では，遷移 (sˆ0 2 , ŝ2 ) は除去可能であるが，遷移 (ŝ1 , ŝ2 ) は除去不可能である．したがって図 3 のモデルの抽象状態 ŝ1 に対して状態の複製を行う必要がある．ŝ1 に対して状態の複製を行ったモデルを図 4 に示す．図 4 のモデルでは，遷移 (sˆ0 1 , ŝ2 )，(ŝ0 , ŝ1 ) を除去可能であり，反例を除去することができる．
本改良手法は，クロック空間の複製，遷移の除去からなるが，時間オートマトンは有限の個数のゾーンから表現でき，遷移の個数も有限であり，本改良手法を用いた抽象化改良ループは必ず終了する．
最後に，提案手法による抽象モデルの改良手法の正しさにつ期状態から到達可能であり，かつ次状態へは遷移不可能な状

—4—

図5

照明システムいて，各工程ごとに以下で簡単に説明する．

c1) 状態の複製i 回目のループにおける抽象モデルを M̂i とし，M̂i において，M̂i 上の状態 ŝj の複製である sˆ0 j を追加した抽象モデルを
図 6 照明システムの積オートマトン

M̂i+1 とする．このとき，M̂i における全ての遷移は M̂i+1 上に存在する．したがって，M̂i+1 における全ての遷移が M̂i 上の遷移へ置き換え可能であることを示すことで，２つの抽象モデルが同値であることを説明する．
まず，M̂i+1 における遷移 (â, b̂) について，â 6= sˆ0 j かつ b̂ 6= sˆ0 jであるとき，遷移 (â, b̂) は M̂i でも存在する．â = sˆ0 j である
場合は，遷移 (sˆ0 j , b̂) は M̂i 上の遷移 (ŝj , b̂) へ置き換え可能である．同様に b̂ = sˆ0 j である場合，遷移 (â, sˆ0 j ) は M̂i 上の遷移(â, ŝj ) へ置き換え可能である．したがって，M̂i+1 上の全ての遷移は M̂i 上の遷移へ置き換え可能である．

c2) 遷移の除去
文献 [1], [3] では，抽象モデル上における遷移 (ŝ1 , ŝ2 ) ∈ →ˆに対して，h−1 (sˆ1 ) のどの状態からも h−1 (sˆ2 ) に含まれる状態に遷移不可能な場合に，遷移 (sˆ1 , sˆ1 ) の除去は抽象モデルの改良であるという補題が与えられている．
図 7 初期抽象モデル

提案手法では上記の補題の条件を満たさない遷移の除去が生じる．以下では，補題の条件を満たさない遷移の除去につ照明システムの二つのオートマトンを結合した積オートマトいて抽象化の改良であることを説明する．まず，反例 T̂ 中の状態 ŝj の複製 sˆ0 j について，Dj = h−1 (ŝj ) \ h−1 (sˆ0 j ) とし，ンを図 6 に示す．この積オートマトンに対して抽象化を適用すh−1 (ŝj−1 ) の次状態の集合を Succj−1 とする．このとき提案手法る．したがって検査する性質は−1

では，Dj ∩ Succj−1 = ∅ である，つまり h (ŝj−1 ) から遷移可能な状態は h−1 (sˆ0 j ) に含まれる状態のみである場合は，ŝj−1 かAG¬((dim, idle) ∨ (bright, idle))

ら ŝj への遷移は不可能であるとし，遷移を除去している．ことする．式 3 の性質を図 6 のモデルに対して UPPAAL で検査の場合，h−1 (ŝj−1 ) からは到達不可能である Dj への遷移は除去されているが，h−1 (ŝj−1 ) から到達可能な状態集合 Succj−1 への遷移は残されているおり，このような遷移の除去は抽象モデル(3)を行うと，valid と出力される．したがって図 6 のモデルは式 3の性質を満たしている．
ここからは，図 6 に示す積オートマトンに対して，本稿で提の改良であるといえる．

案している抽象化を適用する．まず，積オートマトンに対して5. 抽象化改良例

初期抽象化を適用したモデルを図 7 に示す．初期抽象化では，積オートマトンが持つクロック変数 x，y を省略する抽象化を

本節では，具体的な時間オートマトンのモデルに対して本稿行っている．

で提案している抽象化手法適用した例を示す．適用したモデル

抽 象 モ デ ル に 対 し て ，UPPAAL を 用 い て 式 3 の 制 約 式

は時間に依存した照明システム [5] である．照明システムのモを 検 査 し た 結 果 ，抽 象 モ デ ル に 対 し て 2 回 の 改 良 が 行 わ

デルを図 5 に示す．照明システムは照明のスイッチモデル (図れ た ．1 回 目 の 改 良 を 図 8 に 示 す．1 回 目 の 改 良 は 反 例左) とユーザモデル (図右) から構成される．照明システムのエT̂1 = h(of f, idle), (dim, relax), (bright, idle)i に対して行わラー状態はユーザモデルが idle 状態である時にスイッチモデルれた．図 6 の具象モデル上で反例 T̂1 を再現した時，初期が dim または bright である状態とする．

状態 (of f, idle) から (dim, relax) に遷移した時に到達可能—5—

6. 考察

本稿では，標準的な時間オートマトンが持つクロック変数の抽象化について具体的な手法を提案している．しかし，提案手法では，UPPAAL 拡張時間オートマトンが持つ整数変数に対する抽象化には対応していない．ここでは，整数変数の抽象化についての考察を与える．整数変数は非連続値であり，有限な
図8 改良

1ドメインであるため，プログラム中の述語に着目した述語抽象化 [8] が適用できると考えられる．述語抽象化では，プログラム中の全ての状態を，プログラム中に現れる述語に対する真偽についての同値類に分類し，抽象化を行う．UPPAAL では整数変数に関する述語はロケーションのインバリアントや遷移におけるガードに現れるため，インバリアントやガードに含まれる述語に着目した同値類を形成することで，整数変数に対する抽象化を与えることができると考えられる．

7. お わ り に
図9 改良

2

本論文では，「反例に基づいた抽象化改良ループ」を利用し，時間モデル検査ツール UPPAAL で用いられる拡張時間オートマトンに対する具体的なモデル抽象化手法を提案した．モデル抽象化には，反例に基づいた抽象化改良ループ CEGAR を適用し，抽象化から検査までの全ての工程を自動的に行うことが可能である．また，反例によるモデルの再抽象化においては時間オートマトンの検証で用いられるデータ構造 DBM を活用する工夫を行なっている．
今後の課題としては，提案手法を実用的な例題に対して適用し，本手法の有効性を評価することが挙げられる．また，本稿では UPPAAL 拡張時間オートマトンが持つ整数変数の抽象化には対応しておらず，整数変数の抽象化も課題として挙げられる．その際，6. で述べた手法の適用を考えたい．
文

図 10

最終的な抽象モデル

な ク ロック 空 間 は x = y で あ る ．し か し x = y で あ る
クロック空間は，遷移 ((dim, relax), (bright, idle)) のガード

x <= 10 ∧ y > 10 を満たさないため，反例 T̂1 は再現不可能である．この反例を除去するため，図 8 の図下のように改良を行う．図の状態 (dim, relax1) は具象モデル上の状態(dim, relax) のインバリアントを満たす状態を表現し，状態(dim, relax2) は x = y を満たすクロック空間のみを表現する抽
象状態である．2 回目の改良は図 9 に示す．2 回目の改良は反例T̂2 = h(of f, idle), (dim, t), (of f, study), (dim, idle)i を除去するために行われた．
これらの改良をした結果として最終的に得られる抽象モデルを図 10 に示す．最終的な抽象モデルに対して UPPAAL で検査を行ったところ，valid という結果を得ることができた．したがって，この例ではクロック変数を全て省略した抽象モデルを用いて具象モデルと同様の結果が得られることがわかる．

献[1] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and V. Helmut: “Counterexample-guided Abstraction Refinement, Computer
Aided Verification:12th International Conference,vol1855,pp154169,July,2000.
[2] E. Clarke, A, Gupta, J. Kukula, and O. Strichman: “SAT
based Abstraction-Refinement using ILP and Machine Learning Techniques, Computer Aided Verification:14th InternationalConference,vol2404,pp695-709,July,2002.
[3] E. Clarke, A. Fehnker, Z. Han, J Ouaknine, O. Stursberg, amd M.
Theobald: “Abstraction and Counterexample-guided Refinement inModel Checking of Hybrid Systems, International Journal of Foundations of Computer Science,Vol.4,No.4,2003.
[4] R. Alur: “TimedAutomata, Computer Aided Verification:11th International Conference,vol1633,pp688,July,1999.
[5] J. Bengtsson, and W.Yi: “Timed Automata: Semantics, Algorithms
and Tools, Lectures on Concurrency and Petri Nets,vol3098,pp87124,2004.
[6] G. Behrmann, A. David, and K.G. Larsen : “A Tutorial on
Uppaal, Formal Methods for the Design of Real-Time Systems,vol3185,pp200,236,2004.
[7] S. Kemper, and A. Platzer: “SAT-based Abstraction Refinement forReal-time Systems, In Third International Workshop on Formal Aspects of Component Software, 2006.
[8] S. Das, D. L. Dill, and S.Park : “Experience with predicate abstraction, In Computer-Aided Verification, volume1633,pp160-171, 1999.

—6—