SDVerifier:
プロセス代数
CSP
を用いた
シーケンス図検証ツール
海津 智宏 磯部 祥尚 鈴木 正人
コンポーネントを利用したソフトウェアを設計する際，シーケンス図が幅広く利用されている．しかし，従来シーケ ンス図の正しさを自動的に検証することは困難であった．我々はシーケンス図を検証するために SDVerifier という ツールを開発している．SDVerifier はシーケンス図を CSP のプロセスに変換することによって，既存のモデル検 査器で検証可能とする．また，モデル検査器が出力する反例を逆変換して元のシーケンス図に戻すことによって，問 題が発見された場合に効率的に原因を調査できる．本論文では，SDVerifier の機能を説明し，実システムでの試行 によりその有効性を確認したことを報告する．Sequence diagrams are often used in the modular design of softwares. However, it is difficult to verify UML diagrams automatically. In this work, we develop a verification tool of sequence diagrams named SDVerifier. It converts sequence diagrams to processes in CSP, so that existing model checking tool can verify them. One of the main contributions in this work is that counter examples found in the model checking can be translated back to sequence diagrams for supporting to correct their inconsistency. We implemented the tool and conducted experiments with real world case studies.
1 はじめに
近年，ソフトウェア開発ではより短い納期で多品種 化・マルチプラットフォーム化への対応が求められる ようになっている．そのような要求にこたえ効率的に システムを開発するために，コンポーネントを利用し たソフトウェア開発が広まっている． ソフトウェアコンポーネントの構造やふるまいを定 義する際には，OMGによって標準化されたモデリン グ言語であるUML [11]がしばしば利用される．ソ フトウェアの上流設計では，コンポーネントの相互作 用を理解し検証するために，UMLのうち特にシーケSDVerifier: A Tool for Verification of Sequence Dia-grams using the Process Algebra CSP.
Tomohiro Kaizu, Masato Suzuki, 北陸先端科学技術大 学院大学, Japan Advanced Institute of Science and Technology.
Yoshinao Isobe, 産業技術総合研究所, National Institute of Advanced Industrial Science and Technology. コンピュータソフトウェア, Vol.32, No.1 (2015),pp.234–252. [研究論文] 2014 年 1 月 15 日受付. ンス図が利用されることが多い． しかし，シーケンス図の仕様は複雑かつ柔軟であ り，シーケンス図を自動的に検証することは難しい． 設計の不整合や不完全な詳細化などのシーケンス図 の誤りを発見するのは人手での確認にたよっている場 合が多い．そのような誤りが開発の上流工程で発見さ れず下流工程で発見された場合，修正には多くの時間 とコストが必要となる． シーケンス図を検証する手法として，我々は論文 [7]において，形式的な意味論をもつシーケンス図の サブセットを定義し，そのシーケンス図で記述された 設計の正しさを検証する手法を提案した．この手法で は，開発者は状態不変式を用いて各コンポーネントの 状態変化を形式的に記述できる．本手法を用いること で，開発者は形式的な記述により仕様を明確にするこ とができ，検証ツールによって早期に誤りを発見する ことが可能となる． 本手法では，シーケンス図を検証するために，複数 のシーケンス図を合成してシステムのふるまいを導出 し，プロセス代数CSP (Communicating Sequential
Processes) [6] [13]で記述されたプロセスを生成する． この合成手法は次のように実現される．まず，シーケ ンス図から各コンポーネントのメッセージ送受信と状 態変化の情報を抽出する．この情報はCSPのプロセ スとして形式的に記述することができる．次に，同一 のコンポーネントの同一の状態を起点としたCSPの プロセスを集め，論文 [7]で提案したシーケンス図合 成演算子を用いて合成する．最後に，合成されたプロ セスに対してシーケンス図合成演算子の展開規則を 適用し，通常のCSPプロセスへと変換する．シーケ ンス図合成演算子を含まない CSPプロセスはPAT [14]やFDR2 [4]などの既存のモデル検査器により検 証が可能である． 論文[7]では，上記の合成手法の有効性を示すため のプロトタイプとしてSD2CSPというツールを開発 し，説明した． 本論文では，SD2CSP を元に開発した新しいツー ルであるSDVerifierについて述べる．SDVerifierは， 設計工程の上流において適用することを想定してい る．ソフトウェアの機能を実現するためのコンポーネ ントを設計するにあたり，不整合なくコンポーネント の分割ができていること，適切に状態が定義できてい ることを検証できる．状態を明記しなくても検証は可 能であるが，状態を明記することによって，より詳細 にふるまいを検証できるようになる．このツールは， 実際のプロジェクトで活用可能とするため，SD2CSP と比較して下記の機能を持つ． • 同一クラスの複数インスタンスへの対応: 例え ば，ホテルにおける「部屋」はそれぞれの部屋が インスタンスとなり，「予約済み」や「空室」など の状態を持つことができる．複数インスタンスへ の対応に関しては3. 1節で詳しく述べる． • オブジェクトの生成および破棄への対応:各オブ ジェクトは ⟨⟨create⟩⟩メッセージで生成し，オ ブジェクト破棄(×)によって破棄することがで きる．オブジェクトの生成および破棄に関しては 3. 2節で詳しく述べる． • シーケンス図編集機能: 検証用のシーケンス図を 簡単に作成できるよう，シーケンス図編集機能を ツールに統合した．これはHTML5およびCSS で実装され，Web上で公開されている．シーケン ス図編集機能に関しては3. 3節で詳しく述べる． • 反例解析機能: 検証により出力された反例を元 のシーケンス図上で可視化することができる．反 例解析機能に関しては3. 4節で詳しく述べる． この論文は次のように構成される．まず，2節で論 文 [7]において提案されたシーケンス図の検証方法に ついて簡単に説明する．3節では，新しいSDVerifier ツールについて，論文 [7]内で示したプロトタイプで あるSD2CSPと比較して説明する．4節では，我々 が行ったケーススタディの結果を示す．最後に，5節 と6節では，関連研究とこの論文の結論について述 べる．
2 シーケンス図の変換の概要
我々は論文 [7]において，シーケンス図で記述され た設計の正しさを検証する手法を提案した．本節で は，この手法の概要を説明する． 図1は簡単なeコマースサイトの設計である．ユー ザは login, addT oCart, buy および logoutをこの サイトで実行できる．ユーザを表す U ser オブジェ クトはlogin メッセージの後でloggedin 状態に状 態が変化し，logoutメッセージの後で元の状態に戻 る．また，システムを表すSystemオブジェクトはaddT oCartメッセージの後でhasCart 状態に状態 が変化し，buyメッセージの後で元の状態に戻る． シーケンス図において，縦の直線はライフラインと 呼ばれ，相互作用の個々の参加者を表す．ライフライ ン間の矢印はメッセージであり，ライフライン間の特 定のコミュニケーションを表す．角丸の長方形は状態 不変式と呼ばれ，実行時の制約として，属性・変数の 値や状態を指定する．本手法では状態不変式をオブ ジェクトの状態を表すために用いる．メッセージ間の 長方形は活性区間と呼ばれ，ライフライン内の1つ のふるまいやアクションを表す． 本手法では，シーケンス図で与えられた複数のシナ リオから状態遷移モデルを自動的に合成することで， モデル検査によるシステムのふるまいの検証を可能 とする． しかし，通常，シーケンス図は特定のシナリオのみ
236 (a) (b) (c) (d) 図1: eコマースサイトのシーケンス図 を表すものであり，シーケンス図に書かれたものと異 なるシナリオが許可されるかどうかは不定である．複 数のシナリオを合成して状態遷移モデルを得る場合， 「出力される状態遷移モデルが入力のシナリオをすべ て実行できる」ことが制約となるが，そのような状態 遷移モデルは一意には定まらない．例えば，「すべて のオブジェクトがすべての状態ですべてのメッセージ を送受信できる」という状態遷移モデルを考えれば， これは任意のシナリオを実行できるため，どのような シーケンス図の入力に対しても正当な合成結果となっ てしまう．これは，シーケンス図の検証という目的に はそぐわない． そのため，本手法におけるシーケンス図のサブセッ トでは，各シーケンス図がどのように状態遷移モデ ルと対応するかも定義する．例えば，図1bにおける U serオブジェクトは，通常のシーケンス図としては 「addT oCartを送信し，okを受信し，buyを送信し，
ok を受信する」という 1シナリオのみしか表さな いが，本手法では「addT oCartもしくはbuyを送信 し，okを受信することを任意回数繰り返す」という 意味を持つ．そのように1つのシーケンス図が複数 のシナリオを表すことで，実用的な状態遷移モデルを 合成して検証することが可能となる． 本手法ではシーケンス図におけるふるまいは次の ように定義される． • 各オブジェクトは，ライフラインにそって上か ら下の順にメッセージを送受信できる． • オブジェクトが状態不変式に到達した場合，同 じ状態名が記述された他の状態不変式の箇所か ら続きのメッセージを送受信できる． • ライフラインの先頭および末尾，活性区間の完 了直後で状態名の明記されていない状態を標準 状態と呼ぶ．状態不変式が書かれている場合と同 様に，オブジェクトが標準状態に到達した場合に は他の標準状態の箇所から続きのメッセージを送 受信できる． また，複数のシーケンス図を合成する際には，次の ようなふるまいが期待される． • 合成後のオブジェクトは，合成前のシーケンス 図に含まれる遷移をすべて実行できる． • 同一のふるまいを表す遷移を複数のシーケンス 図に記述することができる．同一の状態から始ま る同一のメッセージが複数のシーケンス図に記述 されていた場合，それらは同一のふるまいを表す ものであり，実行時にどちらのシーケンス図が選 択されたかは区別できない． • ある状態から送受信可能なメッセージが複数記 述されていた場合，送信オブジェクトがそのうち の1つを非決定的に選択して送信する．ソフト ウェアの実装ではオブジェクトの内部状態によっ て決定的にメッセージが選択されるが，シーケン ス図が使われる上流設計では，条件判断に必要な 情報が記述されない場合が多い．そのような場 合，非決定的な選択としてCSPに変換すること で，詳細化後のモデルとの詳細化関係の検証が可 能となる．一方，受信オブジェクトは選択は行わ ず，送信オブジェクトが選択したメッセージがど れであっても受信できる必要がある． ソフトウェアの開発プロセスにおいては，シーケン ス図には状態を記述せず，状態の定義は次の工程でス
テートマシン図を用いて始める場合も多い．本手法で は，状態不変式が記述されていない場合でも，各オブ ジェクトが「標準状態」という特別な状態にあるもの として変換・検証を行うことができる．そのような場 合でも，活性区間の途中の状態は特別な状態として扱 われるため，各活性区間内でソフトウェアの挙動が網 羅されていることは確認できる． 本手法を用いたソフトウェアの開発プロセスでは， 状態を記述しないシーケンス図から始めて段階的に 状態を追加していくことで，シーケンス図設計から段 階的に状態遷移設計を得ることができるようになる． 従来手法におけるシーケンス図設計でも，多くの場合 「このシーケンス図はユーザーログイン後のシナリオ である」というような情報が自然言語で与えられてい た．そのような情報を機械処理可能な状態不変式で置 き換えることは困難ではないと考えられる． 本手法では，シーケンス図をCSPに変換して検証 する．CSPへの変換は上述のシーケンス図のふるま いの定義に従い，次のように定義できる．まず，シー ケンス図のメッセージはCSPのイベントに変換でき る．また，状態不変式はCSPにおけるプロセスの状 態に変換できる．例えば，図1aの左側のライフライ ンはU ser オブジェクトが loginメッセージを送信 し，okメッセージを受信し，loggedIn状態へ遷移す ることを表しているため，次のようなCSPのプロセ スに変換できる．
U ser def ault1 =
Login→ OK → User loggedIn
ここで，シーケンス図は実行可能なひとつのシナリオ を表しており，U serが実行可能なイベントはLogin
のみとは限らないため，U serのdef ault状態(標準 状態)にインデックス1を付けてU ser def ault1 と
している．すなわち，U ser def ault1 はU serが実
行可能なふるまいの一部である．このようなインデッ クスはシーケンス図からCSPプロセスを生成すると きに自動的に付加される．図1の他の状態について も同様に，次のように変換できる．
System def ault1=
Login→ OK → System default U ser loggedIn1=
Add→ OK → User loggedIn U ser loggedIn2=
Buy→ OK → User loggedIn System def ault2=
Add→ OK → System hasCart System hasCart1=
Buy→ OK → System default U ser loggedIn3=
Buy→ Empty → User loggedIn System def ault3=
Buy→ Empty → System default U ser loggedIn4=
Logout→ OK → User default System def ault4=
Logout→ OK → System default Login = call .login.U ser.System
Add = call .addT oCart.U ser.System Buy = call .buy.U ser.System Logout = call .logout.U ser.System
OK = call .ok.System.U ser Empty = call .empty.System.U ser
ここで，a→ P はイベントa を実行した後P と同 様にふるまうCSPのプロセスである．call はシー ケンス図のメッセージと対応するCSP のイベント であり，メッセージ名，送信オブジェクト，受信オブ ジェクトをパラメータとして持つ． これらのプロセスはそれぞれのシナリオにおける オブジェクトのふるまいをCSPに変換したものであ り，検証のためにはこれらのシナリオベースのモデル から状態ベースのモデルを合成する必要がある．その ため，本手法ではシーケンス図マージ演算子◦と内 部選択化演算子$という2つの新しい演算子を導入 する．◦演算子と$演算子をあわせてシーケンス図 合成演算子と呼ぶ．これらの演算子を用いると，例え ばU ser loggedInプロセスは次のように表せる．
U ser loggedIn = (U ser loggedIn1
◦ User loggedIn2
◦ User loggedIn3
◦ User loggedIn4)
238
ここで，U ser loggedIn1...4はU serオブジェクトの
loggedIn状態から始まるシナリオを列挙したもので あり，{Login, Add, Buy, Logout}はU serオブジェ クトの送信メッセージ集合である．
◦ 演算子は複数のシーケンス図中の同一のイベ ントを 1 つの CSP のイベントに集約する．例え ば，U ser loggedIn2 は Buy イベントの後に OK
を受信できることを表し，U ser loggedIn3 はBuy
イベント後にEmpty を受信できることを表してい る．これらを合成したプロセス (U ser loggedIn2◦
U ser loggedIn3) は，Buy イベントの後にOK と
Emptyのどちらのイベントも受信可能なプロセスと なる．2つのシナリオに共通するBuyイベントは同 一のメッセージを参照しており，どちらのシナリオが 選択されたかはOKもしくはEmptyのイベント発 生後にしか区別できない． 形式的には，◦演算子は次のような性質を持つ． (a→ P ) ◦ (a → Q) =F a→ (P ◦ Q) (a→ P ) ◦ (b → Q) =F (a→ P ) 2 (b → Q) if a ̸= b ここで，aとbはイベントであり，PとQはプロセス である．2 は外部選択と呼ばれ，(a→ P ) 2 (b → Q) は外部環境がa もしくはbを選択することができ， その選択に従ってa→ P もしくはb→ Qのように ふるまうプロセスを表している．等号記号=F は失 敗等価と呼ばれ，2つのプロセスが同一のトレースを 実行でき，それぞれのプロセスの対応する状態どう しでは失敗の可能性があるイベント集合(各状態で実 行できないイベントの集合)が等しいことを表してい る．失敗等価は決定的な選択と非決定的な選択を区別 する． この性質を用いると，U ser loggedInプロセスは 次のように変換できる． U ser loggedIn =F
(Add→ OK → User loggedIn
2 Buy → (OK → User loggedIn 2 Empty → User loggedIn) 2 Logout → OK → User default)
${Login, Add, Buy, Logout}
$演算子は送信イベントに対応する選択を外部選択 ではなく内部選択とするために用いる．本ツールが対 象とする上流設計では詳細なデータ操作が確定され ていないため，非決定的な選択が必要となる．例えば 「ユーザー名とパスワードが正しければログイン成功 メッセージを返し，ユーザー名とパスワードが不正で あればログイン失敗メッセージを返す」という設計に おいて，パスワードの保存方法やチェック方法がまだ 設計されていなければ，どちらのメッセージを返す べきかを決定的に記述できない．そこで，複数のメッ セージが送信可能な場合には，送信側のオブジェクト は非決定的にいずれかのメッセージを選択するものと する．シーケンス図をCSPに変換する場合，合成さ れたプロセスに「$(送信メッセージ集合)」を適用す ることでこのふるまいをモデル化する． 内部選択化演算子$は次のような性質を持つ． ((a→ P ) 2 (b → Q))$Z =F (a→ P $Z) ⊓ (b → Q$Z) if a ∈ Z, b ∈ Z ((a→ P ) 2 (b → Q))$Z =F (a→ P $Z) 2 (b → Q$Z) if a ̸∈ Z, b ̸∈ Z ((a→ P ) 2 (b → Q))$Z =F (a→ P $Z) ▷ (b → Q$Z) if a ∈ Z, b ̸∈ Z ここで，Z はイベント集合である．⊓は内部選択と 呼ばれ，(a → P ) ⊓ (b → Q)は a → P もしくは b→ Qのようにふるまうプロセスを表す．a もしく はbはプロセス内部で非決定的に選択される．▷は タイムアウト演算子と呼ばれ，(a→ P ) ▷ (b → Q) は最初はa→ P のようにふるまい，しばらくすると b→ Qのようにふるまうプロセスを表す．a が実行 されるかどうかはプロセス内部で非決定的に選択され る．一方，bはaが実行されない限り拒否されない． また，$演算子について，次のような性質も成り 立つ． (a→ P )$Z =F a→ P $Z (P $Z)$Z =F P $Z これらの性質を用いると，U ser loggedInプロセ スは次のように変換できる． U ser loggedIn =F
(Add→ OK → User loggedIn
⊓ Buy → (OK → User loggedIn 2 Empty → User loggedIn)
(a) User モデル
(b) System モデル
図2: 図1から合成されたCSPモデル
⊓ Logout → OK → User default)
図2は図 1のシーケンス図から合成された CSP モデルである．τ は内部イベントであり，内部選択に おける選択を表している． ◦演算子と$ 演算子を用いた任意のCSPモデル は，これらの演算子を含まない標準的なCSPモデル に変換できる．変換された標準的なCSPモデルは， 既存のモデル検査器により検証できる． 例えば，図2のU serモデルとSystemモデルを 並行合成したプロセスを検証するとデッドロックが 検出される．login→ ok → addT oCart → ok とい うトレースの後，U serはloggedin状態にあり，buy
もしくはlogoutもしくはaddT oCartメッセージを 送信できる．しかし，SystemはhasCart状態にあ り，buyメッセージしか受信できない．もしU serが
logoutもしくはaddT oCartを選択した場合，この モデルはデッドロックする．開発者はこのような状況 を考慮し，logoutやaddT oCartが送信された場合 のシーケンス図を作成する必要がある． また，開発者が抽象モデルと詳細モデルを記述すれ ば，CSPの詳細化関係もしくは同値関係を検証する ことで，詳細化が正しく行われたかどうかも検証でき る．検証の詳細は論文 [7]で公開されている．
3 検証ツール SDVerifier
SDVerifierはモデル検査器PAT [14]を用いてシー ケンス図を検証するためのツールである．このツール は，シーケンス図をPATで検証できるCSPモデル に変換し，また，PATによる解析結果を逆変換して シーケンス図上に表示する．本節では，論文 [7]で紹 介したプロトタイプであるSD2CSPからの変更点を 中心にこのツールの機能を説明する． SD2CSPからの主な変更点としては，下記の4点 が挙げられる． • 同一クラスの複数インスタンスへの対応 • オブジェクトの生成および破棄への対応 • シーケンス図編集機能 • 反例解析機能 これらは，ホテルの予約システムやECサイトのカ スタマーサポートシステムのケーススタディなどで 実際にSD2CSPを適用する中で，重要度が高いと考 えられた機能である．これらの機能により，上流工 程で作成されるシーケンス図でよく使われる機能を SDVerifierで検証できるようにすることを目指して いる． SD2CSPの問題点としては，検証可能なシーケン ス図の記述力が不足していたことと，ツールのユーザ ビリティが低く検証結果をフィードバックしてシーケ ンス図を修正することが困難だった点が挙げられる． 「同一クラスの複数インスタンスへの対応」と「オ ブジェクトの生成および破棄への対応」はシーケンス 図に十分な記述力を与えるための変更である．上流工 程での設計において，ホテルで複数の部屋がある場合 など，同一クラスの複数インスタンスが存在してそれ らの間での相互作用が必要となることは多い．一方， 例えば具体的なデータの受け渡しやデータの大小比 較等は必ずしも重要ではない．上流工程での設計に おいては具体的なデータに基づく条件分岐ではなく， 「予約が成功する場合もあるし，キャンセル待ちにな240 図3: ホテル予約システムのシーケンス図 る場合もある」のような非決定的な選択が記述できれ ば提案手法を用いて十分有益な検証が可能である．上 流工程でのシーケンス図を調査する中で，この2つ の機能を実現すれば多くの設計が検証可能になると 判断した． 「シーケンス図編集機能」と「反例解析機能」は ツールのユーザビリティ向上のための変更である． SD2CSPではシーケンス図の入力として XMI形式 を用いていたが，XMI形式にはツール依存の挙動 があり，使用するシーケンス図編集ツールによって は正しく検証ができないという問題があった．また， SD2CSPでは検証に失敗した場合にモデル検査ツー ルの出力を直接開発者が読み取る必要があり，入力と なるシーケンス図のどこに問題があるかを調査する のが難しかった．この2つの機能を実現することで， シーケンス図の編集，検証，結果の確認とシーケンス 図の修正という一連のプロセスをスムーズに適用す ることが可能となった．
SDVerifier はDart 言語で実装され，JavaScript
にコンパイルされてWebで公開されている．そのた め，HTML5とCSS3をサポートする任意のブラウ ザで実行することができる．SDVerifierと図1，図3 に対応するサンプルデータは下記のURLでアクセス できる． • SDVerifier – http://dr.asukaze.net/sdverifier/editor.html • 図1 – http://dr.asukaze.net/sdverifier/ demo.cgi?model=cart • 図3 – http://dr.asukaze.net/sdverifier/ demo.cgi?model=hotel 3. 1 同一クラスの複数インスタンスへの対応 シーケンス図ではオブジェクト間の相互作用が検証 されるが，ソフトウェアのシステムにおいて複数のオ ブジェクトが1つの仕様に基づいて同じふるまいを する場合は多い．例えば，図3はホテル予約システム のシーケンス図である．このうちU ser[user id1]と U ser[user id2] は異なるオブジェクトであるが，両 方とも Userクラスのインスタンスであり，User ク ラスで定められた同一のふるまいをすることが期待 される．SDVerifierでは，同一クラスの複数インス タンスが設計に存在する場合，複数インスタンスのふ るまいからクラスのふるまいを合成し，検証するこ とを可能とした．もし1つのクラスが複数のインス
タンスを持つ場合，シーケンス図では「ClassName [IdName]」のように記述する．ここで，ClassName はそのオブジェクトのふるまいを規定するクラスの名 前であり，IdNameは特定のインスタンスを識別する ための名前である． 2節でも述べたように,通常のシーケンス図は特定 のシナリオのみを表すものであるが，本手法ではシー ケンス図で記述されたシナリオから状態遷移モデル を合成して検証するため，シーケンス図と状態遷移モ デルとの対応関係も定義する．この対応関係の定義に あたっては，実際のシーケンス図を調査し，開発者が 自然に期待するふるまいと近くなるよう考慮した． まず，同一クラスのインスタンスは同じふるまいを するため，1つのインスタンスは異なるライフライ ンで記述されたふるまいを実行できる．例えば，1つ のUserオブジェクトが，あるときはU ser[user id1]
としてふるまい，別のあるときはU ser[user id2]と してふるまうことができる．つまり，各インスタン スが固定された名前としてuser id1やuser id2を 持っているのではなく，user id1やuser id2はこの シナリオの中でのみ有効な名前である．本手法によ る変換規則では，各インスタンスはどのシナリオで も変化しない0, 1, 2 . . .という整数値の名前を持つこ ととする．この名前をプロセスIDと呼ぶ．user id1 やuser id2は1つのシナリオの中で1つのプロセ スIDを保持する変数であるとみなす． 次に，メッセージを受信するインスタンスについ て考える．直観的に，返信メッセージは対応する同期 メッセージの送信元オブジェクトに返されるというこ とが期待される．しかし，送信元のクラスが複数のイ ンスタンスを持つ場合，それらのうちどのインスタ ンスに返信メッセージを返すべきなのかは，返信メッ セージを送信するオブジェクトが記憶している必要が ある．そのため，本論文の変換規則では，各オブジェ クトが他のオブジェクトのプロセスIDを記憶できる こととする．この記憶領域をここではメモリと呼ぶ． メモリを持つふるまいは，状態遷移モデルとしては メモリに格納される可能性のある値の種類だけ状態 遷移を複製したものである．この「プロセスID」と 「メモリ」という考え方を用いると，返信メッセージ 以外のメッセージも含め，メッセージを受信するイン スタンスは次のように定められる． • もし送信オブジェクトが受信オブジェクトのプ ロセスIDを知っている場合，そのIDを持つオ ブジェクトがメッセージを受信する． • もし送信オブジェクトが受信オブジェクトのプ ロセスIDを知らない場合，受信オブジェクトは 非決定的に選択される． ここで，「知っている」とは，シーケンス図中の Id-Nameと対応するプロセスIDがメモリに存在する ことを表す．オブジェクトが他のオブジェクトとメッ セージの送受信をする際に相手のプロセスIDがメモ リに加えられ，活性区間の終了時にメモリは破棄さ れる． さらに，メモリの内容をより詳細に設計可能とする ため，メッセージのパラメータおよび状態のパラメー タに関する変換規則を定義する．本手法では，シーケン ス図中のメッセージは「MessageName(Parameters)」 の形式でパラメータを持つことができる．ここで， Pa-rametersは送信オブジェクトが知っているIdName のリストである．状態遷移モデルでは対応するプロ セス IDが受け渡しされ，受信オブジェクトは受信 したプロセスIDをメモリに追加する．これにより， 受信オブジェクトはそのプロセスIDで指定したイ ンスタンスにメッセージを送信することが可能とな る．また，シーケンス図中の状態不変式も「 State-Name(Parameters)」の形式でパラメータを持つこと ができる．ここで，Parametersはそのオブジェクト が知っているIdNameのリストである．活性区間の 直後にパラメータを持つ状態不変式がある場合，状態 不変式のパラメータに指定されたIDは次の活性区間 の完了まで保持される． 上記をまとめると，本論文の変換規則は論文 [7]の 変換規則を次のように拡張したものである． • オブジェクトがメッセージを受信した場合，送 信オブジェクトの IDおよびメッセージのパラ メータがメモリに加えられる．例えば，図3に おいて，Hotelオブジェクトはcancel(rsv id1)
メッセージを受信した後，その送信オブジェクト であるU ser のIDをメモリ上に保持する．こ
242 れにより，Hotelオブジェクトはcancelledメッ セージを同一のU ser オブジェクトに返却する ことができる． • オブジェクトがメッセージを送信する場合，も し受信オブジェクトのIDがメモリに存在するな らば，そのIDのオブジェクトのみがメッセージ を受信できる．例えば，図3でHotelオブジェ クトからU ser[user id2]オブジェクトに送信さ れるresered(rsv id2)メッセージを受信できる のは，W aiting[wait id]オブジェクトが保持し ていたuser id2をIDとして持つU serのみで ある． • オブジェクトがメッセージを送信する場合，もし 受信オブジェクトのIDがメモリに存在しないな らば，受信オブジェクトはそのメッセージを受信 可能なオブジェクトのうち1つが自動的に選択さ れる．選択されたIDは送信オブジェクトのメモ リに加えられる．例えば，図3中で，getU serId メッセージは任意の W aiting オブジェクトが 受信できる．それに続くcancel(user id2)メッ セージはgetU serIdメッセージで選択されたオ ブジェクトのみが受信できる． • 活性区間の完了時に，その活性区間中で記憶され たメモリは破棄される．ただし，活性区間の直後に パラメータを持つ状態不変式がある場合，状態不変 式のパラメータに指定されたIDは次の活性区間 の完了まで保持される．例えば，図3中で，Hotel のメモリは reserved(rsv id2) メッセージの送 信後に削除される．また，Reservation[rsv id2] のメモリはreserved(rsv id2)メッセージの後で 削除され，user id2のみ保持される． な お ，各 ク ラ ス の イ ン ス タ ン ス 数 に つ い て は シーケンス図のみからでは決定できない．例えば， 図 3 で は Reservation ク ラ ス の イ ン ス タ ン ス は
Reservation[rsv id1] およびReservation[rsv id2]
の2つであるが，これはReservationクラスのイン スタンス数が2であることを意味しない．実際には より多くのインスタンスが存在するが，その中でこ のシナリオに登場する2インスタンスのみが記述さ れている可能性がある．そのため，SDVerifierでは， インスタンスの最大数は開発者が任意の有限の値を 設定できる．例えば，仮にプロセスの最大数が3と 設定されていた場合，Reservation[rsv id1] および Reservation[rsv id2] は次のようなプロセスに変換 される． Reservation (0) || Reservation (1) || Reservation (2) こ こ で ， || は PAT の 並 行 合 成 演 算 子 で あ り，Reservation (x) は Reservation[rsv id1] と
Reservation[rsv id2]を合成して得られる状態遷移モ デルである．Reservation (0)とReservation (1) と Reservation (2) は，Reservation (x) にした がって同じふるまいをする3つのプロセスとなって いる．図4はReservation プロセスの定義である． 図5 は図3 のHotelオブジェクトから上述の変 換規則に基づいて変換された CSPプロセスである． ここで，[*]はPATで外部選択を表す記号である． シーケンス図のメッセージは次のようなCSPのイベ ントに変換されている．
call ! SenderClass . ReceiverClass . M essageN ame . P arameters . SenderId . ReceiverId
call ? SenderClass . ReceiverClass . M essageN ame . P arameters . SenderId . ReceiverId
こ こ で ，! は メッセ ー ジ 送 信 を 表 し ，? は メッ セ ー ジ 受 信 を 表 し て い る ．例 え ば ，call_?User .Hotel.cancel.b1_.b2_.0 はHotelが U serから
cancelメッセージを受信するためのイベントであり， b1_はメッセージのパラメータ，b2_は送信オブジェ クト，0は受信オブジェクトのIDを表している．1 つのメッセージが複数のパラメータを持つ場合もあ るので，Parametersは実際には可変長であり，パラ メータの個数分の値を「.」で区切ったものとなる． メッセージがパラメータを持たない場合，CSPのイ ベントは次のような5つ組となる．
1 Reservation__(id_) = ( 2 call_?Hotel.Reservation.create.0.id_ -> Reservation_i3_i30_(id_) 3 [*] end_ -> Skip); 4 5 Reservation_i3_i30_(id_) = 6 call_?Hotel.Reservation.reserve.b1_.0.id_ 7 -> Reservation_i31_i4_(id_, b1_); 8 9 Reservation_i31_i4_(id_, a1_) = 10 call_!Reservation.Hotel.reserved.id_.0 11 -> Reservation_reserved_(id_, a1_); 12 13 Reservation_reserved_(id_, a1_) = 14 call_?Hotel.Reservation.cancel.a1_.0.id_ -> Reservation__(id_); 15
16 System_() = User_default_(0) || User_default_(1)
17 || User_default_(2) || Hotel_default_() || Waiting__(0) 18 || Waiting__(1) || Waiting__(2) || Reservation__(0) 19 || Reservation__(1) || Reservation__(2);
図4: 変換されたReservationのCSPプロセス(プロセス数の最大値は3)
. M essageN ame . SenderId . ReceiverId
call ? SenderClass . ReceiverClass
. M essageN ame . SenderId . ReceiverId
変換されたCSPでは，プロセスのパラメータがメ モリを保持するために使われている．図5では，a1_， a2_，a3_，a4_，a5_がオブジェクト内に保持されて
いるメモリである．複数のシーケンス図の中では同じ パラメータが異なる名前を持つ場合があるため，CSP への変換の過程でシーケンス図中で用いられている 名前は連番に変換される．この連番はオブジェクトが その値を受け取った順序と対応しており，複数のシー ケンス図で同じメッセージの送受信が記述されてい れば同一のパラメータは同一の番号に変換されるよ うになっている．同じメッセージが複数のシーケンス 図に記述されている場合，◦演算子 によってそれら は1つのCSPのイベントに集約されるため，このよ うな名前の付け替えが必要となる．この例では，a1_
がrsv id1と，a2_がuser id1と，a3_がwait id
と，a4_がuser id2と，a5_がrsv id2と対応して いる．この対応関係は1つのシーケンス図のライフ ラインをCSPに変換する間は保持されており，シー ケンス図中に記述されているID，メッセージや状態 不変式のパラメータはこの対応関係にしたがって変換 される．一方，複数のシーケンス図をシーケンス図合 成演算子で合成する際には，シーケンス図に記述され た名前ではなく連番のみを用いて合成が行われる． 図5では，2行目のcancelメッセージや17行目 の ok メッセージを受信した後，送信オブジェクト のIDとメッセージのパラメータがメモリに加えられ る．6行目のcancelメッセージ，9行目のcancelled メッセージ，31行目のreserveメッセージ，および 39行目のreserved メッセージでは，受信オブジェ クトのIDと対応するパラメータがメモリに保持さ れているため，そのメモリの値によって受信オブジェ クトが決定される．13行目のgetU serIdメッセージ では，受信オブジェクトのIDであるwait idがメモ リに存在しないため，このメッセージを受信可能なオ ブジェクトのうち1つが外部選択[*]により選択さ れる．選択されたIDはb3_としてメモリに加えら れている．27行目のcreateメッセージも同様に，受 信可能なオブジェクトのうち1つが選択され，その IDがメモリに加えられている．39行目のreserved メッセージの送信後，メモリはすべて破棄される． SDVerifierで用いる変数はプロセスIDのみであ り，それ以外のデータは検証に用いない．入力モデル 内で算術演算子や制御構造を記述可能とすればプロ
244 1 Hotel_default_() = (( 2 call_?User.Hotel.cancel.b1_.b2_.0 -> Hotel_i1_(b1_, b2_) 3 ) [*] end_ -> Skip); 4 5 Hotel_i1_(a1_, a2_) =
6 call_!Hotel.Reservation.cancel.a2_.0.a1_ -> Hotel_i2_(a1_, a2_); 7
8 Hotel_i2_(a1_, a2_) =
9 call_!Hotel.User.cancelled.0.a2_ -> Hotel_i4_(a1_, a2_); 10
11 Hotel_i4_(a1_, a2_) = Hotel_i4__sub_1_(a1_, a2_); 12 Hotel_i4__sub_1_(a1_, a2_) = (
13 [*] b3_:{0..2}@ call_!Hotel.Waiting.getUserId.0.b3_ 14 -> Hotel_i6_(a1_, a2_, b3_));
15
16 Hotel_i6_(a1_, a2_, a3_) =
17 call_?Waiting.Hotel.ok.b4_.a3_.0 18 -> Hotel_i7_(a1_, a2_, a3_, b4_); 19
20 Hotel_i7_(a1_, a2_, a3_, a4_) = 21 call_!Hotel.Waiting.cancel.a4_.0.a3_ 22 -> Hotel_i8_(a1_, a2_, a3_, a4_); 23
24 Hotel_i8_(a1_, a2_, a3_, a4_) =
25 Hotel_i8__sub_1_(a1_, a2_, a3_, a4_); 26 Hotel_i8__sub_1_(a1_, a2_, a3_, a4_) = (
27 [*] b5_:{0..2}@ call_!Hotel.Reservation.create.0.b5_ 28 -> Hotel_i9_(a1_, a2_, a3_, a4_, b5_));
29
30 Hotel_i9_(a1_, a2_, a3_, a4_, a5_) = 31 call_!Hotel.Reservation.reserve.a4_.0.a5_ 32 -> Hotel_i12_(a1_, a2_, a3_, a4_, a5_); 33
34 Hotel_i12_(a1_, a2_, a3_, a4_, a5_) = 35 call_?Reservation.Hotel.reserved.a5_.0 36 -> Hotel_i13_(a1_, a2_, a3_, a4_, a5_); 37
38 Hotel_i13_(a1_, a2_, a3_, a4_, a5_) =
39 call_!Hotel.User.reserved.a5_.0.a4_ -> Hotel_default_(); 図5: 変換されたHotelのCSPプロセス セスID以外の変数を検証対象とすることも可能では あるが，シーケンス図はそのような詳細なふるまいを 記述するには適しておらず，シーケンス図を検証対象 とするSDVerifierではそのような需要はないと考え られる． 3. 2 オブジェクトの生成および破棄への対応 SDVerifierはシナリオ中でのオブジェクトの生成 と破棄に対応している．⟨⟨create⟩⟩ メッセージやオ ブジェクト破棄(×)を含むシーケンス図を変換す ると，SDVerifierは停止状態のオブジェクトとして CSPのプロセスを生成する．停止状態のプロセスは ⟨⟨create⟩⟩メッセージのみを受信できる．⟨⟨create⟩⟩ メッセージを受信した後は通常のオブジェクトのよう にふるまう．シーケンス図中の×は停止状態への状 態遷移に変換される． 例えば，図 4は図 3のReservationオブジェク トから変換されたCSPのプロセスである．1行目の Reservation__が停止状態のプロセスを表す．2行 目でcreateメッセージを受信すると通常の状態に遷
移する．14行目でcancelメッセージを受信すると このプロセスは停止状態に戻る． ここで，動的なオブジェクトを検証するためには， オブジェクトの個数の最大値を有限個に制限する必要 がある．制限されたモデルでは，実際のシステムでは 起こりえないデッドロックが発生する場合がある．例 えば，図3のホテル予約システムでは，ホテルはユー ザの予約リクエストに対し非決定的にReservation オブジェクトもしくはW aitingオブジェクトを作成 する．しかし，もしすべてのユーザがキャンセル待ち となった場合，予約をキャンセルするユーザがいなけ ればどのユーザもそれ以上処理が進められなくなる． PATツールはこれをデッドロックとして報告するが， もしU ser，Reservation，W aitingの各クラスのイ ンスタンス数が十分に大きければ，キャンセル待ちの ユーザは他のユーザのキャンセルを待つことができる ので，これはデッドロックとはならない． SDVerifierでは，このような誤判定に対し，「End states」という変換オプションを設けている．これは， オブジェクトの各状態に対し，その後に状態遷移が必 要であるかを指定するものである．例えば，活性区間 の途中でメッセージの受信を待っている状態では，い つかはメッセージを受信して状態遷移をすることが 期待されている．しかし，W aitingオブジェクトは， その後に誰も予約をキャンセルするユーザがいなけれ ば，そのままwaiting状態で存在し続けるオブジェ クトであり，その後に状態遷移が起こらない可能性が ある．このような場合，その後に状態遷移が起こらな くてもデッドロックと判定すべきでない状態を「End states」として指定する．すべてのプロセスの状態が 「End states」に含まれれば，検証ツールは処理でき るイベントが存在しない場合でもデッドロックを報告 しない．これにより，モデル検査が重要な問題を発見 する前に誤判定によって停止する問題を回避する． どの状態が「End states」にあてはまるかは，開発 者による設計事項のひとつである．例えば，キャンセ ル待ちが一定期間後に無効になるという設計であれ ば，予約をキャンセルするユーザがいない場合でもい つかはW aitingオブジェクトがwaiting状態から他 の状態に遷移することが期待される．そのような設計
であればwaiting状態は「End states」に含めるべ きではない．開発者は，その状態のままオブジェクト が存在し続けることに問題がないかを考慮して「End states」を指定する必要がある． SDVerifierは指定された状態を変換する際，次の ようなプロセスを出力する． P2 end → SKIP ここで，P はシーケンス図から変換された通常のプ ロセスである．例えば，図 5 ではHotel オブジェ クトのdef ault状態が「End states」として指定さ れており，3行目に「[*] end_ -> Skip」が出力さ れている．また，停止状態は暗黙的に「End states」 と し て 扱 わ れ る ．そ の た め ，図 4 の 3 行 目 に も 「[*] end_ -> Skip」が出力されている． すべてのプロセスの状態が「End states」に含まれ る場合，end イベントが実行可能となる．end イベ ントが実行されるとすべてのプロセスが成功終了を 表すSKIP 状態となるため，PAT ツールはこれを デッドロックとして報告しない． 3. 3 シーケンス図編集機能 検証用のシーケンス図を簡単に作成できるように， SDVerifierはシーケンス図編集および表示機能をツー ルに統合した．このシーケンス図編集機能では，独 自の文法を用いてシーケンス図を記述する．図6は SDVerifierのスクリーンショットである．開発者は画 面の左上のテキストエリアにシーケンス図を記述で きる．テキストエリアの内容が変更されると，右側の シーケンス図が動的に更新される． 本ツールがシーケンス図編集および表示機能を統 合しているのは，以下の理由による． • 外部のUMLモデリングツールを活用する場合， 入力ファイルの形式はXMI形式となる．しかし， 後述するようにXMI形式ではツール依存の挙動 があり，UMLモデリングツールによっては検証 ができない場合があった．そのため，本ツールで は入力形式を独自に定義することで入力すべき 情報を明確化した． • 3. 4節で説明する反例解析機能ではCSPのイベ ントと対応するメッセージをハイライト表示する
246 図6: SDVerifierツールのスクリーンショット 機能がある．検証ツールがシーケンス図表示機能 を持つことで設計時と反例解析時に同じ図面を 用いることが可能となった． • 提案手法では，シーケンス図を網羅的に記述し， それらを合成して検証を行う．既存の図面を複 製・変更して新しいシナリオを定義する際には， グラフィカルなモデリングツールよりもテキスト 形式でののほうが効率的な場合がある． 例えば図1b (図7右に再掲)はSDVerifierの記法で は図7左のように記述できる．最初の行はこの図に登場 するオブジェクトを列挙したものである．残りの行にメ ッセージと状態不変式を記述する．「User @loggedin」 はU serのライフライン上のloggedin状態不変式を 表す．これはU serオブジェクトがloggedin状態にあ ることを示している．「User -> System addToCart」
はU ser からSystemに送信されるaddT oCartと いう名前のメッセージを表す．また，「{」 により，受 信オブジェクトでこのメッセージから活性区間が開始 されることを表している．「User <- System ok」は Systemから U ser に送信されるok という名前の メッセージを表す．また，「}」により，送信オブジェ クトの活性区間がこのメッセージで終了することを表 している． 論文 [7]で述べたSD2CSPでは，シーケンス図の 入力形式としてXMI形式 [12]のファイルを用いて いた．しかし，XMI形式には若干のツール依存の挙
User System User @loggedin
User -> System addToCart { User <- System ok }
User @loggedin System @hasCart User -> System buy {
User <- System ok } User @loggedin 図7: SDVerifierの記法で記述したシーケンス図の例 動があり，具体的には，シーケンス図に記述された メッセージの順番がXMI形式では保存されないとい う問題があった．これは，メッセージの順番は図面上 の位置関係に基づくものであるが，XMI形式で定義 されるモデルは図面上の位置関係を保持しないため である．SD2CSP では入力ファイル上のメッセージ の記述順序と図面上のメッセージの順序が一致するこ とを仮定していたが，UMLモデリングツールによっ ては別途独自形式の位置情報ファイルを入力しない と正しい順序が得られない場合があった．そのため， SDVerifierでは XMIではなく独自形式の入力を用 いることで入力すべき情報を明確化している．XMI ファイルおよびメッセージの順番を示す情報が入力さ れれば，それらをSDVerifierの形式に変換すること は容易である． 本シーケンス図編集機能は開発途上のものであり， グラフィカルな入力方法への対応や，既存のUMLモ デリングツールごとにXMIファイルの変換機能を用 意して開発者が利用可能なUMLモデリングツール の選択肢を増やすことなどが今後の課題として考え られる． 3. 4 反例解析機能 検証が失敗した場合，PATツールは期待しない状 態になるまでのイベントトレースを反例として出力す る．SDVerifierはこのイベントトレースを逆変換し， 元のシーケンス図上で図示できる．この反例解析機 能を使うと，イベントトレースのそれぞれのステップ で，CSPのイベントに対応するシーケンス図のメッ セージをハイライト表示できる．また，それぞれの オブジェクトの状態とその状態から送受信できるメッ セージの一覧を表示できる．これらの情報を用いるこ とで，期待しない動作の原因を効率的に調べることが できる． 図6のスクリーンショットでは，図1のシーケン ス図をデッドロック検証した結果の反例を表示してい る．左下のセレクションボックスにはイベントトレー スが表示されている．開発者がこの中のイベントを選 択すると，SDVerifierはそのイベントと対応するメッ セージをハイライト表示する．また，右下の表には， それぞれのオブジェクトの状態と送受信可能なメッ セージの一覧が表示される．このスクリーンショット では，最後のokメッセージが選択されている．U ser
はloggedIn状態であり，buy，logout，addT oCart
のメッセージを送信できる．SystemはhasCart状 態であり，buyメッセージを受信できる． この反例解析機能はイベントトレースの実行をエ ミュレートし，それぞれのオブジェクトの状態を判 断している．SDVerifier はシーケンス図をCSP に 変換する際，送信オブジェクトのクラス名とプロセ スID，受信オブジェクトのクラス名とプロセスID， メッセージ名とパラメータを出力するため，隠蔽され たイベントがなければオブジェクトのふるまいを完 全にエミュレートでき，オブジェクトの状態を正確に 出力できる．隠蔽されたイベントがある場合，「state」 と「available messages」は観測できるイベントのみ
248 図8: ケーススタディで用いたシーケンス図の一部 から推測されたものとなる．
4 ケーススタディ
我々は，SDVerifierツールの有効性を確認するた め，実システムを用いたケーススタディを行った [8]． 検証対象となるシーケンス図はある企業の実際のEC サイトのカスタマーサポートシステムのものである． このシステムの開発では検証をするのに十分なシー ケンス図が記述されていなかったため，自然言語によ る設計情報及び実装済みのソースコードをもとに検 証用のシーケンス図を作成した．この検証では，抽象 モデル4枚，詳細モデル8枚の合計 12枚を用意し た．抽象モデルはユーザおよびユーザと直接メッセー ジを交換するフロントエンドのオブジェクトのみを 記述したシーケンス図であり，ユーザのリクエストの 種類と，それらに対してシステムがどのような返答 を返す可能性があるかを記述した．詳細モデルはフ ロントエンドから処理を移譲されるバックエンドの オブジェクトを含めて記述したシーケンス図である． この詳細モデルでは，実装時に別プロセスで動作する サーバごとにライフラインを記述した． 図8は詳細モデルのシーケンス図の中のひとつで ある．このモデルでは，データベースに情報を保存す べき箇所を状態として定義している．本システムで は，ServerCとServerRがそれぞれデータベースを 管理するため，ServerCとServerRに状態不変式が 記述されている． このシーケンス図を検証することで，モデルにデッ ドロックがないことおよびユーザから見て抽象モデル と詳細モデルが同じふるまいをすることを確認でき た．検証にはSDVerifierとPAT ツールのバージョ ン3.2.1を用いた．また，このシーケンス図により各 オブジェクトのふるまいが明確化されているため，今 後システムに変更を加える際にもこのシーケンス図 を参考に設計を行い，変更後のシーケンス図と現在の シーケンス図を比較して検証するといった活用ができ る．従来はシーケンス図を機械的に活用する方法がな かったためシーケンス図がほとんど記述されていな かったが，提案手法の導入によりシーケンス図の記述 を開発者に促すことが可能になると考えられる． 表1は検証対象のモデルのサイズと検証にかかっ た時間をまとめたものである．「シーケンス図」の4 列は検証対象のシーケンス図のページ数，定義され たクラス数，1クラスに対して生成されるオブジェク表1: ケーススタディの結果
(実験環境：2.8 GHz Intel Core i7-2640M CPU，8.0 GB RAM)
シーケンス図 変換 CSP ページ数 クラス数 オブジェクト数 状態数 時間 状態数 検証時間 抽象モデル デッドロック検証 4 3 5 12 0.026s 263 0.026s 詳細モデル デッドロック検証 8 7 10 44 0.049s 6481 0.337s 抽象・詳細モデル 詳細化検証 - - - 20691 0.575s 不正モデル デッドロック検証 8 7 10 44 0.025s - 0.006s トの最大個数を3とした場合の最大オブジェクト数， 状態不変式で定義された状態の数を表している．「変 換時間」はシーケンス図からCSPへの変換にかかっ た時間を表している．「CSP」の2列はPATツール の出力であり，全オブジェクトの状態を組み合わせた システム全体の状態数および検証にかかった時間を表 している． 検証対象の抽象モデルと詳細モデルのそれぞれにつ いてデッドロックが発生しないことと，2つのモデル がユーザの視点で同じふるまいをすることを検証し， すべて1秒以下で検証を完了することができた．な お，2種類のモデルが同じふるまいをすることは，次 のような検証項目で検証した． (AbstractM odel \ X) =F (ConcreteM odel \ X) ここで，AbstractM odelは抽象モデルから変換され たCSPモデル，ConcreteM odel は詳細モデルから 変換されたCSPモデル，X は2つのモデルで共有 されていないイベントの集合である．このケースス タディではユーザが直接入出力をするメッセージは 抽象モデルと詳細モデルで共通していたため，この 検証項目によりそれらのメッセージのふるまいが変 化していないことを検証できた．さらに，SDVerifier でエラーが発見できることを確認するため，図8で
ServerW が送信するref undingとref undの2つ のメッセージの順序を入れ替えて意図的に不正なシー ケンス図を作成した．この不正なシーケンス図に対し ても，1秒以内でこの問題を検出することができた． このケーススタディの検証対象であるシーケンス 図では，同一クラスの複数インスタンス，メッセー ジおよび状態のパラメータ，オブジェクトの生成が使 用されている．ケーススタディを通して，SDVerifier がこれらを適切に表現し，実用的な時間で解析できる ことを確認できた．シーケンス図からCSPへの変換 に関しては3節で提案した手法を用いれば手作業で 変換することもできる．しかし，手作業での変換には 時間がかかり，変換時に誤りが発生する場合もある． SDVerifierでの変換時間は本ケーススタディでは100 ミリ秒以内であり，変換に時間をかけずにシーケンス 図の修正と検証を繰り返すことが可能である． また，不正なシーケンス図を入力とした場合では， PATツールの出力は図9のようなイベントトレース のみであった．この情報のみでは，シーケンス図とイ ベントトレースの関係がわかりづらく，バグの発見に は時間がかかる．ここで，このイベントトレースを反 例解析機能に入力すると，以下の情報が表示される． • デッドロックに至るトレースでは，入力した8 枚のシーケンス図のうち1枚目のシナリオが実 行中である． • デッドロック時，ServerW オブジェクトはi7 状 態 に あ り，次 に 送 受 信 で き る メッセ ー ジ は ref undingである．
250
<init -> [int_choice] -> call_.User.ServerF.request.0.0 -> [int_choice] -> call_.ServerF.ServerR.createsubmit.0.0 -> call_.User.ServerF.request.1.0 -> call_.ServerF.ServerR.createsubmit.0.1 -> call_.ServerR.ServerC.create.0.0 -> call_.ServerC.ServerR.ok.0.0 -> call_.ServerR.ServerW.submit.0.0.0 ->
call_.ServerR.ServerC.create.1.1 -> call_.ServerC.ServerR.ok.1.1 -> [int_choice] -> call_.ServerW.ServerR.refund.0.0 -> call_.ServerR.ServerO.refund.0.0 ->
call_.ServerR.ServerC.close.0.0>
図9: PATツールから出力された反例
• デッドロック時，ServerC[0] オブジェクトは
closed状態にあり，ref unding メッセージを受 け付けない．
こ の こ と か ら ，1 枚 目 の シ ー ケ ン ス 図 に お い て
ServerW と ServerC との相互作用に不具合があ る可能性が高いことがわかる．ServerC[0]がclosed
状態に遷移したのはServerRからServerCにclose
メッセージが送信されたためであり，それはServerW
から ServerRへの ref und メッセージがトリガと なっていることがシーケンス図から読み取れる．これ により，ServerW からServerRへのref undメッ セージとServerW からServerC への ref unding
メッセージには依存関係があり，メッセージの送信順 序を修正する必要があることがわかる．このように， イベントトレースの情報だけではなく，各イベントと 対応するシーケンス図のメッセージおよびそれぞれの オブジェクトの状態と送受信可能なメッセージの一覧 が表示されることで，どのオブジェクトが意図しない 状態になっているのか，なぜそのオブジェクトがその 状態へ遷移したのかを効率的に調査できることを確 認できる． このケーススタディにおける詳細化の検証は，CSP の詳細化関係ではなく，2つのモデルの等価関係に よって検証した．これは，今回検証対象としたシーケ ンス図の詳細化ではバックエンドのオブジェクトの数 は増加したが非決定性の情報が変化しなかったからで ある．今後この設計がステートマシン図やプログラミ ング言語のソースコードとして詳細化されていく過 程では，シーケンス図において非決定的であった選択 が決定的な選択に置き換えられていくことが想定で きる．そのようなモデルが与えられれば，CSPの詳 細化関係を検証することで，詳細化の妥当性が確認で きる．
5 関連研究
UMLやシナリオベースのモデルの検証に関しては すでにいくつかの研究が存在する． I. Abdelhalim らは UMLのステートマシン図と fUMLのアクティビティ図を対象としてCSPを用い て整合性を検証する手法を提案している [1]．ステー トマシン図やアクティビティ図ではシステムのふるま いが状態ベースのモデルとして記述されるため，対象 となる設計が十分に詳細に記述されていれば，その 図の整合性を検証したり動作可能なプログラムを自 動生成したりすることが可能となる．我々の手法は， シナリオベースの設計を合成することでそのような 状態ベースのモデルを得ることを目的としている． L. DanらはUMLのシーケンス図をCSPに変換 する手法を提案している [3]．この手法では，UML 2 で導入された結合フラグメントを用い，「alt」「loop」 「break」「opt」といった演算子をCSPに変換する． 我々の手法は，複数のシナリオを合成して状態ベース のモデルを得ることを目的としていることがこの手 法とは異なる．結合フラグメントを用いたシーケンス 図が複数枚ある場合，彼らの手法を用いて個々のシー ケンス図をCSPに変換し，我々の手法を用いてそれ らを合成してシステム全体のふるまいを得ることが 可能であると考えられる． E. M¨akinenらは「MAS」という名前のツールを 提案している [10]．この手法では，メッセージ送信を 状態に，メッセージ受信を状態間の遷移に対応させる ことでシーケンス図から状態ベースのモデルを得る． この手法では状態不変式などの情報を付加すること なく状態ベースのモデルを生成できる点が優れている．しかし，この手法では常に決定的なモデルが生成 されるため，非決定的にいずれかのメッセージが選択 されるようなモデルを記述できない．シーケンス図は 開発の初期段階で用いられる図であるため，シーケン ス図の範囲では記述されない要因による非決定性は 重要である．我々の手法ではメッセージ送信に非決定 性を持たせることで，この問題を解決している． シーケンス図に付加的な情報を加えることで検証 を可能とする手法としては，「Live Sequence Chart」 や「HMSC」という図を用いる手法がある．Live Se-quence Chart を用いる手法はD. Harel らによって 提案されている [5]. Live Sequence Chartはシーケ
ンス図を拡張した図であり，特定の条件でトリガされ るシナリオを記述できる．明示的にシーケンス図の開 始条件を記述することで，各シナリオの意味が明確化 され，状態ベースのモデルへの変換が可能となる．R. KumarらはLive Sequence Chartをオートマトンに 変換することでコミュニケーション・プロトコルを自 動的に検証する手法を提案している [9]．HMSCを用 いる手法はR. Alur らによって提案されている [2]． HMSCはシーケンス図間の実行順序を示す図である．
LTSA モデル検査器のプラグインである Message Sequence Chart plugin (LTSA-MSC)はHMSCを 用いてシーケンス図を検証する [15]．我々の手法で は，シーケンス図間の関係を記述するために新たな 記法を追加するのではなく，UMLの標準で定義され た状態不変式を利用している．これにより，標準的な シーケンス図に大きく手を加えることなく，検証が可 能となる．
6 まとめ
本論文では，同一クラスに複数のインスタンスが存 在でき，オブジェクトをシナリオ中で動的に生成・破 棄できるようなシーケンス図を検証する手法を提案 した．また，その提案手法を実際にSDVerifierツー ルとして実装し，ケーススタディにより有効性を確認 したことを報告した．このツールはシーケンス図を CSPに変換することで，モデル検査器PATで検証 可能とする．さらに，PATの出力する反例をシーケ ンス図上に逆変換することで効率的に反例を解析で きる機能を実現した．実際のシステムに対してケース スタディを行い，複雑なシステムの設計において提案 手法およびツールが有用であることを確認できた． 今後の課題としては，現状ではシーケンス図を検 証可能とするために自明なシナリオも含めて網羅的 にシーケンス図を記述しなければならないため，こ れを軽減するような改善が必要であると考えている． 具体的には，以下のような改善が考えられる． • 異常系のシナリオはテンプレートから自動生成 可能とする． • オブジェクトのおおまかな状態遷移設計などを 別途与えることで，状態不変式の記述を省略可能 とする． 参 考 文 献[ 1 ] Abdelhalim, I., Schneider, S. and Treharne, H.: Towards a practical approach to check UML/fUML models consistency using CSP, in
Pro-ceeding ICFEM’11 ProPro-ceedings of the 13th interna-tional conference on Formal methods and software engineering, 2011, pp. 33–48.
[ 2 ] Alur, R. and Yannakakis, M.: Model Checking of Message Sequence Charts, in Proceedings of the 10th
International Conference on Concurrency Theory,
1999.
[ 3 ] Dan, L. and Danning, L.: An Approach to For-malize UML Sequence Diagrams in CSP, in 3rd
In-ternational Conference on Computer and Electrical Engineering, 2010.
[ 4 ] Formal Systems: FDR2, 2010, http://www.fsel. com/software.html.
[ 5 ] Harel, D. and Kugler, H.: Synthesizing state-based object systems from LSC specifications, in
International Journal of Foundations of Computer Science, 2002.
[ 6 ] Hoare, C. A. R.: Communicating Sequential Processes, Prentice Hall, 1985.
[ 7 ] Kaizu, T., Isobe, Y. and Suzuki, M.: Refine-ment and Verification of Sequence Diagrams Us-ing the Process Algebra CSP, IEICE Transactions
on Fundamentals of Electronics, Communications and Computer Sciences, Vol. E96-A, No. 2 (2013),
pp. 495–504.
[ 8 ] Kaizu, T., Isobe, Y. and Suzuki, M.: Ver-ifying sequence diagrams using the process al-gebra CSP, in AVOCS 2013 Automated
Verifi-cation of Critical Systems Pre-proceedings, 2013,
pp. 203–206. http://dr.asukaze.net/pub/avocs proc kaizu 20130913.pdf.
[ 9 ] Kumar, R. and Mercer, E. G.: Verifying Com-munication Protocols Using Live Sequence Chart
252
Specifications, in Proceedings of the 8th
Interna-tional Workshop on Automated Verification of Crit-ical Systems, 2008.
[10] M¨akinen, E. and Syst¨a, T.: MAS — an inter-active synthesizer to support behavioral modelling in UML, in Proceedings of the 23rd International
Conference on Software Engineering, 2001.
[11] Object Management Group: UML 2.4.1, 2011, http://www.omg.org/spec/UML/2.4.1/.
[12] Object Management Group: XMI 2.4.1, 2013, http://www.omg.org/spec/XMI/2.4.1/.
[13] Roscoe, A. W.: The Theory and Practice of Concurrency, Prentice Hall, 1998.
[14] Sun, J., Liu, Y. and Dong, J. S.: Model check-ing CSP revisited: Introduccheck-ing a process analysis toolkit, Leveraging Applications of Formal
Meth-ods, Verification and Validation, Springer, 2009,
pp. 307–322.
[15] Uchitel, S., Chatley, R., Kramer, J. and Magee, J.: LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios, in
Proceed-ings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2003. 海 津 智 宏 2006年東京工業大学大学院情報理工 学研究科卒．2014年北陸先端科学技 術大学院大学情報科学研究科博士課 程修了．2006年日本電気株式会社入 社．2010年グーグル株式会社入社．ソフトウェアエ ンジニアとして同社サービスのシステム開発に従事． 磯 部 祥 尚 1992年芝浦工業大学大学院電気工学 専攻修士課程修了．同年電子技術総 合研究所(2001年に産業技術総合研 究所に改組)入所．現在，セキュアシ ステム研究部門高信頼ソフトウェア研究グループ長． 2001年工学博士(静岡大学)．2003年4月∼2004年 3月ウェールズ大学スウォンジー校訪問研究員．2012 年11月∼北陸先端科学技術大学院大学客員准教授 (兼務)．並行計算理論，特にCSPの研究と産業応用 に従事．情報処理学会，日本ソフトウェア科学会，電 子情報通信学会各会員． 鈴 木 正 人 1992年東京工業大学理工学研究科博 士後期課程修了．博士(工学)．同年 北陸先端科学技術大学院大学情報科 学研究科助手，1998年東京工業大学 大学院理工学研究科助教授，2002年より2年間国立 情報学研究所ソフトウェア研究系助教授(兼務)．2004 年北陸先端科学技術大学院大学情報科学研究科助教 授，現准教授．ソフトウェア開発方法論/開発支援ツー ル，UML，ソフトウェアアーキテクチャ，組込みシ ステム等の研究開発に従事．情報処理学会，日本ソフ トウェア科学会，電子情報通信学会各会員．
