マルチメディア通信と分散処理ワークショップ 平成6年10月
分散システムの仕様記述と検証に関する研究
山 根 智 島根大学理学部情報科学科 分散システムは分散プロセスが非同期的に並列動作して，動作が正しいタイミン グで行われることが重要である.本稿では，停止性が仮定できないタイミング制約 記述を含む分散システムの仕様記述と検証を実現するために，次の手法を提案する. (1)仕様記述はプロセス代数や時間オートマトンにより階層的に構成して，システム 仕様を自動生成する. (2)システム仕様と検証仕様の統一的記述をベースとして，形式言語理論により形式 的な検証をする.1
.まえがき
交換機や自動車などの分散システムは多くの分散プロセスが同期的または非同期 的に通信しあいながら並列動作する.さらに，システムの論理動作の正当性だけで なく，動作が正しいタイミングで行われるかどうかが非常に重要である(1). (2) 多くの場合，分散システムの仕様は状態や動作，時間などの概念からなる有効グラ フで表現できる.仕様記述と検証のポイントは，効率的な有効グラフの作成手法や 表現力の高い検証性質記述言語，効率的な検証アルゴリズムである. 従来より，分散システムの仕様記述手法としては，プロセス代数やペトリネット， オートマトンなどが研究されており (2) 以下の特徴を有する. (1)ペトリネットは並行プロセスの記述能力や解析能力は高い.しかし， トランジショ ンやプレースの中のトークンの動作としてモデル化しなければならず，抽象度や直 感性が低く，決して使いやすい手法ではない. (2)オートマトンは状態と動作を統一的に扱いながら仕様記述できる.並行プロセス や複雑な状態が扱いにくいことや抽象度が低いといった問題があるが，従来より最 も多く使われている手法である. (3)プロセス代数はシステム動作をプロセス聞の通信動作として表現して，プロセス 聞のインターフェースが簡潔に記述できる.しかし，動作の順序関係に着目したモ デル化であるために，状態の概念が扱いにくく，並行プロセスの合成作業も容易で ない.また， Nicollinら{3}により実数時間領域を対象とする時間プロセス代数が提 案されており，時間オートマトンにコンパイルしてモデルチェッキングする手法が 提案されている. 本稿では， NicolIinらのアプローチと異なり，分散システムの仕様記述は分散プロS
t
u
d
y
on s
p
e
c
i
f
i
c
a
t
i
o
n
and v
e
r
i
f
i
c
a
t
i
o
n
method of d
i
s
t
r
i
b
u
t
e
d
s
y
s
t
e
m
S
a
t
o
s
h
i
Y
AMANE
セスの構成仕様とプロセス仕様の階層的なものと捉える.構成仕様は動作に着目し てプロセス代数により記述し，プロセス仕様は状態と動作に着目して時間オートマ トンにより記述する. 一方，検証手法は仕様記述手法と密接に関係しており，検証性質記述言語や検証 アルゴリズムの観点から以下が研究されている. (1)時相論理は状態、の時間的な制約関係から安全性や活性といった重要な性質が表現 できる (4) しかし，時相論理は動作の概念が表現できない.検証アルゴリズムは 論理式のKripke構造における充足性判定であり，モデルチェッキング (5)やシンボ リックモデルチェッキング (6)がある.
(
2
)
プロセス代数は等価性による仕様と実装の検証であり，時間プロセス代数におけ る完全かつ健全な公理系(7).(8)が提案されている. しかし，機械化が容易でない. (3)システム仕様と検証仕様がオートマトンにより記述されると，形式言語理論の言 語包合問題により検証できる.また，時間オートマトンによる言Z
飽，合アルゴリズ ムが提案されている (9) 本稿では，システム仕様と検証仕様との統一的な記述と機械化を狙って，検証仕様 をオートマトンにより記述して，形式言語理論の言語包合問題により検証するJ
以上より，本稿では，停止性が仮定できないタイミング制約記述を含む分散シス テムの仕様記述と検証を実現するために，以下の手法を提案する. (1)仕様記述は分散プロセスの構成仕様とプ白セス仕様の階層的なものと捉える.構 成仕様は動作に着目してプロセス代数により記述する.プロセス仕様は状態と動作 に着目して時間オートマトンにより記述する.システム仕様は構成仕様とプロセス 仕様から自動生成する. (2)活性や安全性などの検証性質は時間オートマトンにより形式的に記述する.検証 アルゴリズムは形式言語理論の言語包合アルゴリズムにより行う. 以下の本稿は 2章では分散システムの階層的な仕様記述手法を述べ， 3章では 検証手法を提案する. 4章では事例を示して 5章では関連研究を述べて， 6章で はまとめを述べる.2
.分散システムの仕様記述手法
本章では，分散システムの階層的な仕様記述手法を述べる.2
.
1
分散システムの構成仕様 上位階層は分散システムの構成情報を記述する.構成情報はプロセス代数により 構成仕様として記述する;プロセス代数は分散システムの動作をプロセス聞の通信 動作として表現する.プロセス聞のインターフェース聞の動作を簡潔に表現できる. [定義1
]
(構成仕様の定義) 構成仕様Pは以下のように帰納的に定義する. P:=Pl+P2IP1IIP2+.
1
1
:
P
1とP
2
の並列走行(AND
結合)口 [例1] (構成仕様の例) 構成仕様の図形表記の例を図 lに示す. (a)プリミテイプなプロセスは楕円形のプロセスと有効直線のイベントで記述する. (b)プロセスの構成仕様では，OR
結合は角のない正方形で縦に並べて記述して， AND
結合は長方形で横に並べて記述する. (c)分散システムの階層表現が有益である.下位階層が存在する場合は太い線により により記述する.図lではPl+P2に下位階層があり さらにP2がP3 11P 4 により構成されることを示す.口ー→Q2)←
- b→<E>←
- c・ (a)i'rimilivcpr民 間:斗dbrb仁
:
(b】Configur.llionspecilic:llion 図1 tI成仕織の例 fig.l Example ofαmfiguration勾陪cificalion 2. 2 分散プロセスのプロセス仕様 (c)HieuachicaJconfigurlllIon spccilicalion 下位階層は時間オートマトンによりプロセス仕様として記述する.時間オートマ トンはω・オートマトンをクロック変数によるタイミング制約式により拡張したもの であり (9) 停止性が仮定できない分散プロセスの記述を可能とする.時間オート マトンの受理言語は時間付き正規言語であり，以下のように定義できる. [定義2] (プロセス仕様) プロセス仕様はP=
(~， S， S 0， C， E， F)の6つ組で定義される. 、，、'・4哩L ~~ ¥".， ヱ:有限イベント集合S
:有限状態集合 SocS :初期状態集合C:
クロックの有限集合 EÇSXSX~X2CXφ( C) 時間付遷移関数FCS:
受理状態集合 なお， φ(C) はクロック Cのタイミング制約式8であり，クロック集合Cと整数 の時刻定数dにより再帰的に定義される: 8:=XくdldくXI
-， 8I
8 1^
8 2I
X:= 0 . また，所与のイベントにより，無限回遷移する状態と受理状態、集合Fとの共通集合 が空集合でないならば，そのイベントは受理される.口[例2] (プロセス仕様の例) プロセス仕様の例を図
2
に示す.S
0
→S 1
の遷移はイベント aにより生起してク ロック変数yがリセットされる.また， S 1→ S 2の遷移はイベント bの生起かっ クロック変数y=lの条件を満たすとき起きる.受理状態はS1であり， S 1を無 限回繰り返す状態遷移列が受理される.口 2. 3 分散システムのシステム仕様 構成仕様とプロセス仕様からシステム仕様を自動合成する.自動合成の規則とし ては，選択的走行はプロセス仕様のOR
結合であり並列走行はプロセス仕様のA N D結合に対応する.また，プロセス代数のリラベリング操作とレストリクション操 作()0)を定義する. [定義3]
(システム仕様の自動合成) プロセス仕様はP
1 = (~ぃ S l' S 10， Cぃ El' F1) とP
2=(
ヱ
2' S 2' S 20， C 2' E 2 t F 2 )により与える.自動生成の規則はOR
結合とA N D結合，リ ラベリング操作，レストリクション操作である. (1)
0
R
結合 P 1+
p
2 = (~1 U ~ 2' S 1 U S 2' S 10U S 20， C 1 U C 2' ここで EIÇSlXSlX~lX2ClXφ(C 1) E2C;52X52XI2X2C2Xφ(C 2) (2)AND結合 E1U E21 F1U F2) P 1 11p 2 = (I 1 U I 2 ' S 1 X S 2' S 10 X S 20， C 1 U C 2 ， E.' F 1 X F 2)ここで， EE(S lxS 2)
×
(21UZz)X2c luC2Xφ(C1n C2) (3)リラベリング操作 イベントの名前を変更する操作であり，異なるプロセスを結合するための操作で ある.リラベリング関数μ:Il → ~2 であり， μ(p 1) . ( I 2 ， 5 l' 5 10， C l' E ， F 1) である.ここで， ECS}XS}XI2X2C1Xφ(C 1) (4)レストリクション操作 イベントを隠蔽することにより，プロセスの動作を抽象化する.a
c
~ 1とすると， P 1¥a = (~l - a， S l' S 10， C l' E， F 1 )である.ここで， ECSlXS}X (ヱ l-a) X 2C1Xφ(C 1)
口
3
.分散システムの検証手法
本稿では，検証手法としてはシステム仕様と検証性質仕様が統一的に扱える言語 包合問題を考える.ここでは，分散システムに対する検証性質記述言語と検証アル
3
.
1
検証問題の言語包合問題への帰着 分散システムのシステム仕様と検証性質仕様をオートマトンで記述すれば，検証 問題は言語包合問題に帰着できる (9) [定義4] (言語包合問題) 言語包合問題は L (M¥) 三 L (M2) と定義できて，以下と等価である: L (M))ハτ
一てlVI"TJ
=
併 ここで， M1
:
システム仕様を表現する時間オートマトン L (M1) : M1の受理言語 M2 :検証性質仕様を表現する時間オートマトン L (M2) : M2の受理言語 検証コストより L (M2) は補集合演算閉包性と決定性が条件である (9) 口3
.
2
検証性質記述言語 分散システムにおける検証性質は「何も悪いことは起きない」といった安全性や 「何か良いことが起こるだろうJ
といった活性に分類できる.検証性質記述言語は， 決定性手続きの存在性の要件より，決定性時間Mullerオートマトンが適用できる. このオートマトンは状態のベキ集合を受理状態集合する (9) [定義5] (決定性時間Mullerオートマトンの構文) 決定性時間Mullerオートマトンは(~，S
，S
O
，C
，E
， F) の 6つ組で定義され る.ここで，FC2
S
:
受理状態集合であり，他の項は[定義2J
と同じである.I
501=
1であり状態遷移は決定的である.口 この言語包合問題による検証手法は決定性手続きが存在する (9)3
.
3
検証アルゴリズム 検証アルゴリズムはシステム仕様と検証性質仕様の補集合との積オートマトンに 対する閉ループ発見である.積オートマトンはタイミング制約が存在するので，通 常の有効グラフの探索アルゴリズムにタイミング条件の判定アルゴリズムを追加す る必要となる.本検証手法は次の手II}貢より構成できる. (1)まず，検証性質記述の補集合とシステム仕様との積オートマトンを生成する. (2)積オートマトンの閉ループ発見は，時間オートマトンのタイミングシミュレーショ ン(9)であり，以下の手順で行う. (a)Targanの深さ優先探索(13)により閉ループを発見する. (b)ノード探索毎にタイミング制約やクロック値，因果 関係との相互関係の無矛盾 性をチェックする.もし 相互関係に矛盾があれば，該当ノードの枝刈りを行う. 矛盾がなければ探索を続ける. (1)の積生成のアルゴリズムは容易なので省略する. (2)に関しては，積時間オートマトンを直接的にタイミング条件を考慮しながらシミユレーションする. (a)タイミングシミュレーションは，初期状態ですべてのクロック変数にゼロを割り 当ててからシミュレーションを開始する. (b)すべてのクロック変数は同じ割合でカウントアップされて，リセット式によりゼ ロに設定する. リセット式により，クロック変数の聞の因果関係(クロック値の大 小関係を表わす全順序関係)が変化する.イベントが生起して，クロック値や因果 関係，タイミング制約が矛盾しなければ遷移が発生する. (c)因果関係が変化する場合，リセット式が存在しなければタイミング制約が矛盾と 判定する.そうでなければ無矛盾と判定する. [例
4]
(タイミングシミュレーションの例) 図2のプロセス仕様に対応するタイミングシミュレーションを図 3に示す.図 3の 右側(2)はリセット式が存在しないのに因果関係が変化しているので，タイミング条 件に矛盾が存在する.ゆえに，左側(1)の遷移のみが可能である.また，図4はクロッ ク値や因果関係，タイミング制約との相互関係を示す.時間を進行させながら，タ イミング制約から因果関係を導出して，クロック値を求める.クロック値は時間領 域上の等式又は不等式である.図4(b)のように，因果関係に矛盾が起きればタイミ ングに矛盾があると判定する口
l.
t
x>y X>O. y圃o x>y
• x> 1 ?
>0. Y>O x>y ∞x>y ntradicllon • x> 1 ? x<y y:
。
園
①
x>o・Y"'O x >.， (a15 0 -5 1-53 -5.1ー… (b1 50-51-52-53-51--図3 タイミングシミュレーシ田ン clock valucs 腕8.3Timin& slm且1&11on a， '1<1?， '1:目。 図2 プロセス仕様の例 Fig.l Eumple or proc白sspecific:llion each symbolmI::IIISrollowin8 : 4・H・H・.deriY81ion orc:ausdily rclalion 圃 園 田 園cloclc叫ue ← -relwcn belween cl∞k叫ue制 limins∞ns回inl~stalc lIllnsltlon 図4 タイミングシミュレーションにおけるタイミングの相互関係 腕8.4Timing Intcrrelations in timing slmuladcnこのように，タイミングシミュレーションでは時間を経過させながら，クロック値 や因果関係，タイミング制約・の問に成立する不等式を解いて矛盾を発見するもので ある.また，状態列の探索は
T
a
r
g
a
n
の深さ優先探索アルゴリズムで行う.4
.事例
本稿では，提案する手法の有効性を自動車制御システムの事例により示す.自動 車制御システムはドライパや路面などの環境と相互作用する.自動車制御システム はエンジン系とその他の系から構成されて エンジン系はアクセルやエンジンなど から構成される.また，プレーキはノーマルプレーキとABSプレーキの選択的結合 である.以上の階層関係を図5(a)に示す.本稿では，アクセルとエンジンの並列的 走行を例に取り上げる. アクセJレとエンジンのプリミテイプなプロセスや構成仕様は(b)と(c)に示す.また， アクセルとエンジンのプロセス仕様は図6
に示す.プロセス仕様と構成仕様から自 動生成したシステム仕様を図7
に示す.また，検証すべき性質としては，イベントa
c
c
e
l
o
n
が生起してからイベントs
o
p
e
n
が生起するといった不変性を示す安全性やイベ ントa
c
c
e
l
o
f
f
が生起してから9
時刻未満にイベントs
k
e
e
p
が生起するといった時間応 答性を示す活性などである.図8に検証性質仕様の記述例を示す.次に，検証用の 積オートマトンはシステム仕様と検証性質仕様の補集合のオートマトンから生成す る.オートマトンの補集合は受理状態集合F
の補集合であり2s
"
'
:
'
F
である.積オー トマトンは図9のように生成できる.SUN-IPC上にインプリメントした検証プログ ラムにより積オートマトンを入力したら，受理ループなしを出力した.つまり，検 証性質は満たされることがわかった. 本稿では自動車制御システムの一部のみを検証対象としたが，システム全体を対 象とすると状態空間が大きく成り過ぎて検証コストが大きくなる.これを解決する 一手法として，C
l
釘k
e
らのインターフェースルールによる検証の局所化を既に提案 している (9) これはリストリクション操作により検証性質仕様に無関係なイベン トを隠蔽するものである.また，リラベリング操作により，インターフェースの異 なる他車種の部品を組み合わせて，仕様の構成も可能である. 本手法の仕様記述と検証の手法を支援するシステムはプロセス仕様と構成仕様か ら シ ス テ ム 仕 様 を 合 成 す るs
p
e
c
i
f
i
c
a
t
i
o
na
u
t
o
m
a
t
i
c
g
e
n
e
r
a
t
o
r
や検証機能を果たすl
a
n
g
u
a
g
e
i
n
c
l
u
s
i
o
n
verifierÌ)~ら構成した. 以上の事例により，自動車制御システムの階層的な仕様記述と検証の手法の有効 性が確認できた.5
.関連研究
停止性が仮定できないタイミング制約記述を含む非同期型システムの仕様記述と 検証に関する研究事例としては，時間プロセス代数法 (3)やt
i
m
e
d
μ・c
a
l
c
u
l
u
s
j法(I 4) 時間付きステートチャート法{引などがある.時間プロセス代数法は，時間プ....~Iomob~... engine syscemI :molhcr syslcm
/
l
t
6
inCSYS~.JL偲~YS，信豆
EbKEPi-
〈
E
D
-
-
-
:
(a)Auωmobileco明lrol$y$lem護
法
p三蚕豆診器三玄⑤←
Ignon (b)針 刷tiveproc君" 1Cc:c1∞ ac句Ikeep accelofT acceler.&ωr I enginc 主二Z
S
E
E
6~t~n C!亙!:)l工=15dtff (c)白nfigurationspeciliclllion 図5 自動車制御システム{ー部) Fig.5 AUlomobile conlrol sySlem(apart) -acxclon (a)safely (b)li刊nωs 図8t食lit主貸住鎌 Fig.8 Vcrific;1lion propcrty spccific3lion al (a)accelerBlor (b)enginc 図6 プロセス仕犠 Fig.6針OC:CSS5戸cific:uion 図7 システム仕線 Fig.7 System specilic:llion ロセス代数により記述した仕様を時間オートマトンにコンパイルして，モデルチッ キングにより検証するものである.しかし，仕様記述言語と検証記述言語の違いや 仕様記述レベルと検証レベルの違いがあり，エラー箇所の発見や使い易さなどに問 題がある.timed μ-ca1culus法はガーデイツドコマンドプログラミング言語により記 述した仕様をtimedμ・calculusによりモデルチッキングするものである.本手法は仕 様記述の記述レベルが低く，大規模システムが記述できる構成的な手法でない.ま た，仕様記述と検証記述の体系が統一的でない.時間付きステートチャート法はス テートチャートを時間オートマトンにより拡張したものであり，仕様記述と検証記 述の体系が統一的である.しかし，仕様記述の抽象度が低く ステートチャートの 制限により，あまり大きなシステムが記述できない.図9績オートマトン Fig.9 Produαo( lIulOmDIOn
また，タイミング制約記述を含む非同期型システムの仕様記述は時間グラフ(時 間オートマトン)で表現できる場合が多く，時間グラフの探索手法が重要である. 従来の研究では，時間グラフからリージョングラフを生成して，時間なしの有効グ ラフの探索問題に定式化している(l5) しかし，リ}ジョングラフ法はノード数が タイミング制約の長さのペキ乗オーダで効いており，メモリ量と閉ループの発見の 時間コストが大きなボトルネックとなっている.我々はこの問題を解消するために， リージョングラフの代わりに通常の積オートマトンをタイミングシミュレーション して検証する手法を既に評価しており，検証コストの削減を確認した (9)
6
.むすび
本稿では，停止性が仮定できないタイミング制約記述を含む分散システムの仕様 記述と検証を実現するために，分散プロセスの構成仕様(プロセス代数)とプロセ ス仕様(時間オートマトン)の階層的体系と言語包合アルゴリズムを提案した.本 手法を自動車制御システムの事例に適用して有効性を示した. 本手法を実際に適用する場合，高度なGUIにより仕様の編集作業支援や仕様の誤 りの発見のツールのガイドラインが必要である.今後の課題としては以下が考えられる. (1)本検証をシンボリックモデルチェッキングにより実現する (2)時間汎用時相論理などのより抽象度の高い仕様から時間グラフを自動生成する
参考文献
(1) Tilborg A.M.:"Foundations of reaItime computing Fomal Specifications and Me出ods"， p.316，Kluwer academic publishers(1991) (2) Kavi K.M.:"ReaI-time Systems， Abstraction， Languages and Design Methodologies'¥ p.660， IEEEComputer Society (1992) (3) Nicollin X. Sifakis J. Yovine S."Compi1ing Real-Time Specifications into Extented Automata"， IEEE Trans. Software Eng. Vol.18，No.9， pp.794-804(1992)(4) Leeuwen 1. V.:"FormaIModels and Semantics"， Handbook of Theoretical Computer Science Vol.B， pp.995-1072(1990)
(5) Clarke E.M. Emerson E.A. Sistla A.P.:"Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications"，ACM Trans. on
Programming Languages and Systems，Vo.8，INo.2，pp.244-263(1986)
(6) Burch J. R. Clarke E. M.， McMillan K.L.， Dil1 D.L.， Hwang L. J.:"Symbolic Model Checking: 1020States and Beyond"， Proc. 5th IEEE Logic in Computer Science， pp.428・439(1990) (7) NicollinX. Sifakis J.:"An Overview and Synthesis onTimed Process Algebras
ぺ
Lecture Notes in Computer Science 600，pp.526・548(1992) (8)佐藤一郎，所真理雄."時間的特性を考蔵した並列プロセスの形式的記述" 情報処理学会論文誌， Vo1.34，No.4，pp.540・548(1993) (9) 山根智，梅原伸年."無限列時間付きステートチャートによる並行システムの 仕 様 記 述 と 検 証 の 手 法 信 学 技 報J CAS94-55，pp.37・44(1994) (1O)Milner R.: "Communication and Concurrency" ，Prentice Hall，p.260(1989) (11)Hoare C.A.R:"Communication Sequential Processes"， Prentice Hall，p.256(l985)(12)Hopcroft J. E. Ullman J. D.:"Introduction to Automata Theory ， Languages and Computation"， Addison-Wesley (1979) (13)Tarjan R."Depth-first search and linear graph algorithms"，SIAM Journal of Computing1(2)，pp.146・160(1972) (14)Henzinger T.A. Nicollin X. 'Sifakis J. YovineS. : "Symbolic model-checking for real -time systems"，Proc. 8th IEEE Logic in Computer Science，pp.394-406(1992) (15)Alur R. Courcoubetis C. DilID.:"Model-Checking for Real-Time Systems
