日本ソフトウェア科学会第 31 回大会 (2014 年度) 講演論文集

シーケンス図を用いたモデル検査支援ツール
後藤 隼弐

吉岡 信和

モデル検査を実際の業務に適用する場合，モデル検査の知識や経験を有した人材の不足やモデル検査未習熟者のための学習コストの発生が問題となる．そこで，著者は従来の設計ツールであるシーケンス図を用いてモデル検査を可能とするモデル検査支援ツールを開発した．開発したツールでは，シーケンス図で記載した内部仕様と外部仕様を，検査モデルと検査仕様にそれぞれ変換することでモデル検査ツールへの入力を可能とする．また，モデル検査ツールが出力する反例情報をシーケンス図に変換することで，設計者はモデル検査を意識することなくモデル検査の恩恵を受けることができる．提案ツールの評価として，業務モデルに提案ツールを適用し，業務で実際に検出した再現性の低い不具合が学習コストを抑えながら効果的に検出できることを確認した．

In case of applying a model checking method to a business, a learning cost and a stable securement of humanresources are problems. So author developed a model checking support tool that enables model checking
method using a sequence diagram widely used as a design tool. In the tool, internal specifications andexternal specifications written by sequence diagrams are translated into inspection models and inspection
specifications, and a counterexample as a result of verification by a model checking tool is translated into asequence diagram. As a result, a designer can take benefits of a model checking method without learning
it. As a evaluation of the tool, author confirmed that a low reproducibility defect is detected eﬀectively asa result of applying the method to a business model.

を人手によるレビューで確認するのは容易ではなく，

1 はじめにまた，状態数に比例してレビューに要する工数が増大

著者は，デバイス制御ミドルウェアの開発業務経験するため，設計工程で検出するコストメリットが少なより，再現性の低い不具合を早期かつ効果的に検出す

くなってしまうことがある．実際に，手戻りリスクをることが困難であることを問題として認識している．

覚悟して早めに動作検証を実施するほうが全体的な再現性の低い不具合は，負荷耐久試験といったシステ

コストを低減できる場合がある．

ム試験工程など，数多く試行することで初めて不具合

人手によるレビューで確認するのではなく，システが顕在化することが多く，開発工程の最下流で検出さムがとりうるすべての状態に対して期待する性質が満れることで改修の手戻りが大きくなり，コスト増やスたされるかどうかを自動的に検証する技術として，モケジュール遅延の原因となることが多い．

デル検査手法がある．しかし，モデル検査を実際の業

再現性の低い不具合を設計工程で検出するために，務に適用する場合，モデル検査の知識や経験を有した

状態遷移表を作成して考慮に漏れがないか確認するこ

人材が不足していることや，モデル検査未習熟者へのとが一般的に行われる．しかし，状態遷移表の妥当性

学習コストが発生することが問題となる．たとえば，

A model checking support tool using a sequence
diagramJunji Goto, フェリカネットワークス株式会社, FeliCa
Networks, inc..
Nobukazu Yoshioka, 国立情報学研究所, National Institute of Informatics.

モデル検査を実施するためにはモデル検査ツールへの入力となる検査モデルや検査仕様を記述する必要があるが，検査モデルを記述するためにはモデル検査
ツール毎に定義されたモデル記述言語を習得する必要があり，検査仕様を記述するためには命題論理や述語論理，時相論理，集合論，オートマトンといった知識

2. 1 目標を習得する必要がある．また，モデル検査ツールが出

著者は，提案ツールの実現により達成するべき目標

力する反例情報は，シーケンス図などの設計ツールととして，著者が業務で実際に検出した再現性の低い不して一般的に利用される形式で出力されるわけでは具合が，学習コストをかけずに検出できることを設定ないため，解釈するのが容易ではなく，複雑な反例情した．当該不具合は発生確率が低く，開発の最終工程

報を解釈するためにはある程度の経験が必要となる．

として実施する連続運転による負荷耐久試験により

ここで，モデル検査を業務に適用する場合の問題を検出された．リリース直前の工程で検出されたため，解決するための課題として，次の 3 つを設定する．

影響が大きい根本的な改修は実施することが出来ず，

課題 1 検査モデル記述能力習得コストの低減

設計としては筋の良くない改修をするしか選択肢が課題 2 検査仕様記述能力習得コストの低減なかった．もし設計工程にてモデル検査を用いて当該

課題 3 反例情報解析能力習得コストの低減

不具合を検出することができていれば，より望ましい

著者は，これらの課題の解決により，学習コストを根本的な改修が可能であったと考えられる．

抑えながらモデル検査の適用を可能とすることを目

当該不具合を検出したソフトウェアはデバイス制的としたモデル検査支援ツール (以降，“提案ツール”

御ミドルウェアである．デバイス制御ミドルウェアと表現する) を開発した．提案ツールは，設計者がモの構成を図 1 に示す． デバイス制御ミドルウェアは，

デル検査ツールの入出力データを直接記述，解析しな

アプリケーション向けの API とデバイス制御デーモ

くてもモデル検査を実施できるようにすることで学ンで構成される．API はライブラリとして提供され，習コストの低減を実現している．提案ツールはオープ

アプリケーションにリンクされる．API とデーモン

ンソースソフトウェアとして公開している [13]．

はプロセス間通信を行い連携して動作する．API は開発にあたり，著者は，まず要求を分析し提案ツー

アプリケーションからデバイスの操作要求を受け取ルの実現により達成するべき目標を定め，提案ツール

り，デーモンに伝達する．デーモンは API からの要に求められる機能を整理した．要求分析については 2求を受信すると，実際にデバイスを制御してその結果章にて述べる．つづいて，実際の開発は，機能毎に要を API に通知する．

件を整理し，要件毎に設計方針を定め実装を行った．

デバイス制御ミドルウェアで検出した不具合は，デ要件と設計方針については 3 章にて述べる．実装にバイス制御の処理中断機能の外部仕様違反である．処

ついては 4 章にて述べる．提案ツールの評価として

理中断機能の期待動作となるシーケンス図を図 2 に，は，業務で実際に開発したソフトウェアに提案ツール

不具合発生時のシーケンス図を図 3 に示す．

を適用することで効果を確認した，また提案ツールを処理中断機能は，デーモンがデバイス制御の処理完適用しなかった場合との比較を行い，目標の達成度を了を待っている間にアプリケーションからデバイスク確認した．評価については 5 章にて述べる．最後に，ローズ要求を受信した際に処理完了待ちを中断する

6 章でまとめと課題，今後の展望について述べる．
!"#$%
!"#&%
+,-.'(6789:!%

2 要求分析
本章では，要求分析として提案ツールの実現により達成するべき目標を明確にし，目標を達成するために

$;<%

$;<%

<;@

<;@

5%

+,-.'(+=>?%/01234

必要な提案ツールに要求される機能がなにかを明確'()*+,-.%

にする．

図1

デバイス制御ミドルウェアの構成

!GH!
!""!

H"'96&$.2!

#)$L@.!

9)66I)'JKD($)*!

H"'>$(%$(!

34$'12@(!

96@-$(!

#$%&'$!

($)*+,!
-$.*/$01$-2+/3!#,!
$4$'12$+/3!#,!
5(&2$+/$)*,!

($)*+,!

'6@-$+,!
-$296@-$C6)E+,!

<=>?!

B6)E8F82(1$($)*+,!
<=>?!

-$.*/$01$-2+9;A>3,!
$4$'12$+9;A>3,!

を がなのでコールバックに通知しない8').'$6+,!

B6)E 2(1$H"'96&$.2-$.*/$-162+/3!#789!:93;3#,!

5(&2$+/$-$2,!
"@5$(ABB+,!

-$.*/$-162+9;A>378>=993>>,!
B6)E8F8B)6-$@./$'%+9;A>378>=993>>,!
@.96@-$C&.&-D+>=993>>,!

図2

処理中断機能の期待動作シーケンス図機能である．アプリケーションが API を実行するとしないタイミングで偽に設定されてしまうことでア

デバイス制御をデーモンに要求し，その結果はコール

プリケーションへのコールバック通知の抑制に失敗しバックにより通知されるが，アプリケーションがコーてしまうことで発生していた．つまり，内部仕様と外ルバックの通知を待つ間にデバイスクローズ API を部仕様との間に整合性がなかったことが不具合の原因

実行すると，通知待ち対象のコールバックの通知がである．

キャンセルされるというのがデバイス制御ミドルウェ
アの外部仕様になっている．内部仕様としては，キャ2. 2 要求される機能

ンセル対象のコールバックがデーモンから API に通2. 1 節にて，提案ツールの実現により達成するべき知された後，API 内のコールバック通知抑制フラグ

目標として，業務で検出した不具合が学習コストをかによりアプリケーションに通知するか否かを制御する

けずに検出できることを設定した．また，業務で検出仕組みとしていた．フラグは，デバイスクローズ要求

した不具合が，内部仕様と外部仕様の不整合に起因すの実行時に真に設定され，デバイスクローズ要求のることを説明した．

コールバックが通知された時に偽に設定されるように内部仕様と外部仕様の不整合は，モデル検査を用い実装していた．コールバックはフラグが偽のときのみて内部仕様と外部仕様の詳細化関係，つまり内部仕様

アプリケーションに通知される．

が外部仕様を満たしているかを検査することで検出

しかし，検出した不具合では，キャンセルされるべ

することができる．学習コストをかけずにモデル検査

きコールバックが通知されてしまうという外部仕様を実施するためのアプローチとして，ソフトウェア設

違反を起こしていた．不具合は，キャンセル対象とな計者がモデル検査ツールの入出力を直接扱わないよるコールバックよりも先に，デバイスクローズ要求のうにする方針を採用した．この方針に従い，提案ツー

コールバックが通知されることにより，フラグが意図

ルに要求される機能として，次の 3 つを設定した．

!GH!
!""!

H"'<:&$.2!

#)$I;.!

<)::J)'KLC($)*!

H"'8$(%$(!

34$'12;(!

<:;-$(!

#$%&'$!

($)*+,!
-$.*/$01$-2+/3!#,!
$4$'12$+/3!#,!
5(&2$+/$)*,!

($)*+,!

':;-$+,!

6789!

-$2<:;-$B:)D+,!
A:)D@E@2(1$($)*+,!
6789!

-$.*/$01$-2+<=>83,!
$4$'12$+<=>83,!
').'$:+,!

5(&2$+/$-$2,!
";5$(>AA+,!

-$.*/$-1:2+<=>83?@87<<388,!
A:)D@E@A):-$;./$'%+<=>83?@87<<388,!
;.<:;-$B&.&-C+87<<388,!

-$.*/$-1:2+/3!#?@<!F<3=3#,!
;./$'%+/3!#?@<!F<3=3#,!
;./$)*B&.&-C+<!F<3=3#,!

外部仕様違反！!
図3を がなのでコールバックに通知してしまう@

A:)D A):-$
H"'<:&$.2のが遅れる場合がある@/3!# -$.*/$-1:2

処理中断機能の不具合発生時のシーケンス図

機能 1が出力する反例情報をシーケンス図へ変換する機能

シーケンス図で表現された内部仕様を検査モデ(機能 3) を提供する．つまり，提案ツールは，モデル

ルに変換する機能検査ツールの入出力を，設計者にとって馴染みのある

機能 2

シーケンス図に置き換える機能を提供する．提案ツーシーケンス図で表現された外部仕様を検査仕様

ルはモデル検査を実施する機能は提供しないため，外に変換する機能部のモデル検査ツールを用いてモデル検査を実施す

機能 3
反例情報をシーケンス図に変換し期待動作と異常動作の差分を表示する機能

る．図 4 に提案ツールを利用した場合のモデル検査実施の流れを示す．
機能 3 では，単に反例情報をシーケンス図に変換

これらの機能は，1 章で設定したモデル検査を業務にするだけでなく，期待動作と異常動作のシーケンス図

適用する場合の 3 つの課題に対応している．

を両方表示し差分を明示することで，異常動作に至る提案ツールは，オブジェクト指向モデリング [8] で経緯を容易に推測できることが要求される．これは，モデル化されたシステムを対象とし，UML(Unified

検査対象のシステムが複雑である場合を考慮すると，

Modelling Language) [4] [5] シーケンス図 (以降，単反例情報として単に異常動作のシーケンス図を表示に “シーケンス図” と表現する) を，モデル検査ツーしたとしても，異常の原因および異常に至る内部動作

ルに入力するための検査モデルや検査仕様へ変換すの分析自体が困難であると考えたためである．

る機能 (機能 1，機能 2)，および，モデル検査ツール

提案ツールを利用することで，設計者は，シーケン

,-./+#$%)*+)*+#$%)++)++

6789+!"#$%&'()*+#$%),+
),+

#$%*+

)*G+

)*+

EFCD#+

)++
),+

=>?@+

0"1234+

CD#EF+
!"#+

5-./+

67:;+

)*<+

#$%*+
)*+

)++
),+

#$%#&'(+
!"#+

)*H+

EF./+

AB?@+
0"1234+0"1234+

図4

提案ツールを利用した場合のモデル検査

ス図を用いてシステムの仕様を記述するだけでモデ3. 1. 1 モデル検査ツールの選定

ル検査ツールへの入力を準備することができ，検査モ

バックエンドで動作させるモデル検査ツールとしデルや検査仕様を記述するための学習コストを必要ては，プロセス代数 CSP(Communicating Sequen-としない．また，モデル検査ツールが出力する反例情tial Processes) [3] [7] に基づくモデル検査ツールで報も提案ツールによりシーケンス図へ変換され表示ある FDR3(Failures/Divergence Refinement 3) [11]されるため，モデル検査ツール毎の反例情報形式の[12] を採用した．FDR3 を採用した理由は，次の 3 点

学習や慣れるための経験を積む必要がなく，さらに，である．

期待動作と異常動作の差分が明示されるため容易に反例情報を解釈することができる．

• FDR3 は CSP でモデル化された 2 つのプロセス間の等価関係や詳細化関係を検証することに適しており，内部仕様と外部仕様の整合性検査に3 設計適しているため本章では，提案ツールの設計について述べる．はじ• FDR3 では検査モデルと検査仕様の記述に同じ

めに，提案ツールが対象とするモデル検査ツールにつ言語である CSPM [10] を用いるため，シーケンいて述べ，つぎに，2. 2 節で述べた提案ツールに要求

ス図から検査モデル，検査仕様への変換に同じ仕される機能毎に要件を整理し，要件毎に設計方針を述

組みを適用できるため

べる．

• FDR3 は 反 例 情 報 を ，JSON(JavaScript Object Notation) 形式 [2] や YAML(YAML Ain’t

3. 1 モデル検査ツール

Markup Language) 形式 [1] といった，機械処理

提案ツールは，シーケンス図を検査モデルおよび検が容易な形式で出力することができ，シーケンス

査仕様へ変換し，反例情報をシーケンス図に変換する

図への変換が容易であるため機能を提供するが，シーケンス図の変換先である検査

FDR3 への入力は内部仕様と外部仕様のシーケン

モデルおよび検査仕様は，対象とするモデル検査ツー

ス図から変換した CSPM 形式のファイルである．まル毎に異なる．シーケンス図への変換元となる反例情

た，シーケンス図への変換元となる FDR3 が出力す報についても同様である．本節では，対象とするモデ

る反例情報の形式は YAML 形式とした．

ル検査ツールの選定と，選定したモデル検査ツールを

3. 1. 2 内部仕様と外部仕様の整合性検査

用いて内部仕様と外部仕様の整合性を検査する方法

内部仕様と外部仕様の整合性の検査は FDR3 を用について述べる．

いて次のような手順で実施する．

1. 検査対象のシステムを構成する各オブジェクト

毎に，内部仕様として，オブジェクトが受理可能なメッセージと，他オブジェクトとのメッセージ
交換による相互作用の関係を CSPM を用いてモデル化する．

2. 各オブジェクトの内部仕様を表す複数のモデル
を，オブジェクト間のメッセージ交換による相互作用が同期するように並行合成し，合成内部仕様を表すひとつのモデルを生成する．

シーケンス図をセマンティクスを維持したまま検査モデルに変換できること
要件 1-4
複数オブジェクトの内部仕様のシーケンス図を合成し，システムの検査モデルに変換できること

3. 2. 1 要件 1-1 設計方針
内部仕様を検査モデルの CSPM 形式に変換するために，入力となる内部仕様のシーケンス図が CSPM

3. システムの外部仕様として，システム外部のオ

形式への変換に適した，機械処理できる形式になってブジェクトとシステムの相互作用の関係を CSPM

いることが求められる．そのためには，シーケンス図を用いてモデル化する．モデル化された外部仕様

から機械処理できる形式へ変換できること，あるいの CSPM が検査仕様となる．ここで，モデル化

は，機械処理できる形式からシーケンス図へ変換できされた検査仕様を Spec とする．

ることのどちらかが求められる．

4. 合成内部仕様を表すモデルに対し，外部仕様の要件 1-1 に対する設計方針としては，機械処理でモデルと合成することで，システム外部との相互きる形式からシーケンス図へ変換する方式を採用し作用が適用されたシステムの検査モデルが得らた．つまり，シーケンス図から直接 CSPM 形式へれる．

変換するのではなく，シーケンス情報が表現できる

5. 検査モデルを検査仕様で検査できるようにする

DSL(Domain-Specific-Language)(以降，sd-DSL とために，検査モデルからシステム外部に公開され表現する) から CSPM 形式に変換することで内部仕ていない内部メッセージを隠蔽することで，検査様の検査モデルを作成し，sd-DSL からシーケンス図

モデルが扱うメッセージ集合を検査仕様と同等にを描画できる提案ツールを用いてシーケンス図を作する．ここで，内部メッセージが隠蔽された検査

図する．

モデルを System とする．

この方式を採用した理由は，後述する反例情報から

6. System が Spec の失敗詳細化 (Spec ⊑F Sys-

シーケンス図へ変換 (機能 3) する際に，YAML 形式

tem) であることを，FDR3 を用いて検査する．

の反例情報からシーケンス図を描画する必要があることを考慮すると，内部仕様と反例情報が同じシーケ

3. 2 内部仕様シーケンス図から検査モデルへの変
換 (機能 1)ンス図の作図ツールで描画されたほうが，表現が統一される点で望ましいと考えたためである．

本節では，2. 2 節で提案ツールに要求される機能のこの設計方針に従って，sd-DSL からシーケンス図

ひとつとして設定した，内部仕様のシーケンス図からを作図できる提案ツールを調査し，最終的に Plan-

検査モデルへ変換する機能 (以降，“機能 1” と表現す

tUML [6] を採用した．PlantUML を採用した理由は，

る) について，要件毎に設計方針を述べる．

内部仕様を記述するために必要な，複合フラグメント

機能 1 に対する要件としては次の 4 つが挙げられる．

や注釈といったシーケンス図の構成要素を作図できる

要件 1-1ためである．内部仕様を記述するために必要なシーケ入力となるシーケンス図が機械処理できる形式

ンス図の構成要素については要件 1-2(3. 2. 2 小節) にになっていることて述べる．PlantUML の sd-DSL の例を図 5 に，図要件 1-2
メッセージの返り値や引数，状態変数による式が評価できる検査モデルに変換できること
要件 1-35 の sd-DSL を PlantUML でシーケンス図に変換した例を図 6 に示す．

シーケンス図は振る舞いを表現するのに特化した
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

@startuml
title IpcServer
control IpcClient
control IpcServer
control Executor
control Closer
hnote over IpcServer : Ready====hnote over IpcServer : Ready
IpcClient -> IpcServer ++ : sendRequest(apiName)alt apiName==CLOSE
IpcServer -> Closer ++ : execute(CLOSE)
returnelse
IpcServer -> Executor ++ : execute(apiName)
returnend
returnhnote over IpcServer : Ready@enduml図であり，メッセージの型情報を表現するには適していない．そのため，提案ツールでは，メッセージの引数や返り値の型情報を定義する定義情報ファイルを別途用意し，内部仕様を検査モデルに変換する際に，定義情報も検査モデルに埋め込む方針とした．
定義情報は YAML 形式で記述し提案ツールに入力する実装とした．表 1 に，定義情報と対応する CSPMの例を示す．定義情報の 1-3 行目は，ユーザ定義型として Result と Mode を，代数的データ型として定義している．これらは CSPM では datatype を用いる

図5

PlantUML の sd-DSL 例

定義に変換される．定義情報の 4 行目以降はクラス毎にメッセージの引数および返り値の型情報を定義している．定義情報で定義されたクラスは，CSPM
では Class_型の要素として定義される (CSPM 3 行目)．メッセージは CSPM では “クラス名_メッセー
ジ名. 引数の型”(応答メッセージの場合は “return_
クラス名_メッセージ名. 返り値の型”) という形式でMethod_型の要素として定義される (CSPM 4 行目以降)．5-8 行目は Daemon クラスのメッセージを定義しており，start メッセージは引数が無く，Result 型を返却することを表現している．11 行目は引数が複数ある場合の記述例であり，15 行目は返り値が無い
場合の記述例である．16 行目の cancel メッセージには返り値に関する記述が無いが，これは cancel メッ
セージが非同期メッセージであることを示している．
図6

図 5 の sd-DSL を PlantUML でシーケンス図に変換した例

3. 2. 3 要件 1-3 設計方針
sd-DSL を検査モデルの CSPM に変換する際，シーケンス図のセマンティクスを維持したまま CSPM に

3. 2. 2 要件 1-2 設計方針変換する必要がある．本小節では，提案ツールで採内部仕様を厳密に表現するためには，シーケンス図

用したシーケンス図と CSPM の対応関係について述上のメッセージの返り値や引数を用いた式を扱える必べる．

要がある．たとえば，メッセージの返り値を元に条件

シーケンス図におけるライフラインとメッセージ

分岐の条件式を指定したり，状態変数を用いた何らか

は，CSPM のプロセスとイベントに対応付ける．ラの演算結果をメッセージの引数に指定したりする場合

イフラインとメッセージの CSPM への変換例を表 2である．その場合，内部仕様のシーケンス図を検査モに示す．内部仕様のシーケンス図はオブジェクト毎

デルに変換する際に，検査モデルでは整数・論理・集に用意するが，表 2 はオブジェクト A に関する内部

合・列などの演算が扱える必要があり，そのためには仕様を表している．CSPM においてメッセージの送検査モデルにてメッセージを定義する際に返り値や引信は，プレフィックス演算子により，メッセージ送信

数の型情報が必要となる．

前のオブジェクトを表すプロセスが，メッセージ送表1

定義情報の CSPM への変換例

定義情報 (YAML)
1 Data:2
Result: [ SUCCESS, FAILED, CANCELED ]3
Mode: [ RW_MODE.Bool.Bool, CTRL_MODE ]4 Class:5
Daemon:6
start:
7
args: []
8
return: Result
9
Device:10
open:
11
args: [ Int, Mode ]12
return: Bool13
close:
14
args: []
15
return: null
16
cancel:17
args: [ Bool ]

CSPM
1
2
3
4
5
6
7

datatype Result = SUCCESS | FAILED | CANCELED
datatype Mode = RW_MODE.Bool.Bool | CTRL_MODE
datatype Class_ = Daemon | Device
datatype Method_ = Daemon_start | return_Daemon_start.Result |Device_open.Int.Mode | return_Device_open.Bool |Device_close | return_Device_close |Device_cancel.Bool

信を表すイベントの実行後に，メッセージ送信後のる状態注釈であり，これは状態注釈で表される状態へ

オブジェクトを表すプロセスとして振る舞うようにの遷移を表す．シーケンス図の開始直後は，初期状態定義される．たとえば，表 2 では，シーケンス図上(Init) であるとした．

のオブジェクト A から B への m1 メッセージの送信

また，状態は状態変数を持つことができ，状態変数

が，CSPM の 4 行目に対応しているが，ここでは，をメッセージの引数や複合フラグメントでの条件判定

CSPM の A_Init_0() がメッセージ送信前のオブジェに用いることができるとした．状態変数は，状態の開クト A を，msg_.A.B.B_m1!0 が m1 メッセージの送始を表す状態注釈で状態名の後に “変数名:型名” を信イベントを，A_Init_1() がメッセージ送信後の括弧内に記述することで定義する．変数は複数定義でオブジェクト A を表しており，プレフィックス演算

き，その際は変数名と型名の定義をカンマ (“,”) で区

子->により A_Init_0() が，m1 メッセージの送信後切り記述する．状態遷移の状態注釈では遷移先の状態に A_Init_1() のように振る舞うように定義されて名の後に括弧で遷移後の状態変数の値を指定できるいる．メッセージ送信後の復帰やメッセージの受信にとした．たとえば，表 3 のシーケンス図では，オブついても，メッセージ送信と同じようにイベントとプ

ジェクト A の状態 Ready が状態変数 v0(型：Int) をレフィックス演算子を用いて CSPM に変換する．メッ持ち，シーケンス図の最後で，状態 Ready に状態変セージ送信を表すイベントは，表 2 CSPM の 3 行目

数 v0 の値が v0+ret となるように遷移していることに示すとおり，送信元のオブジェクト，送信先のオブがわかる．

ジェクト，送信するメッセージの三つ組をパラメータに持つチャネル msg_として定義される．
内部仕様を作成する際，オブジェクトの状態毎に処理を記述することで作成が容易になることがある．

状態変数は，ライフライン上で四角形の注釈を用いることで値を更新できるとした．たとえば，表 3 のシーケンス図では，オブジェクト A の状態変数 v0 が

v0+1 に更新される例を示している．

シーケンス図において，オブジェクトの状態をライフ

CSPM において，状態は，プロセス名の一部としてライン上に六角形の注釈 (以降，“状態注釈” と表現す変換される．たとえば，オブジェクト A が状態 Readyる) を記述することで表現することにした．状態遷移であるプロセスは A_Ready_n として表される．n はと状態変数の CSPM への変換例を表 3 に示す．シー

当該状態での処理毎に採番される整数である．CSPM

ケンス図上の状態注釈は，使われる箇所によって 2 つにおいて，状態変数は，状態変数を管理するプロセの意味合いを持つとした．1 つ目は，二重線の直後にスと状態変数を操作するためのイベントを用いて表現れる状態注釈であり，これは状態注釈で表される状現される．表 3 CSPM では，3 行目でオブジェクト A

態の開始を表す．2 つ目は，二重線の直後以外に現れの状態変数 v0 をユーザ定義型 StateVar_の要素とし表2
シーケンス図ライフラインとメッセージの CSPM への変換例

sd-DSL
1
2
3
4
5
6
7

表3
シーケンス図

CSPM
1
2
3
4
5
6
7

@startuml
participant A
participant B
A -> B ++ : m1(0)return ret
A ->> B : m2(ret)@enduml

datatype Class_ = A | B
datatype Method_ = B_m1.Int | return_B_m1.Int | B_m2.Int
channel msg_ : Class_.Class_.Method_
A_Init_0() = msg_.A.B.B_m1!0 -> A_Init_1()
A_Init_1() = msg_.B.A.return_B_m1?ret -> A_Init_2(ret)
A_Init_2(ret) = msg_.A.B.B_m2!ret -> A_Init_3(ret)
A_Init_3(ret) = SKIP

状態遷移と状態変数の CSPM への変換例

sd-DSL
1
2
3
4
5
6
7
8
9
10
11

@startuml
participant A
participant B
hnote over A : Ready(0)====hnote over A : Ready(v0:Int)
A -> B ++ : m1(v0)return ret
note over A : v0 = v0+1
hnote over A : Ready(v0+ret)@enduml

CSPM
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

datatype Class_ = A | B
datatype Method_ = B_m1.Int | return_B_m1.Int
datatype StateVar_ = A_Ready_v0.Int
channel msg_ : Class_.Class_.Method_channel init_, sync_, update_ : StateVar_
SV_A_Ready_v0_Init = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)SV_A_Ready_v0(val) = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] update_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] sync_.A_Ready_v0!val -> SV_A_Ready_v0(val)
A_Init_0() = init_.A_Ready_v0!0 -> A_Ready_0()
A_Ready_0() = sync_.A_Ready_v0?v0 -> msg_.A.B.B_m1!v0-> A_Ready_1()
A_Ready_1() = msg_.B.A.return_B_m1!ret -> A_Ready_2(ret)A_Ready_2(ret) = update_.A_Ready_v0!(v0+1) -> A_Ready_3(ret)A_Ready_3(ret) = init_.A_Ready_v0!(v0+ret) -> A_Ready_0()て定義し，5 行目で状態変数の操作に用いるチャネル

オブジェクトにより決定される場合である．表 5 に

init_，sync_，update_を定義している．init_は初

ガード無しの alt と opt の CSPM への変換例を示す．

期化，sync_は値の参照，update_は値の更新を表し

表 5 のシーケンス図では，alt 複合フラグメントによている．また，6-7 行目では，オブジェクト A の状態

りオブジェクト B のメッセージ m1 か m2 がオブジェ

変数 v0 を管理するプロセス SV_A_Ready_v0 を定義

クト A により選択され送信されることを表現していしている．

る．変換後の CSPM では 4 行目にて外部選択を用いシーケンス図における複合フラグメントの alt とて表現されている．

opt は，ガードの有無によって CSPM での表現が異シーケンス図における複合フラグメントの loop は，なる．ガード有りの alt と opt では条件分岐を用い

CSPM では条件分岐と逐次合成を用いて表現する．表て表現する．表 4 に，複合フラグメント (ガード有り

6 に，複合フラグメント (loop) の CSPM への変換例

alt，ガード有り opt) の CSPM への変換例を示す．

を示す．ここで，逐次合成を用いる理由は，繰り返し

一方，ガード無しの alt と opt は CSPM では外部処理の終端で先頭に戻る処理を考慮する必要がなく選択を用いて表現する．ここで，内部選択を用いない

なり，変換処理を簡略化できると考えたためである．

理由は，本論文において内部仕様は実装工程への入力

たとえば，表 6 CSPM の 16 行目は，sd-DSL の 9 行となる詳細設計情報となることを想定しているため，目，つまり繰り返し処理の終端箇所を表しているが，非決定的な振る舞いを意図して alt や opt を利用する

単に成功終了しているだけであり，先頭に戻るためのことは無いと考えたためである．内部仕様でガード処理を必要としない．

無しの alt や opt を用いる必要があるのは，外部から

3. 2. 4 要件 1-4 設計方針のメッセージを受信する際に，メッセージの受信有無

3. 1. 2 小節で説明したとおり，内部仕様と外部仕様

や，受信するメッセージの種類などがメッセージ送信の整合性を検査するためには，オブジェクト毎に定表4複合フラグメント (ガード有り alt，ガード有り opt) の CSPM への変換例

シーケンス図sd-DSL
1
2
3
4
5
6
7
8
9
10
11
12
13
14

表5

@startuml
participant A====
hnote over A : Ready(v0:Int)
alt v0 >= 10
note over A : v0 = v0+10
else
note over A : v0 = v0+1
end
opt v0 > 100
note over A : v0 = 0
end
hnote over A : Ready(v0)@enduml

CSPM
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

datatype Class_ = A
datatype StateVar_ = A_Ready_v0.Int
channel init_, sync_, update_ : StateVar_
SV_A_Ready_v0_Init = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)SV_A_Ready_v0(val) = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] update_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] sync_.A_Ready_v0!val -> SV_A_Ready_v0(val)
A_Ready_0() = sync_.A_Ready_v0?v0 -> if v0 >= 10
then A_Ready_1()
else A_Ready_3()
A_Ready_1() = update_.A_Ready_v0!(v0+10) -> A_Ready_2()
A_Ready_2() = A_Ready_5()
A_Ready_3() = update_.A_Ready_v0!(v0+1) -> A_Ready_4()
A_Ready_4() = A_Ready_5()
A_Ready_5() = sync_.A_Ready_v0?v0 -> if v0 > 100
then A_Ready_6()
else A_Ready_8()
A_Ready_6() = update_.A_Ready_v0!(0) -> A_Ready_7()
A_Ready_7() = A_Ready_8()
A_Ready_8() = init_.A_Ready_v0!(v0) -> A_Ready_0()

複合フラグメント (ガード無し alt，ガード無し opt) の CSPM への変換例

シーケンス図sd-DSL
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

@startuml
participant A
participant B====
hnote over B : Readyalt
A ->> B : m1(v0)else
A ->> B : m2(v0)endopt
A ->> B : m1(v0)endhnote over B : Ready@enduml

CSPM
1
2
3
4
5
6
7
8
9
10
11
12

datatype Class_ = A | B
datatype Method_ = B_m1.Int | B_m2.Int
channel msg_ : Class_.Class_.Method_
B_Ready_0() = B_Ready_1() [] B_Ready_3()
B_Ready_1() = msg_.A.B.B_m1?v0 -> B_Ready_2()
B_Ready_2() = B_Ready_5()
B_Ready_3() = msg_.A.B.B_m2?v0 -> B_Ready_4()
B_Ready_4() = B_Ready_5()
B_Ready_5() = B_Ready_6() [] B_Ready_8()
B_Ready_6() = msg_.A.B.B_m1?v0 -> B_Ready_7()
B_Ready_7() = B_Ready_8()
B_Ready_8() = B_Ready_0()

義した内部仕様を，システム全体の内部仕様として 1

にて，複製型アルファベット付並行合成演算子を用

つの検査モデル CSPM に合成する必要がある．提案

いてオブジェクト A とオブジェクト B を合成していツールでは，内部仕様をオブジェクト毎に CSPM にる．複製型アルファベット付並行合成演算子に与え変換した後，複製型アルファベット付並行合成演算子

るプロセスとイベントは，22-27 行目で定義した関数を用いて，オブジェクトのプロセス同士をメッセー(getProcIf_() および getProc_()) により得る．こジの送受信が同期するように並行合成することでシ

れらの関数は，クラス (Class_の要素) を引数により，ステム全体の検査モデルを生成する方針とした．内当該クラスに対応するプロセスやメッセージ送受信イ

部仕様合成の CSPM への変換例を表 8 に示す．表 8

ベント集合を返す．

は，システムを構成するオブジェクトであるオブジェ
クト A とオブジェクト B の内部仕様シーケンス図を合成する例を示している．シーケンス図中の U はシ

3. 3 外部仕様シーケンス図から検査仕様への変換(機能 2)

ステム外部のアクターであり，内部仕様としては定

本節では，機能 2 である，外部仕様のシーケンス

義しない．内部仕様の sd-DSL は，オブジェクト毎に図から検査仕様への変換について，要件と要件に対す@startuml と@enduml で囲み title で定義するオブる設計方針について述べる．

ジェクト名を記述する．変換先の CSPM の 25 行目

機能 2 に対する要件は，シーケンス図から CSPM

表6
シーケンス図複合フラグメント (loop) の CSPM への変換例

sd-DSL
1
2
3
4
5
6
7
8
9
10
11

@startuml
participant A
participant B====
hnote over A : Ready(v0:Int)loop v0 < 10
A ->> B : m1(v0)note over A : v0 = v0+1
end
hnote over A : Ready(0)@enduml

表7
シーケンス図

CSPM
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

datatype Class_ = A | B
datatype StateVar_ = A_Ready_v0.Int
datatype Method_ = B_m1.Int
channel msg_ : Class_.Class_.Method_channel init_, sync_, update_ : StateVar_
SV_A_Ready_v0_Init = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)SV_A_Ready_v0(val) = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] update_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] sync_.A_Ready_v0!val -> SV_A_Ready_v0(val)
A_Ready_0() = sync_.A_Ready_v0?v0 -> if v0 < 10then A_Ready_1(); A_Ready_0()
else A_Ready_4()
A_Ready_1() = sync_.A_Ready_v0?v0 -> msg_.A.B.B_m1!v0-> A_Ready_2()
A_Ready_2() = update_.A_Ready_v0!(v0+1) -> A_Ready_3()
A_Ready_3() = SKIP
A_Ready_4() = init_.A_Ready_v0!(v0) -> A_Ready_0()

複合フラグメント (par) の CSPM への変換例

sd-DSL
1
2
3
4
5
6
7
8
9
10
11
12

@startuml
participant A
participant B====
hnote over A : Ready(v0:Int)
parA ->> B : m1(v0)else
A ->> B : m2(v0)endhnote over A : Ready(0)@enduml

CSPM
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

datatype Class_ = A | B
datatype StateVar_ = A_Ready_v0.Int
datatype Method_ = B_m1.Int | B_m2.Int
channel msg_ : Class_.Class_.Method_channel init_, sync_, update_ : StateVar_
SV_A_Ready_v0_Init = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)SV_A_Ready_v0(val) = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] update_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] sync_.A_Ready_v0!val -> SV_A_Ready_v0(val)
A_Ready_0() = (A_Ready_1() ||| A_Ready_3()); A_Ready_5()
A_Ready_1() = sync_.A_Ready_v0?v0 -> msg_.A.B.B_m1!v0-> A_Ready_2()
A_Ready_2() = SKIP
A_Ready_3() = sync_.A_Ready_v0?v0 -> msg_.A.B.B_m2!v0-> A_Ready_4()
A_Ready_4() = SKIP
A_Ready_5() = init_.A_Ready_v0!(v0) -> A_Ready_0()

へ変換する点において，機能 1 と基本的には同等できないため，システム外部とシステムとの相互作用をある．具体的には，要件 1-1，1-2，1-3 と同等の要件

外部視点で表現する外部仕様としては，上記のようなが機能 2 に対しても存在する．ここでは，機能 2 にケースに対しては非決定的な振る舞いとして定義す

対する要件 1-1，1-2，1-3 と同等の要件をそれぞれ要るのが適当であると考えたためである．

件 2-1，2-2，2-3 とする．
基本的に要件 2-1，2-2，2-3 に対する設計方針は要

3. 4 反例情報からシーケンス図への変換 (機能 3)

件 1-1，1-2，1-3 に対する設計方針と同等であるが，本節では，機能 3 である，反例情報からシーケン

要件 2-3 に対する設計方針において次のような違いがス図への変換について，要件と要件に対する設計方針

ある．

およびその実装について説明する．

• ガード無し alt，ガード無し opt を CSPM に変換する際に，外部選択 ([]) ではなく内部選択 (|~|)
を用いる• メッセージ受信時のイベントのフィールドタイ
プを決定的入力 (?) ではなく非決定的入力 ($) を用いる
これは，システム内部のイベントは外部からは観測で機能 3 に対する要件としては次の 3 つが挙げられる．
要件 3-1
反例情報 (YAML 形式) から sd-DSL 形式へ変換できること
要件 3-2
反例情報から異常動作だけでなく，期待動作のシーケンス図も表示できること

表8シーケンス図内部仕様合成の CSPM への変換例

sd-DSL
1
2
3
4
5
6
7
8
9
10
11
12
13

@startuml
title A
Actor Uparticipant A
participant B====
hnote over A : Ready(v0:Int)U -> A ++ : m1(a0)
A -> B ++ : m2(a0+v0)
return ret
return ret
hnote over A : Ready(ret)@enduml

1
2
3
4
5
6
7
8
9
10

@startuml
title Bparticipant A
participant B====
hnote over B : Ready
A -> B ++ : m2(arg)return arg+1
hnote over B : Ready@enduml

CSPM
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

要件 3-3
異常動作と期待動作の差異を明示できること

datatype Class_ = U | A | B
datatype Method_ = A_m1.Int | return_A_m1.Int| B_m2.Int | reutrn_B_m2.Int
datatype StateVar_ = A_Ready_v0.Int
channel msg_ : Class_.Class_.Method_channel init_, sync_, update_ : StateVar_
SV_A_Ready_v0_Init = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)SV_A_Ready_v0(val) = init_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] update_.A_Ready_v0?v -> SV_A_Ready_v0(v)[] sync_.A_Ready_v0!val -> SV_A_Ready_v0(val)
A_Ready_0() = msg_.U.A.A_m1?a0 -> A_Ready_1()
A_Ready_1() = sync_.A_Ready_v0?v0 -> msg_.A.B.B_m2!v0-> A_Ready_2()
A_Ready_2() = msg_.B.A.return_B_m2?ret -> A_Ready_3(ret)A_Ready_3(ret) = msg_.A.U.return_A_m1!ret -> A_Ready_4(ret)A_Ready_4(ret) = init_.A_Ready_v0!(ret) -> A_Ready_0()
B_Ready_0() = msg_.A.B.B_m2?arg -> B_Ready_1(arg)
B_Ready_1(arg) = msg_.B.A.return_B_m2!(arg+1) -> B_Ready_2(arg)
B_Ready_2(arg) = B_Ready_0()
getSv_(A) = Union({productions(A_Ready_v0)})
getSvCh_(x) = {init_.s, sync_.s, update_.s | s<-getSv_(x)}getProc_(A) = A_Ready_0() [|getSvCh_(A)|] SV_A_Ready_v0_Init\ getSvCh_(A)getProc_(B) = B_Ready_0()
getProcIf_(x) = Union({{msg_.x.t.m|t<-diff(Class_, x), m<-Method_},{msg_.f.x.m|f<-diff(Class_, x), m<-Method_}})InternalSystem_ = || x:Class_ @ [getProcIf_(x)] getProc_(x)えば反例情報の 6 行目は，オブジェクト A からオブジェクト B へメッセージ m1 を引数の値を 0 として送3. 4. 1 要件 3-1 設計方針

信するイベントであることがわかるため，それをその反例情報をシーケンス図に変換するために，反例情

まま sd-DSL での表現に変換すればよい．違反してい報を sd-DSL 形式に変換できる必要がある．提案ツーる箇所については複合フラグメント neg を用いて囲ルでは，FDR3 が出力する YAML 形式の反例情報かみ，メッセージを赤色で表示することとした．

ら違反箇所に至るまでのイベント列を取得し，イベン

3. 4. 2 要件 3-2 設計方針

ト列のうち，メッセージの送受信と状態変数の更新を反例情報から得た異常動作のシーケンス図だけで表すイベントを sd-DSL 形式に変換する方針とする．

は，違反箇所に至る経緯や要因が把握しにくい可能性

表 9，に反例情報と変換後の sd-DSL およびシーケがある．そのため，課題 3 である反例情報の解析能

ンス図の例を示す．表 9 の反例情報例は説明に必要な力習得コストを低減するためには，異常動作だけでな箇所のみを抜粋しており，実際の反例情報はもう少しく，期待動作のシーケンス図も表示できることが望ま複雑である．反例情報の 5 行目以降は，イベントのしい．

識別子となる整数 (以降，イベント ID と呼ぶ) とイ

期待動作のシーケンス図を作成するためには，期待ベントの対応を定義している．そして 1 行目は検査動作となる場合のシステム内部のイベント列を取得すモデルが検査仕様に違反しているイベント ID を示しる必要がある．一方，FDR3 は検査仕様に違反するており，2-4 行目が違反に至るイベント ID のトレー場合のイベント列を反例情報として出力する機能はス列を示している．

あるが，違反しない場合，つまり期待動作である場合

反例情報を元に sd-DSL へ変換するには，違反に至のイベント列の情報を出力する機能は有していない．

るイベント列の内容に従い変換していけば良い．たと提案ツールでは，内部仕様と外部仕様の整合性検査

表9

反例情報と変換後の sd-DSL およびシーケンス図の例

反例情報例 (抜粋)
1 error_event: 2
2 trace:
3
- 0
4
- 1
5 event_map:
60: msg_.A.B.B_m1.0
7
1: update_.B_Ready_v0.082: msg_.B.A.return_B_m1.true

sd-DSL
1
2
3
4
5
6
7
8
9

シーケンス図@startuml
participant A
participant B
A -> B ++ : m1(0)note over B : v0=0
group neg
A <-[#red]- B -- : <color red>true</color>end@endumlの結果として取得した反例情報を，異常動作の振る舞イルと外部仕様を表現する PlantUML の sd-DSL 形

い (外部仕様に違反する振る舞い) を行う外部仕様と式のファイル，また定義情報を記述した YAML 形式

して位置づけ，その外部仕様と内部仕様との整合性検のファイルを入力にとり，3. 2 節および 3. 3 節で説明

査を行うことで反例情報として期待動作 (外部仕様にした設計方針に従い，3. 1. 2 小節で述べた内部仕様と違反しない振る舞い) のシステム内部のイベント列を外部仕様の整合性が FDR3 を用いて検査することが取得する方針とした．

できる CSPM の検査モデルおよび検査仕様に変換し3. 4. 3 要件 3-3 設計方針

たのち，結果となる CSPM をファイルに出力する機

違反箇所に至る経緯や違反の要因の把握を容易に能を提供する．実装言語は Python [9] であり，空行するためには，期待動作のシーケンス図と異常動作のを除いた有効行数は 600 行となった．

シーケンス図の差分が明確であり，比較しやすいように表示が調整されている必要がある．

4. 2 機能 3 の実装

期待動作のシーケンス図と異常動作のシーケンス

機能 3 は，要件 3-1 に対応するツールと，要件 3-3

図の差分を明確に表示するために，期待動作と異常動に対応するツールの 2 つツールにより実装されてい作の sd-DSL の差分箇所について，メッセージの色をる．要件 3-2 についてはツールによる自動化に対応せ変えハイライト表示する方針とする．また，期待動作ず，設計者が手動で対処する方針とした．

のシーケンス図と異常動作のシーケンス図を，左右に要件 3-1 に対応するツールは，FDR3 が出力する

並べて差分が確認できるように，メッセージの表示位

YAML 形式の反例情報を入力にとり，3. 4. 1 小節で置が一致するようにメッセージの間隔を調整する方針

説明した設計方針に従い PlantUML の sd-DSL に変とする．

換したのち，結果となる sd-DSL をファイルに出力する機能を提供する．実装言語は Python で空行を除い4 実装
本章では，3 章で述べた設計方針に従い機能 1，2，

3 を実装したツールについて述べる．

た有効行数は 122 行となった．
要件 3-3 に対応するツールは，期待動作の sd-DSLと異常動作の sd-DSL を入力にとり，差分となるメッ
セージや状態変数の更新箇所を色づけてハイライト

4. 1 機能 1 および機能 2 の実装

し，差分前後のメッセージや状態変数の更新箇所の

3. 3 小節で説明したとおり，機能 1 と機能 2 は，表示位置が一致するようにメッセージの間隔を調整

sd-DSL を CSPM へ変換するという点において一部した sd-DSL を出力する機能を提供する．実装言語はの設計方針を除き基本的には同等の機能の実装を必

Python で空行を除いた有効行数は 28 行となった．

要とするため，実際には 1 つのツールとして実装されている．機能 1 と機能 2 を実装したツールは，内部仕様を表現する PlantUML の sd-DSL 形式のファ5 評価
本章では，提案ツールの評価として，2. 1 節で説明
した業務で実際に検出した不具合事例に提案ツール
を適用することで目標の達成を確認する．

5. 1 機能 1 と機能 2 に対応するツールの適用
内部仕様として，業務モデルのシステム内部の各オブジェクトのシーケンスを PlantUML の sd-DSL
形式で記述した．図 6 は，業務モデルの IpcServerというオブジェクトの内部仕様の記述例である．業
務モデルのすべてのオブジェクトの内部仕様 sd-DSLの空行を除く有効行数の合計は 190 行となった．記述した sd-DSL は PlantUML によりシーケンス図に作図できることを確認している．sd-DSL を記述する
際，シーケンス図を確認しながら作図できるため，内部仕様の妥当性を視覚的に確認しながら記述することができることを確認した．
同様に，業務モデルの外部仕様として，図 2 で示した業務モデルの期待動作のシーケンスを PlantUMLの sd-DSL 形式で記述した．図 7 に業務モデルの外部仕様を示す． 外部仕様 sd-DSL の空行を除く有効行
数は 62 行となった．記述した sd-DSL は PlantUML
によりシーケンス図に作図できることを確認している．こちらも内部仕様と同様にシーケンス図を確認しながら作図できるため，外部仕様の妥当性を視覚的に確認しながら記述することができることを確認した．
機能 1，機能 2 では内部仕様と外部仕様で現れるメッセージの型情報を定義情報として別途ツールに入力することで，検査モデルでの式の評価を可能としている．業務モデル用に記述した定義情報の空行を除く
有効行数は 70 行となった．
業務モデルの内部仕様と外部仕様および定義情報

図7

業務モデルの外部仕様

を 4. 1 節で述べた sd-DSL を CSPM に変換するツー
ルに入力し，検査モデルと検査仕様の CSPM が得られることを確認した．出力された CSPM の空行を除

5. 2 FDR3 による内部仕様と外部仕様の整合性
検査

く有効行数は 381 行となった．381 行のうち，内部

5. 1 節で述べた検査モデルと検査仕様の CSPM を仕様である検査モデルの記述に該当するのは約 320

FDR3 に入力し，内部仕様と外部仕様の整合性検査

行，外部仕様である検査仕様に該当するのは約 80 行の結果として YAML 形式の反例情報が得られることであった．

を確認した．FDR3 の検証に要した時間は，CPU：

1.8GHz Intel Core i7，メモリ：4GB の環境で 0.745

ジの間隔を調整するツールに入力することで，差分が秒であった．

明確になるように調整された sd-DSL が出力されることを確認した．差分がハイライトされた sd-DSL は，

5. 3 要件 3-1 に対応するツールの適用結果

PlantUML によりシーケンス図を作図できることを確

5. 2 節で得られた YAML 形式の反例情報を，4. 2

認している．表 10 に差分がハイライトされた期待動作

節で説明した，反例情報を sd-DSL に変換するツールと異常動作のシーケンス図を示す．違反箇所が赤色に，により入力することで，異常動作の sd-DSL が出力さ両者の差分が青色にハイライトされ，また両者の同じれることを確認した．異常動作の sd-DSL の空行をメッセージの位置が一致するようにメッセージの間隔

除く有効行数は 146 行であった．異常動作の sd-DSLが調整され，期待動作と異常動作の振る舞いを容易には PlantUML を用いてシーケンス図に変換できるこ比較できることがわかる．これにより，期待動作と異とを確認している．

常動作の差異が，Executor から CallbackThread へ

異常動作のシーケンス図は，外部仕様の違反箇所がの sendResult(READ, CANCELED) メッセージの呼びシーケンス図の複合フラグメント neg によりハイラ

出しタイミングに起因することが容易に判断できる．

イト表示されていることを確認しており，図 3 で示した異常動作のシーケンス図の内容と一致しているこ

5. 6 提案ツールを適用しなかった場合との比較とを確認した．

本節では，提案ツールを適用しなかった場合と適用した場合について課題毎に比較し，提案ツールの効果

5. 4 要件 3-2 の実施結果
要件 3-2 については，4. 2 節で述べたとおり，手動を確認する．

5. 6. 1 検査モデルの記述 (課題 1)

で異常動作に含まれる違反箇所を外部仕様に取り込提案ツールを適用しない場合，内部仕様である

むことで対応する．具体的には，5. 1 節で記述した外CSPM を直接記述する必要があり，CSPM の学習コ部仕様 sd-DSL を元に，5. 3 節で取得した異常動作のストがかかる．また，CSPM の記述の妥当性を確認

sd-DSL から違反箇所の sd-DSL の記述を取り込み，する方法としては CSPM の有識者によるレビューし反例情報として期待動作のイベント列を取得するこ

か方法がなく，プロジェクト内に CSPM 有識者が複とができる外部仕様の sd-DSL を作成した．作成した数人いることが必要となる．

期待動作取得用の外部仕様の sd-DSL と内部仕様の一方で，提案ツールを適用した場合は，内部仕様を

sd-DSL を，4. 1 節で述べたツールにより CSPM へ

sd-DSL で記載するため，sd-DSL の記法を学習する変換したのち，FDR3 を用いて検査することで期待必要はあるが，sd-DSL の記法はシーケンス図の構成

動作を表す反例情報が出力され，その反例情報を 4. 2

要素と対応がとれており，作図しながら sd-DSL の記節で述べた要件 3-1 に対応するツールを用いること

載内容が確認できるため比較的学習が容易である．まで期待動作の sd-DSL に変換できることを確認した．

た，内部仕様がシーケンス図として表現されるため，作成した期待動作の sd-DSL は，PlantUML を用い妥当性を確認するために sd-DSL を習得する必要はてシーケンス図を作図できることを確認している．期

なく，一般的な設計者によるレビューが可能である．

待動作のシーケンス図は，図 2 で示した期待動作の

内部仕様の記述量を比較すると，5. 1 節で述べたシーケンス図の内容と整合していることを確認した．

とおり，内部仕様を CSPM で直接表現する場合は約320 行の記述が必要であるが，sd-DSL と定義情報で
5. 5 要件 3-3 に対応するツールの適用結果

記述する場合は，それぞれ 190 行と 70 行の記述で済5. 3 節と 5. 4 節により得られた，期待動作の sd-DSL

むため，提案ツールを適用した場合のほうが検査モデと異常動作の sd-DSL を，4. 2 で説明した期待動作と異常動作の sd-DSL の差分をハイライトし，メッセー

ルの記述コストを下げられることがわかる．

表 10

提案ツールが出力する期待動作と異常動作のシーケンス図の差分表示の例
期待動作

異常動作

5. 6. 2 検査仕様の記述 (課題 2)

確認の容易性，記述コストの面で優位性があるとい検査仕様を記述する場合においても，5. 6. 1 小節

える．

と同様の理由で，提案ツールを適用せずに CSPM を

実際に外部仕様の記述量を比較すると，外部仕様を直接記述する場合に比べて，提案ツールを適用してCSPM で直接表現する場合は約 80 行の記述が必要で

sd-DSL を記述した場合のほうが学習コストや妥当性あるが，sd-DSL と定義情報で記述する場合は，定義

情報は内部仕様と共有であるため sd-DSL の 62 行のストを抑えながら効果的に検出・解析できることを確記述で済み，提案ツールを適用した場合のほうが検査認した．以上より，2. 1 節で掲げた提案ツールの実現

仕様の記述コストを下げられることがわかる．

により達成するべき目標が達成できたと判断した．

5. 6. 3 反例情報の解析 (課題 3)
提案ツールを適用しない場合，FDR3 が出力する

6 おわりに反例情報を直接解析する必要がある．図 8 に，業務

本論文では，はじめに，著者がデバイス制御ミドル

モデルの検査モデルと検査仕様を FDR3 に適用し出ウェアの開発業務経験より，再現性の低い不具合を効力された反例情報の表示例を示す．

果的に検出することが困難であることに問題意識を

FDR3 が出力する反例情報は，FDR3 独自の形式もっていることを示し，モデル検査を業務に適用するで表示される．具体的には，縦にプロセスの一覧が並場合に 3 つの課題があることを説明した．そして，こび，横にイベントが，発生したプロセス上に発生したれらの問題意識と課題より，提案ツールの実現により順で並んで表示される．この表示形式の問題点は，す達成するべき目標と要求される機能について述べた．

べてのプロセス間のメッセージのやりとりが平坦に

次に，要求される機能毎に求められる要件を説明し，表示されるため，メッセージがどのプロセス間でやりそれぞれの要件毎に設計方針としてどのような方法とりされているのか一見しただけではわからないこで実現したのかを述べた．また，設計方針に従った提とである．そのため，検査対象が複雑なモデルになれ

案ツールの実装について述べた．最後に，提案ツール

ばなるほど，反例を解析する場合に違反箇所に至るを業務モデルに適用した場合の効果と，適用しなかっ経緯を推測するのが非常に困難になる．実際に，図 8た場合との比較を説明し，提案ツールの有効性を示し

では業務モデルの反例情報を FDR3 で表示している

た．結果として，提案ツールを適用することで，外部が，膨大なイベント列が平坦に表示されているため，仕様と内部仕様の不整合に起因して発生する再現性違反箇所に至る要因をこの反例情報から解析するのの低い不具合事例が，学習コストを抑えながら効果的が困難であることがわかる．また，反例情報として仕に検出・解析できることを確認した．

様に違反する異常動作のみが表示されるため，期待動提案ツールに関する今後の展開としては，4. 2 節で作となる場合の検査モデルの振る舞いが明確でない

ツールではなく手動で対応すると述べた要件 3-2 を自状態で解析する必要があることも，解析を困難にする

動化することが挙げられる．要件 3-2 の作業をツール要因となっている．

により自動化するためには，違反箇所が外部仕様のど一方で提案ツールを適用した場合は，表 10 で示しの箇所で発生しているかをツールが判断できるようにたとおり，反例情報が馴染みのあるシーケンス図で表する必要があるため，外部仕様の各メッセージに識別示されるため，直感的，視覚的に違反に至る経緯を把

番号を振るといった修正が必要になると考えている．

握することができる．さらに，期待動作と異常動作をまた，本論文により業務モデルの不具合事例が効果的

比較しながら確認することができ，また違反箇所やに検出・解析できることは確認できたが，他の事例に期待動作と異常動作の差分がハイライトされるため，対しても有効であるか，つまり，汎用的に利用できる

違反箇所に至る要因を容易に解析することができる．

ツールとなっているかについては未確認であるので，他の事例に適用し効果を測定することも有益である

5. 7 評価結果のまとめと考えている．

5. 1 節から 5. 5 節にて，業務モデルに対し提案ツールを適用した場合の効果を確認した．また，5. 6 節に

参 考 文 献て，提案ツールを適用しなかった場合と比較すること[ 1 ] Ben-Kiki, O., Evans, C., and Ingerson, B.:
YAML Ain’t Markup Language (YAML) TM Version
1.2, Technical report, YAML.org, 2009.
[ 2 ] Crockford, D.: JSON: Javascript object nota-

で，提案ツールにより外部仕様と内部仕様の不整合に起因して発生する再現性の低い不具合事例が，学習コ

!"#

図8

FDR3 が出力する業務モデルの反例情報の表示例

tion, 2006.
[ 3 ] Hoare, C. A. R.: Communicating Sequential
Processes, Prentice Hall, 1985.
[ 4 ] Object Management Group, inc.: Unified Modeling Language (UML): Infrastructure specification,version 2.4.1, 2011.
[ 5 ] Object Management Group, inc.: Unified Modeling Language (UML): Superstructure specification, version 2.4.1, 2011.
[ 6 ] Roques, A.:
PlantUML, http://plantuml.
sourceforge.net, 2013.
[ 7 ] Roscoe, A. W.: The Theory and Practice ofConcurrency, Prentice Hall, 1997.
[ 8 ] Rumbaugh, J., Blaha, M., Premerlani, W.,
Eddy, F., Lorensen, W. E., et al.: Object-oriented
Modeling and Design, Vol. 199, No. 1, Prentice-hallEnglewood Cliﬀs, NJ, 1991.

[ 9 ] Sanner, M.: Python: A Programming Language
for Software Integration and Development, J. Mol.
Graphics Mod, Vol. 17(1999), pp. 57–61.
[10] Scattergood, B.: The Semantics and Implementation of Machine-Readable CSP, PhD Thesis, Oxford University, 1998.
[11] Thomas Gibson-Robinson, Philip Armstrong, A.
B. A. R.: FDR3 — A Modern Model Checker
for CSP, Tools and Algorithms for the Construction and Analysis of Systems, brahm, E. andHavelund, K.(eds.), Lecture Notes in Computer Science, Vol. 8413, 2014, pp. 187–201.
[12] University of Oxford: Failures-Divergence Refinement – FDR 3 User Manual, https://www.cs.
ox.ac.uk/projects/fdr/manual/, 2013.
[13] 後 藤 隼 弐:
csp-seq, https://github.com/
goto-junji/csp-seq, 2014.