背景 並行システム : 協調する複数の処理 ( プロセス ) から構成されるシステム 並行システムの例 ( 昇降舵のフライバイワイヤ ) 操縦桿 x2 角度 x3x2 ジャイロ x3 重量計 x4 フラップ LVDT IRU WOW FSACE PB 優先ボタン x2 MON モニタ COM コマン

並行システム解析支援ツール

～協調動作の可視化～

第

10回クリティカルソフトウェアワークショップ 10

th

_WOCS

2

2012年9月28日

この資料の一部またはすべての内容について、作成者の許可なき使用・複製・配布を固くお断りします

○磯部祥尚

*

1

, 大岩寛

*

1

, 高橋孝一

*

1

, 田中純

*

2

産業技術総合研究所

*

1

_{セキュアシステム研究部門}

_,

_*

2

_{イノベーション推進本部}

背景

 並行システム：

協調する複数の処理（プロセス）

から構成されるシステム

並行システムの例（昇降舵のフライバイワイヤ）

角度

x3x2

ジャイロ

x3

重量計

x4

フラップ

操縦桿

x2 IRU WOW FSACE

MON

モニタ

COM

コマンド LVDT ACE, PCU PB

優先ボタン

_x2

フライト制御

x4

アクチュ

エータ

x4 協調

センサ

プロセッサ アクチュエータ

（エンブラエル社 レガシー）

なぜ並行システム？

 センサに対する応答性

 故障時に対する冗長性

 制御情報の通信（共有）

 背景

：ネットワークやマルチコアの普及によって、並行処理が身近になっている

 課題

：全体で正しく並行処理するように、個々のプロセスを設計するのは難しい

目標

 目標

：設計モデルの協調動作を理論的に解析するツール

_CONPASU

の開発

手戻りコスト

削減

 効果

：信頼性の向上、手戻りコストの削減

CONPASU-tool

REM SQ SUM

並行システムのモデル

解析

設計

要求

分析

実装

結合

テスト

受入

テスト

単体

テスト

フィードバック

解析結果

設計レビュー支援

発表概要

 はじめに（済）

 背景

 目標



CONPASUツールの特徴

 並行システムの解析例

 協調動作の可視化

 モデル検査との違い



CONPASUの適用

 既存ツールとの連携



CSPモデルベース設計工程



CONPASUの機能

 記号処理

 状態数削減

 おわりに

 まとめ、今後の課題

pp.5-11

pp.12-15

pp.16-20

CONPASUツールの特徴

 並行システムの解析例

 協調動作の可視化

UI

並行システムの解析例

 並行システム全体の動作を把握するのは難しいので…

input

ok

ng

quit0

succ

start

net

term

quit1

ack

upload

cancel

complete

output

Sender

Receiver

構造

UI

Receiver

Sender

通信

通信

振舞い

？

UI

並行システムの解析例

 並行システム全体の動作の可視化するツール

CONPASU

[1]

_を開発中

input

ok

ng

quit0

succ

start

net

term

quit1

ack

upload

cancel

complete

output

Sender

Receiver

構造

UI

Receiver

Sender

通信

通信

振舞い

！

並行システム

全体の振舞い

τ[#ds0>0] /ds0:=tail(ds0), ds1:=ds1^<head(ds0)> @(0(11))

デッドロック

入力：

 並行システムの構造

 各プロセスの振舞い

出力：

 全体の振舞い

処理：

 並行合成

 状態数削減

CONPASU-tool

CONPASU（産総研知財管理番号：H24PRO-1409）

協調動作の可視化

 既存のツール（例：

PAT

[10]

_{, LTSA}

[11]

_{）でも状態遷移図を表示できる}

⇒

_{入力値は具体化されるため}

状態数が多くなる

REM SQ SUM

状態数

_{: 42}

遷移数

: 67

LTSA

パイプライン並列計算の例

状態数

_{: 105}

遷移数

_{: 160}

PAT

入力値

_:{0,1}

入力回数

_:3

状態数

: 8

遷移数

_{: 12}

CONPASU

入力値

_:無制限

入力回数

_:任意

in.0

in.1

in?x1

状態数

: 3

遷移数

_{: 3}

状態遷移図の抽象化



CONPASUでは興味のあるイベントに着目した状態数の削減が可能

状態数

: 8

遷移数

_{: 12}

CONPASU

CONPASU-tool

途中結果の

表示を隠蔽

REM SQ SUM

in?

x1

[

n>0

]

/

y:=y+(x1

*

x1)%10,n:=n-1

@ ((11)1)

（計算式が見える！）

状態数

: 3

遷移数

_{: 3}

計算過程の可視化



CONPASUでは任意の入力値に対する計算過程（計算式）を確認できる

in.0

in.1

in.1

prts.2

入力値

_:{0,1}

入力回数

:3

状態数

: 105

遷移数

_{: 160}

入力値

_:無制限

入力回数

:任意

CONAPSU

PAT

式

値

in?x1

比較

モデル検査との違い



CONPASUでは検証用の性質（時相論理式など）を

記述

する必要がない

Snd

in

Ack

c2

ack

Rcv

out

c1

□（

_{in→◇ack）}

性質（時相論理）

並行システムの設計モデル

逐次動作

“in” の後にいつか “ack” が起きる？

“

in” と“ack” の関係は？

in

ack

in

ack

in

ack

c1

c2

out

c2

ack

c1

in

この性質を記述

inとackを選択

 性質（逐次動作）はCONPASUが

抽出する

 両ツールを

併用すると効果的

CONPASUの適用

 既存ツールとの連携

変換器

UML→CSP_M

既存のモデル／ツールとの連携



CONPASUは形式手法

CSP

*

1[2,3]

_{に基づく解析ツール}



CONPASUの入力言語には形式言語

CSP

_M

*

2

_を採用

（例：モデル検査器

_{FDRと連携して、UMLモデルを解析可能）}

Snd = in -> c1 -> Snd Rcs = c1 -> out -> c2 -> Rcv Ack = … Sys = ((Snd|||Ack) [|…|]Rcv)＼{…} （サリー大学[7]_） モデル検査器[8] （オクスフォード大学） モデル検査器[9] デュッセルドルフ大学、 サウサンプトン大学 モデル解析器[1]_{（産総研）} *1 _{CSP : 並行システムを記述し、解析するための理論（プロセス代数）} *2 _CSP M: CSPの代表的なモデル検査器FDRの入力言語（関連研究が多い）

変換器

SimuLink→CSPM ペルナンブコ連邦大学、 エンブラエル社[6]

CONPASU

ProB

FDR

MATLAB/Simulink

UML State M.

UML Activity

CSP

_M

言語

意味論

状態遷移図

形式手法

CSP

in

_out

CNTL

back

x

_y

z

in?x

back?z

out!y

y:=

f(x,y,z)

UI

𝑓 𝑥, 𝑦, 𝑧

= 𝑥 + 𝑦 − 𝑧 ∗ 𝐶

協調部（構造）

協調部（振舞い）

データ部（関数）



CSPモデルはメッセージパッシング通信を採用

⇒ 協調部（並行処理）とデータ部を分割して設計しやすい

 比較：共有メモリではプロセス間の結合強度が高い（分割しにくい）

x

_z

y

y:=g(x,z)

共有メモリ

z:=h(x,y)

x:=f(y,z)

設計手順・役割分担の明確化

プロセス

チャネル

データ部

概念モデル

解析済の

CSPモデル

シミュレーション

CSPモデルベースの設計工程



CSPでは協調部（並行処理）とデータ部を分割して設計・解析しやすい

データ部

（関数定義等）

網羅的解析

構造図（コンポーネント図）

協調部

振舞い図（ステートマシン図）

int fact(n){ ... }

協調部

設計工程

解析工程

間違えやすい協調部は網羅的解析

（

_{CONPASUに実装中）}

状態数の多いデータ部はシミュレーション解析

（

_{CONAPSUに実装予定）}

CONPASUの機能

 記号処理

 状態数削減

CONPASUの機能



CONPASU

は並行処理の全体像を解析して可視化するツール

 逐次化機能

: 並行処理を

記号的意味論

によって逐次処理に展開する機能

 状態数削減機能

: 振舞いの等しさを保ったまま状態数を減らす機能

並行システムの設計モデル

in

c1

B1

B0

c2

B2

out

逐次化

（

_CONPASU）

状態数削減

（

_CONPASU）

状態数

_{: 8}

容量3のバッファ

状態数

_{: 4}

CONPASU

c1

in

c2

c1

out

c2

ack

in?

_𝑥

out!(

_{𝑥 × 2)}

記号的意味論

 プロセス代数の

記号的意味論

[4,5]

_は

_{1995年頃から研究が行われている}

Proc = in?

𝑥 → out!(𝑥 × 2) → ack → Proc

CSPモデル

（普通の）意味論

記号的意味論

in.0

in.1

in.2

in.9

…

out.0

out.2

out.4

out.19

…

ack

入力値

_{𝑥 ∈ {0, … , 9}}

○

状態数の増加を抑えられる

×

解析（等価性判定など）は難しい

変数

値

状態数削減

 状態遷移図（変数含）の振舞いを変えずに

状態数を削減する方法

を考案

 振舞いを変えないように内部動作をバイパスする

（注：振舞いに影響する、すなわちバイパスできない内部動作もある）

 振舞いの等しさには

CSPの失敗等価性 ＝

_F

を採用

/ n:=1,m:=0

print!

n

print!

n

τ

/

m:=m+2

τ

/

m:=m+2

STOP

print!

m

S1(n, m) S2(n, m) S3(n, m) S4(n, m)

bak/

n:=n+1

bak/

n:=n+1

観測されない内部動作

/ n:=1, m:=0+2

print!

n

STOP

print!

m

bak/

n:=n+1

S2(n, m) S4(n, m)

並行処理では、このような順番が可換な振舞いはよく現れる（インターリービング）

状態数削減

＝

_F

UI

並行システムの解析例

 並行システム全体の動作の可視化するツール

CONPASU

を開発中

input

ok

ng

quit0

succ

start

net

term

quit1

ack

upload

cancel

complete

output

Sender

Receiver

構造

UI

Receiver

Sender

通信

通信

振舞い

！

入力：

 並行システムの構造

 各プロセスの振舞い

出力：

 全体の振舞い

処理：

 並行合成

 状態数削減

CONPASU-tool

普通の意味論

で状態遷移図

を作成した場合（

_FDR使用）

状態数：

約

_12万

データ種類：

_4種類

転送回数：

_4回

状態数

: 8

おわりに

 まとめ

まとめ



CONPASU研究のポイント

 ネットワークやマルチコアの普及によって、並行処理が身近になっている

 複雑な並行処理の全体像を解析して、

簡潔に可視化するツール

を開発



UMLなどの並行処理も解析可能で、既存の開発工程への導入が容易

⇒

_{信頼性の向上、手戻りコストの削減}

手戻り

コスト

削減

設計

UML

要求

分析

結合

テスト

受入

テスト

単体

テスト

解析

CSP

（

_CONPASU）

解析

UML

UMLモデルベース開発工程への導入

実装

設計

CSP/UML

要求

分析

（

_CONPASU）

解析

CSP/UML

CSPモデルベース開発工程の採用

実装

…

並行処理の明確化、

検証効率の向上

今後の課題

 解析結果のフィードバック方法

 見やすい解析結果の表示方法

 解析結果ともとのモデルとの対応表示方法、他

設計モデル

_解析結果

解析

フィードバック

 モデルの表現力の拡張

 実数など、

CSP

_M

では未対応のデータ型も扱えるようにする

参考文献

1. （CONPASU）Y. Isobe, CONPASU-tool: A Concurrent Process Analysis Support Tool based on Symbolic Computation, CPA2011, WoTUG-33, IOS Press, pp.341-362, 2011.

http://staff.aist.go.jp/y-isobe/conpasu/

2. （CSP）C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, 1985. http://www.usingcsp.com/cspbook.pdf

3. （CSP）A. W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall, 1998. http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf

4. （記号的意味論）Z. Li and H. Chen, Computing strong/weak bisimulation equivalences and observation congruence for value-passing processes, TACAS '99, LNCS 1579, Springer, pages 300-314, 1999.

5. （記号的意味論）M. Hennessy and H. Lin, Symbolic bisimulations, Theoretical Computer Science, Volume 138, Issue 2, pp.353-389, 1995.

6. （Simulink-CSP）J. Jesus, A. Mota, A. Sampaio, and L. Grijo, Architectural Verification of Control Systems Using CSP, ICFEM 2011, LNCS 6991, Springer, pp.323-339, 2011.

7. （UML-CSP）I. Abdelhalim, S. Schneider, and H. Treharnea, Towards a Practical Approach to Check UML/fUML Models Consistency Using CSP, ICFEM 2011, LNCS 6991, Springer, pp.33-48, 2011.

8. （FDR）Formal Systems (Europe) Limited, Failures-divergence refinement: FDR2, http://www.fsel.com/

9. （ProB）Universität Düsseldorf and University of Southampton, The ProB Animator and Model Checker. www.stups.uni-duesseldorf.de/ProB/

10. National University of Singapore, PAT: Process analysis toolkit. http://www.comp.nus.edu.sg/~pat/ 11. Imperial College London, LTSA - labelled transition system analyser. http://www.doc.ic.ac.uk/ltsa/