An Introduction to
Communicating Sequential Processes
Hisabumi HATSUGAI
[email protected]
PRINCIPIA Limited
http://www.principia-m.com/
©2016 PRINCIPIA Limited
1
並行システムとリアクティブシステム
●
多くのシステムは並行システムである：
–
並行に動作する複数の実行主体からなり，協調して目的の仕
事をするシステム
–
例
●
組込システム
–
–
●
アプリケーション
–
–
●
複数の CPU ，複数のプロセス
並行動作するデバイス群
ユーザインタフェイス
ネットワーク通信
並行システム
並行システムはリアクティブシステムである：
–
外界との相互作用
–
継続的な動作
©2016 PRINCIPIA Limited
2
計算システムとリアクティブシステム
in
in
f
out
out
計算システム
リアクティブシステム
「リアクティブシステムとは，システムの外部（システムの利用者や他のシス
テムなど）とのやりとりを行いながら計算の実行やサービスの提供を継続する
ことを目的とするシステムである．」
– コンピュータサイエンス入門 － 論理とプログラム意味論，岩波書店
©2016 PRINCIPIA Limited
3
並行システム
●
並行システムは階層的なリアクティブシステムである
–
構成要素（コンポーネント）もリアクティブシステム
–
外界とシステム，および構成要素間にも相互作用がある
自律的に動作
する実行主体
相互作用
相互作用
©2016 PRINCIPIA Limited
このようなシステムの振る舞いを規定し，設計し
検証するためには何が必要か
4
計算システムの開発基盤
システムの認識
システムをどのようなものだと認
識するか
システムの記述
仕様と実装をどのように記述する
か（振る舞いについて）
記述の意味
記述が意味することをどのように
厳密に定めるか
正当性の条件
計算
入出力の関係
仕様：数学による関係表現，事前・事後条件
実装：プログラミング言語
表示的意味論：プログラム→入出力の関係
包含関係は実装を容易に
操作的意味論
するためのゆとり (opt.)
公理的意味論： Hoare 論理
  R  dom   dom R
実装が仕様を満たしているという
仕様
条件は何か
検証の方法
正当性を検証する方法にはどのよ
うなものがあるか
©2016 PRINCIPIA Limited
対比として
実装
 dom   R  S
仕様が規定する範囲の
入力は受理できること
出力は仕様が規定する
範囲から選ぶこと
表示に基づくテスト，正当性条件の証明
Hoare 論理
定義域制限演算子
包含関係は
非決定性の減少
A  R  {(x, y) | x  A  (x, y)  R}
5
CSP とは
●
●
Communicating Sequential Processes
並行システムの振る舞いを記述し，その性質を論証するための数
学的理論
–
プロセス代数と呼ばれる理論の 1 つ（他に計算など）
●
1978 年 C. A. R. Hoare によって提案された
●
特徴
–
詳細化関係の定義
–
豊富な意味論
©2016 PRINCIPIA Limited
Photograph by Rama, Wikimedia Commons, Cc-by-sa-2.0-fr
6
並行システムの開発基盤
システムの認識
システムをどのようなものだと認
識するか
計算と相互作用
継続的に相互作用を行う状態遷移システム
システムの記述
仕様と実装をどのように記述する
か（振る舞いについて）
記述の意味
記述が意味することをどのように
厳密に定めるか
正当性の条件
実装が仕様を満たしているという
条件は何か
検証の方法
正当性を検証する方法にはどのよ
うなものがあるか
©2016 PRINCIPIA Limited
7
システムの認識：時間と状態遷移
●
「継続的に」
–
物理世界の時間概念に対応する何等かの抽象的な時間概念が
必要．時間経過とともにシステムが変化する
状態遷移システム
●
–
ある時刻における実行の断面としての状態がある
–
システムの変化としての遷移がある
遷移の発生順序関係を抽象的・離散的な時間と考える
–
遷移の発生を瞬間的なものと理想化して考える
–
遷移間の状態に滞在する時間の長さは捨象する
※ 定量的な時間を導入した理論もある： Timed-CSP
©2016 PRINCIPIA Limited
8
相互作用とは何か
●
情報を伝達し，お互いの振る舞いに影響を与えるもの
●
応用で利用されている相互作用例：
●
–
制御渡し，共有メモリ，メッセージ通信，同期機構（セマフォ，
ミューテックス，条件変数等），ソケット
–
ユーザとの対話
–
CPU とデバイス間の通信
理論でプリミティブとする相互作用に望まれる性質：
–
意味が厳密で議論・分析に適している
–
上述のような既存の相互作用を記述（モデル化）できる
–
並行合成を定義できる
–
振る舞いの記述が可能でそれに基づいて正当性が定義できる
©2016 PRINCIPIA Limited
9
プリミティブ相互作用の選択
e
イベントによる同期型相互作用
e
e
CSP
遷移が同時に発生することが相互作用であると
考える．同じラベルの付いた遷移が同期する．
これをイベントという．イベントは作用の意味
を表す．
s := f(x)
共有メモリによる相互作用
x

y
?
e
共有メモリを通じて情報の受け渡しを行う．遷
移はすべて独立して発生する．遷移に付随して
[g]/y := h(s) 共有メモリの読み書きができる．ガードによっ
てブロックを表すモデルもある．
非同期相互作用（？）
e
e
©2016 PRINCIPIA Limited
発生した遷移に付随する情報がなんらかの方法
で時間的に後の時刻に別のコンポーネントに届
き，遷移を引き起こすとともに情報が渡され
る．
10
並行システムの開発基盤
システムの認識
システムをどのようなものだと認
識するか
システムの記述
仕様と実装をどのように記述する
か（振る舞いについて）
計算と相互作用
継続的に相互作用を行う状態遷移システム
CSP の構文：
イベント同期，チャネル送受信，選択，非決定的選択，
並行合成，隠蔽，逐次合成，改名
記述の意味
記述が意味することをどのように
厳密に定めるか
正当性の条件
実装が仕様を満たしているという
条件は何か
検証の方法
正当性を検証する方法にはどのよ
うなものがあるか
©2016 PRINCIPIA Limited
11
CSP 構文
 ::= STOP
| SKIP
| e
| A  
| c!v  
| c  
| cA  
|  <b> Q
|  Q
|  Q
|  Q
©2016 PRINCIPIA Limited
|  || Q
X
プロセス代数という名のとおり
プロセスの様々な振る舞いを表
すための定数と演算子がある
|  ||| Q
|  \X
|
|
|

i
iI

i
iI
||X 
i
iI
12
一部紹介
CSP 構文： 逐次プロセス
チャネル送信
イベント同期
e
cv
eP
チャネル受信
prefix-choice
a0
a1
a2
a3
a4
cv  P
c.a0
c.a1
c.a2
c.a3
c.a4
?x:A  P
ai  A
停止（デッドロック）
STOP
再帰
P  F (P )
c?x:A  P
ai  A
選択
P
P Q
Q
©2016 PRINCIPIA Limited
13
プロセスの定義例：キュー
in
Q
in?x/s := sx
out
s
out!hd(s)[s = ]/s := tl(s)
Q(s)  in?x  Q(sx) 
(if s =  then STOP else out ! hd(s)  Q(tl(s)))
※ STOP は選択  の単位元
©2016 PRINCIPIA Limited
14
CSP 構文： 並行合成
並行合成
 || Q
X
X
P
●
閉包性（ closure property ）
–
●
Q
プロセスと Q を並行合成したプロセスを表
す．イベントの集合 X に含まれるイベント
について同期する
プロセスを並行合成した結果はプロセスになる
合成性（ compositionality ）
–
並行合成したプロセスの振る舞いは，構成要素であるサブプロセスとその
間の相互作用によってすべて決定される
これらの性質のおかげで議論が容易になる
©2016 PRINCIPIA Limited
※ 関数型プログラミングにおける関数や，オブジェクト指
向プログラミングにおけるオブジェクトと同様（？）
15
CSP 構文： 隠蔽
隠蔽
Y
並行合成の結果としてのプロセスには
コンポーネント間の相互作用が残って
おり，外部から観測することができ
る．具体的にはイベント集合 X に含ま
れるイベントの発生が見える
X
Z
Y
P X
X
Z
©2016 PRINCIPIA Limited
隠蔽は指定されたイベントの集合に含
まれるイベントを不可視にする．これ
によって外部から観測可能なイベント
のみからなる合成系本来のプロセスを
得ることができる
16
内部遷移・非決定性
P \ b
P
a
a
b

非決定的選択
P Q


内部イベントによる分岐の形があると，どちらかの遷移
が自発的に発生して外部から制御することも観測するこ
ともできない．このような性質を非決定性という．非決
定性は再現しにくい不具合の原因になることがある．ま
た，非決定性は仕様において許容を表すためにも使用さ
れる
●
●
©2016 PRINCIPIA Limited
隠蔽されたイベントは  という特別なイベン
トになる．これは同期のためのイベントでは
なく自発的に発生する．外部から観測するこ
とのできないシステム内部での動作を表す．
内部イベントともいう．またこの遷移を内部
遷移という
非決定性は確率事象とは限らない．テスト回数を増やせば信頼
性が上がるとは必ずしもいえない
非決定性は計算システムにもある．同期しない遷移の発生順序
が任意であるであることから並行システムでは発生しやすい
17
発散（ライブロック）
内部遷移の循環ができると，自発的な遷移を繰り返し外部と相互作用ができなくなる．
この現象を発散（ divergence ）またはライブロックという
a






A

B
©2016 PRINCIPIA Limited

b
C
18
並行システムの開発基盤
システムの認識
システムをどのようなものだと認
識するか
システムの記述
仕様と実装をどのように記述する
か（振る舞いについて）
記述の意味
記述が意味することをどのように
厳密に定めるか
計算と相互作用
継続的に相互作用を行う状態遷移システム
CSP の構文：
イベント同期，チャネル送受信，選択，非決定的選択，
並行合成，隠蔽，逐次合成，改名
表示的意味論：トレース意味論，安定失敗意味論，
発散失敗意味論
操作的意味論
代数的意味論
正当性の条件
実装が仕様を満たしているという
条件は何か
検証の方法
正当性を検証する方法にはどのよ
うなものがあるか
©2016 PRINCIPIA Limited
19
CSP の表示的意味論
a

b

a
b
トレース意味論
安定失敗意味論
[ ]  traces(P )
[ ]  (traces(P ), failures(P ))
観測
failures(P ) =
{(s, X) | s  traces(P )  X  refusals(P /s)}

req, ack, calc, wait, ...
システムを外部から観測したときにみえる，
システムが発生させうるすべてのイベント列
の集合をプロセスの振る舞い（意味）だと考
える．システムが起動時から発生するイベン
ト列をトレースという
©2016 PRINCIPIA Limited
提示
プロセスが持つ非決定性を識別するために
拒否（ refusals ）という概念を導入する．
プロセスにイベントの集合  を提示したと
きにデッドロックする可能性があるならば
それを拒否という．各状態における拒否を
安定失敗（ failures ）といい，これを加えた
20
意味論を安定失敗意味論という
CSP 表示的意味論
failures(STOP) = ( X) | X  }
traces(STOP) = }
traces(SKIP) =  }
failures(SKIP) = ( X) | X  }  ( X) | X  }
traces(P  Q) = traces(P )  traces(Q)
failures(P  Q) = failures(P )  failures(Q)
traces(a  P ) = }  a^s | s  traces(P )}
traces(P  Q) = traces(P )  traces(Q)
traces(P  Q ) = s | s  traces(P )   A (s)}
failures(a  P ) = ( X) | a A X}  (a^s X) | (s X)  failures(P )}
failures(P  Q) = ( X) | ( X)  failures(P )  failures(Q)}
 (s X) | s =   (s X)  failures(P )  failures(Q)}
 s^t | s^  traces(P )  t  traces(Q )}
traces(P || Q ) = u | s t. s  traces(P )  t  traces(Q ) 
X
u  synchX(s t)}
traces(P \ X ) = s \ X | s  traces(P ) }
synchX(s t)  synchX(t s)
synchX( )  }
 ( X) | X      traces(P )  traces(Q)}
failures(P  Q) = (s X) | (s X  })  failures(P )}
 (s^t X) | s^  traces(P )  (t X )  failures(Q)}
failures(P || Q) = (u Y  Z ) | Y  (X  }) = Z  (X  }) 
X
(t Z )  failures(Q) 
x x  X x = x y y  A X
synchX( x)  }
synchX( y)  y}
synchX(x^s y^t)  y^u | u  synchX(x^s t)}
synchX(x^s x^t)  x^u | u  synchX(s t)}
synchX(x^s x^t)  }
synchX(y^s y ^t)  y^u | u  synchX(s y ^t)}
 y ^u | u  synchX(y^s t)}
synchX(s t^)  }
s t (s Y )  failures(P ) 
u  synchX(s t)
failures(P \ X) = (s \ X Y ) | (s X  Y )  failures(P )}
 \ X  
x^s \ X  s \ X
y^s \ X  y^s \ X
x  X y A X
s^ \ X  s \ X^
synchX(s^ t^)  u^ | u  synchX(s t)}
©2016 PRINCIPIA Limited
21
再帰的に定義されたプロセスの表示
例
再帰的に定義されたプロセスの表示は，定義式
から定まる意味関数の不動点になる
P  aP
traces(P) = traces(a  P)
P  F P 
traces(P) = }  a^s | s  traces(P)}
これは traces(P) を未知数  とする方程式になっている
[ ]  [F ]
X = }  a^s | s  X}
※ 連立方程式系の場合はもう少し複雑，不動点は関数になる
プロセス領域の構造（トレース意味論，安定失敗意味論の場合）
完備束（ Complete Lattice ）
●
●
●
完備距離空間（ CMS ）
集合の包含関係を順序とする
最小不動点（ least-fixed-point, lfp ）を採用す
るとよいことがわかっている
発散しているプロセスは一般に複数の不動点
を持つ
※ 再帰関数の理論と同様
©2016 PRINCIPIA Limited
●
●
●
トレースに基づく距離を定義する
唯一の不動点を持つ（意味関数が連続な縮小
写像になる）
発散しているプロセスを除く（より正確には
非構成的なプロセス）
※ 微分方程式の解の存在および一意性と同様
解の存在の保証と性質を議論するための基盤を提供してくれる
22
CSP の操作的意味論
イベントの集合（アルファベット）
プロセスの集合
各プロセスの記述（式）が持つ遷移を推論規則によって定める
u
P IP
●

●

矢印は遷移を表す関係   P    P
遷移のラベルはイベントのいずれか
内部イベント
例
正常終了イベント tick
前提

Para3
P IP
規則名


QIQ

P || QIP  || Q

a   
付帯条件

帰結
●
●
プロセスの遷移から状態遷移システム（ラベル付き遷移システム， LabelledTransition-System, LTS ）が求められる
遷移から traces, failures などの表示を求めることができる
©2016 PRINCIPIA Limited
23
CSP の操作的意味論
PName
a
P
P
a
N
P
Prefix
   

Skip

SKIP
a   
P
 || Q
X
Q
Para5

Q

P || Q
Q
P || 
X

P

PQ

P

P || Q
P

P Q
P

X
IntCh2
Seq1
Para4

P Q
a
aP
IntCh1
P
a = 

X
Para6

 || 
P Q

X
ExtCh1
a
P
a
P Q
ExtCh2
a
Q
P Q
ExtCh3
P
P Q
ExtCh4
P
Q
P Q
a = 
Q
a
Seq2
P
Q

P
PQ
a = 

P || Q

P || Q
X




P
P Q
P || Q
Q
P
P Q
©2016 PRINCIPIA Limited
Q
a
P || Q
X
Para3

a
a
a A   {}
X
P
P || Q
X

a
Q
a

P || Q
Q

P
Hide2
Hide3
P
P \X
P

P \X
a
P

P \X
X
Q
Para2

a A   {}
a
a
P \X
P
a
P
Hide1
Q
a
P
Para1

P


P \X
a A   {}
a  
P


a  
X
24
●
CSP の代数的意味論
●
●
●
同値なプロセスを代数規則（公理）によって定める
●
●
例
●
input-dist
?x  A  P  Q  ?x  A  P   ?x  A  Q
規則による同値変形
a  c  P || c  b  Q
= ||-step

a  c  P || c  b  Q
= ||-step

a  c  P || b  Q

ステップ則による書き換えによって並行合成
されたプロセスを逐次プロセスに書き換える
ことができる
©2016 PRINCIPIA Limited
冪等律
反射律
対称律
結合律
分配律
ステップ則
...
プロセスの標準形（ head-normal-form ）
?x :A

iI
i
i
 i
代数規則によって発散していないすべてのプロセス
をこの形に書き換えることができる．それにより再
帰プロセスの比較が可能になる（後述）．
非決定性を非決定的選択の部分に集約した形になっ
ている．
※ 終了するプロセスおよび発散を除く
25
代数的意味論
P || Q  Q || P
||-sym
P || (Q  R)  (P || Q)  (P || R)
||-dist
P || (Q || R)  (P || Q) || R
||-assoc
X
P PP
-idem
P PP
-idem
P QQP
-sym
P QQ P
-sym
X
X
X
X
X
X
X
X
X
X
X
P  Q  R  P  Q  R
-assoc
P  ?x  A  P , Q  ?x  B  Q
P  Q  R  P  Q  R
-assoc
P  Q  R  P  Q  P  R
P || Q  ?x  C  P  || Q <x  X>
-dist
a  P  Q  a  P   a  Q
prefix-dist
P  Q  R  P  Q  P  R
--dist
?x  A  P  Q  ?x  A  P   ?x  A  Q
input-dist
STOP  ?x    P
STOP  P  P
?x  A  P   ?x  B  Q 
<·>-dist-l
R <b> P  Q  R <b> P   R <b> Q
<·>-dist-r
P <true> Q  P
<true>-id
P <false> Q  Q
<false>-id
<·>--dist
X
P || Q <x  A> P || Q))
X
X
where C = X  A  B  A  X  B  X
P  Q \ X  P \ X  Q \ X
hide-dist
P \ X \ Y  P \ X  Y 
-step
P  Q <b> R  P <b> R  Q <b> R
Limited
P ©2016
 Q <b>PRINCIPIA
R  P  Q <b>
P  R
X

-unit
<·>-idem
X
X
P  || Q  P || Q <x  A  B>
STOP-step
?x  A  B  P  Q <x  A  B> P <x  A> Q
P <b> P  P
X
||-step
hide-combine
null hiding
P \ {}  P
a  P  \ X 
P \X
hide-step1
if a  X
a  P \ X
if a A X
(?x  A  P ) \ X

?x  A  (P \ X)
if A  X  {}
((?x  (A  X)  (P \ X))  STOP) 
if A  X = {}
hide-step


P [a/x] \ X
a A X

26
意味論の等価性（ congruence ）
表示的意味論と操作的意味論の等価性
操作的意味論から導出した表示と，表示的意味論によって定義された不動点
としての表示が一致することの証明
S.D. Brookes, A.W. Roscoe and D.J. Walker, An operational semantics for CSP,
Technical report, 1988
※ トレース意味論については定理証明系 Isabelle による形式的証明がある
表示的意味論と代数的意味論の等価性
表示的意味論によるプロセスの同値類と一致する代数的公理の選定および証明
Yoshinao Isobe, Markus Roggenbach, A Complete Axiomatic Semantics for the CSP
Stable-Failures Model, 2006
※ Isabelle によって形式的に証明されている．後ほど紹介する CSP-Prover の中に証明がある
©2016 PRINCIPIA Limited
27
並行システムの開発基盤
システムの認識
システムをどのようなものだと認
識するか
システムの記述
仕様と実装をどのように記述する
か（振る舞いについて）
記述の意味
記述が意味することをどのように
厳密に定めるか
正当性の条件
実装が仕様を満たしているという
条件は何か
計算と相互作用
継続的に相互作用を行う状態遷移システム
CSP の構文：
イベント同期，チャネル送受信，選択，非決定的選択，
並行合成，隠蔽，逐次合成，改名
表示的意味論：トレース意味論，安定失敗意味論，
発散失敗意味論
操作的意味論
代数的意味論
安全性 (safety)
S T R  traces(R)  traces(S)
活性 (liveness)
S F R  S T R  failures(R)  failures(S)
検証の方法
正当性を検証する方法にはどのよ
うなものがあるか
©2016 PRINCIPIA Limited
28
正当性関係（詳細化関係）
仕様を表すプロセス S と実装を表すプロセス R があり，実装 R が仕様 S を
満たしているとき， R は S を詳細化したものであるといい， 2 つのプロセス
の間には詳細化関係（ refinement relation ）があるという．これを以下の記
号で表す．これはいわゆる正当性関係を一般化したものである
安全性 (safety)
SR
仕様が行ってもよいということだけ
を行う
表示的意味論（トレース）による定義
S T R  traces(R)  traces(S)
表示的意味論（安定失敗）による定義
活性 (liveness)
仕様が拒否してもよいというイベン
ト集合だけ拒否する
S  R  S T R  failures(R)  failures(S)
代数的意味論による定義
SR  SR=S
©2016 PRINCIPIA Limited
＝ 仕様が拒否しないものは
必ず発生する
直感的にいうと， R の振る舞いは S に含まれているので
非決定的に結合すると S と区別できないということ
M[P  Q ] = M[P ]  M[P ],     A   = 
29
同値性・段階的詳細化・単調性
CSP が持つよい性質
プロセスの同値性
P =Q  P Q  Q P
反対称律
詳細化関係から同値性を導くことができる
段階的詳細化
P0  P1  P1  P2  ...  PN1  PN  P0  PN
仕様から実装へ段階的に詳細化することができる
推移律
cf. B-method
構成要素の交換
P  P   C[P ]  C[P ]
単調性
 S  C[P ]  S  C[P ]
推移律
C[P ] は P を含む任意のプロセス式

システムの一部であるプロセス P を，詳細化関係を満たすプロセス P で置き換えた
システムは，元のシステムの詳細化になる．したがって元のシステムが仕様を満たし
ていれば，置き換え後のシステムも自動的に仕様を満たす．
©2016 PRINCIPIA Limited
30
並行システムの開発基盤
システムの認識
システムをどのようなものだと認
識するか
システムの記述
仕様と実装をどのように記述する
か（振る舞いについて）
記述の意味
記述が意味することをどのように
厳密に定めるか
正当性の条件
実装が仕様を満たしているという
条件は何か
検証の方法
正当性を検証する方法にはどのよ
うなものがあるか
©2016 PRINCIPIA Limited
計算と相互作用
継続的に相互作用を行う状態遷移システム
CSP の構文：
イベント同期，チャネル送受信，選択，非決定的選択，
並行合成，隠蔽，逐次合成，改名
表示的意味論：トレース意味論，安定失敗意味論，
発散失敗意味論
操作的意味論
代数的意味論
安全性 (safety)
S T R  traces(R)  traces(S)
活性 (liveness)
S F R  S T R  failures(R)  failures(S)
詳細化検査（モデル検査）← 操作＋表示
模倣 ← 操作，代数
CSP-Prover 不動点帰納法 ← 表示＋代数
31
詳細化検査（モデル検査）
仕様を表すプロセスと実装を表すプロセスをともに操作的意味論に
よって状態遷移システムに変換し，その上で表示を計算して比較する
ことで詳細化関係を満たすかどうか検査する方法．
仕様
実装
S  E(S)
R  F(R)
cf. 時相論理によるモデル検査
操作的意味論
M
“ 仕様”に相当する
のは時相論理式
表示導出
M[S ]
S M R
?
比較
©2016 PRINCIPIA Limited
M[R ]
実装の遷移系が
Kripke 構造になる
（“モデル”検査）
詳細化検査では仕様も実装もプロセスで記述する
32
並行システムの設計支援ツール SyncStitch
プロセスのモデル化
分析
検査
●
●
●
●
トレース意味論
安定失敗意味論
デッドロック検査
発散検査
仕様
振る舞いが異なる状態とそこに至る
パスを発見してくれる
実装
©2016 PRINCIPIA Limited
分析ツール
33
検査例：生産者・消費者問題
実装
仕様
Producer 0
Producer 1
Consumer 0
Producer 1
Consumer 1
Producer 2
Consumer 2
Consumer 0
Queue
Consumer 1
Producer 2
Producer 3
Producer 0
Consumer 2
=F
putp
ピンポイントの性質ではなく
振る舞い全体について検査できる
Mutex + Condvar x 2
count
Buffer
条件変数と
リングバッファ
による解
getp
各プロセスはモックやスタブなしに単独で
分析できる（イベント同期型相互作用）
仕様は全体 / 部分，抽象 / 具象
など目的に応じて記述する
モデルを対話的に修正し検査する
ことで，さまざまな設計を短時間
で確実に試行できる．
有限のモデルしか検査できない
©2016 PRINCIPIA Limited
プロセスの振る舞いを
計算木としてみるビュー
34
操作的意味論と模倣による安全性検査
模倣（ simulation ）
a
p が持つ任意の遷移に対応する遷移を q も持つ
p
a
q
q
p
b
u
(p, q)  S  p u. pIp
u
 q. qIq  (p, q)  S
b
弱模倣（ weak simulation ）
内部イベントを無視する模倣
弱模倣はトレース集合の包含関係を含意する（安全性）
S. (p, q)  S  traces(p)  traces(q)
datatype Event0 = eva
datatype PN0 = S0 | C0 nat
弱模倣による安全性検査
仕様と実装の状態の対応関係を作り，
それが弱模倣であることを操作的意味
論で証明する
©2016 PRINCIPIA Limited
Isabelle による例
fun D0 :: "PN0 => (PN0, Event0) proc" where
"D0 S0 = eva -> $S0" |
"D0 (C0 n) = eva -> $(C0 (Suc n))"
definition R0 :: "((PN0, Event0) proc * (PN0, Event0) proc) set" where
"R0 = {(P, Q).
(EX n. P = $(C0 n) & Q = $S0) |
(EX n. P = eva -> $(C0 (Suc n)) & Q = $S0)
}"
lemma "wsim D0 R0"
...
done
S  aS
Rn  a  Rn+1
35
代数的意味論による同値性証明
プロセスの標準形（ head-normal-form ）
 ?x :A
i
iI
coinductive な再帰プロセスの同値性定義
i
 i = hnf(I, Ai, i)
p =R q  gfp F
双模倣（ bisimulation ）
F(X) = {(p, q) | p = hnf(I, Ai, pi)  q = hnf(I, Ai, qi)  i xi  Ai. (pi, qi)  X}
coinduction による同値性証明
詳細化関係の証明
再帰的に定義されたプロセス
P  G(P )
S R R  S  R = R S
Q  H(Q)
例
coinduction 推論規則（簡略形）
(P, Q)  X  (P, Q)  F (X)
P =R Q
©2016 PRINCIPIA Limited
単調関数
P  e  P, Q  e  e  Q
(P, Q)  F(X)  (P, e  Q)  F(X)
= (e  P, e  e  Q)  F(X)  (e  P, e  Q)  F(X)
 (P, e  Q)  X  (P, Q)  X
 P =R Q
36
CSP-Prover
●
定理証明支援系 Isabelle の上に CSP の理論を構築した並行
システムのための証明フレームワーク
–
完備半順序（ CPO ），完備距離空間（ CMS ），不動点定理
–
表示的意味論（トレース，安定失敗）
–
表示的意味論によって証明された代数規則群
–
証明のための補題群および tactic
–
デッドロックフリー証明パッケージ
–
表示的意味論と代数的意味論の等価性証明
–
Isabelle 理論ファイル約 78,500 行
©2016 PRINCIPIA Limited
37
検証例：シーケンサとイベントカウントによる
排他制御の安全性（状態数無限の例）
シーケンサ
イベントカウント
利用者
T(n)  ticket ! n  T(n + 1)
状態数は無限
E(n)  await ? m : {m | n  m}  E(n)  advance  E(n + 1)
C  ticket ? m  await ! m  advance  C
並行合成
R  ((C ||| C) || (T(0) ||| E(0))) \ Z
この間で仕事をしている
X
X  range await  range ticket  {advance}
利用者は 2 人
Z  range ticket
仕様（安全性）
S  await ? m  advance  S
C0
C1
await と advance は必ず交互に発生する
await
advance
ticket
安全性検証
©2016 PRINCIPIA Limited
S T R
?
n
En
38
検証例：シーケンサとイベントカウントによる
排他制御の安全性（状態数無限の例）
theory Sequencer imports CSP_T begin
CSP-Prover のライブラリを指定
datatype Event = ticket nat | await nat | advance
イベント定義
datatype PNSpec = S
primrec PNfunSpec :: "PNSpec => (PNSpec, Event) proc" where
"PNfunSpec S = await ? v -> advance -> $S" 仕様定義
datatype PNImpl = C | T nat | E nat
実装側プロセスインデックス定義
primrec PNfunImpl :: "PNImpl => (PNImpl, Event) proc" where
"PNfunImpl C = ticket ? turn -> await ! turn -> advance -> $C" |
"PNfunImpl (T n) = ticket ! n -> $(T (Suc n))" |
"PNfunImpl (E n) = await ? m:{m. n >= m} -> $(E n)
[+] advance -> $(E (Suc n))"
各コンポーネントプロセス定義
©2016 PRINCIPIA Limited
39
検証例：シーケンサとイベントカウントによる
排他制御の安全性（状態数無限の例）
primrec Spec_Impl :: "PNSpec => (PNImpl, Event) proc" where
"Spec_Impl S =
!nat n .. ((($C ||| $C) |[insert advance (range ticket Un range await)]|
($(T n) ||| $(E n))) -- (range ticket))"
仕様と実装の対応関係
consts
Spec :: "(PNSpec, Event) proc"
Impl :: "(PNImpl, Event) proc"
defs
実装の並行合成はここに記述
初期状態
Spec_def : "Spec == $S"
Impl_def : "Impl == (($C ||| $C) |[insert advance (range ticket Un range await)]|
($(T 0) ||| $(E 0))) -- (range ticket)"
lemma guardedfun_ex[simp]: プロセス定義が構成的であることの証明
"guardedfun PNfunSpec"
"guardedfun PNfunImpl"
apply(simp add: guardedfun_def, rule allI, induct_tac p, simp)+
apply(simp)
apply(simp)
done
©2016 PRINCIPIA Limited
40
不動点帰納法
仕様
完備距離空間を利用する場合
実装
S  E(S)
R  F(R)
R = lfp F = inf {X | F(X)  X }
S  R = R  S  F(S)  S
※ プロセスと表示を同一視して同じ文字で表している
例
S  a  S  b  S, R  a  R ||| b  R
F(S)  S
S = gfp E = sup {X | X  F(X) }
S  R = R  S  R  E(R)
例
F(R)
= a  S ||| b  S  S
R が消えるので，あとは代数規則で証明できる
©2016 PRINCIPIA Limited
発散していないプロセス（構成的なプ
ロセス）の場合は唯一の不動点を持つ
ので， lfp と gfp が一致する．そのため
不動点帰納法を逆向きにも使うことが
できる
R  E(R)
= R  aR  bR
41
検証例：シーケンサとイベントカウントによる
排他制御の安全性（状態数無限の例）
lemma
apply
apply
apply
apply
apply
apply
apply
apply
詳細化関係の証明
"Spec <=T Impl"
(simp add: Spec_def Impl_def)
(rule cspT_fp_induct_left[of _ "Spec_Impl"])
不動点帰納法の適用
(simp)+
(rule cspT_Rep_int_choice_left)
(rule_tac x="0" in exI)
(clarsimp)
goal (1 subgoal):
不動点帰納法の適用前のゴール
(induct_tac p)
1. $S <=T
(simp)+
($C ||| $C
|[insert advance
(range ticket Un
range await)]| ($T 0 ||| $E 0))
-- range ticket
goal (1 subgoal):
1. await ? v
-> advance
不動点帰納法の適用後のゴール
-> (!nat n ..
($C ||| $C
実装側のプロセスのみなので，あとは代数規則で証明できる
|[insert advance
(range ticket Un range await)]| ($T n ||| $E n))
-- range ticket)
<=T !nat n ..
($C ||| $C
|[insert advance (range ticket Un range await)]| ($T n ||| $E n))
-- range
ticket
©2016 PRINCIPIA
Limited
42
並行システムの開発基盤
システムの認識
システムをどのようなものだと認
識するか
システムの記述
仕様と実装をどのように記述する
か（振る舞いについて）
記述の意味
記述が意味することをどのように
厳密に定めるか
正当性の条件
実装が仕様を満たしているという
条件は何か
検証の方法
正当性を検証する方法にはどのよ
うなものがあるか
©2016 PRINCIPIA Limited
計算と相互作用
継続的に相互作用を行う状態遷移システム
CSP の構文：
イベント同期，チャネル送受信，選択，非決定的選択，
並行合成，隠蔽，逐次合成，改名
表示的意味論：トレース意味論，安定失敗意味論，
発散失敗意味論
操作的意味論
代数的意味論
安全性 (safety)
S T R  traces(R)  traces(S)
活性 (liveness)
S F R  S T R  failures(R)  failures(S)
詳細化検査（モデル検査）← 操作＋表示
模倣 ← 操作，代数
CSP-Prover 不動点帰納法 ← 表示＋代数
43
計算システムの開発基盤
システムの認識
システムをどのようなものだと認
識するか
システムの記述
仕様と実装をどのように記述する
か（振る舞いについて）
記述の意味
記述が意味することをどのように
厳密に定めるか
正当性の条件
計算
入出力の関係
仕様：数学による関係表現，事前・事後条件
実装：プログラミング言語
表示的意味論：プログラム→入出力の関係
包含関係は実装を容易に
操作的意味論
するためのゆとり (opt.)
公理的意味論： Hoare 論理
  R  dom   dom R
実装が仕様を満たしているという
仕様
条件は何か
検証の方法
正当性を検証する方法にはどのよ
うなものがあるか
©2016 PRINCIPIA Limited
対比として
実装
 dom   R  S
仕様が規定する範囲の
入力は受理できること
出力は仕様が規定する
範囲から選ぶこと
表示に基づくテスト，正当性条件の証明
Hoare 論理
定義域制限演算子
包含関係は
非決定性の減少
A  R  {(x, y) | x  A  (x, y)  R}
44
まとめ
●
●
●
●
リアクティブシステムは環境との相互作用と計算を継続的
に行う状態遷移システムである
並行システムは階層的に構成されたリアクティブシステム
である．実行主体であるリアクティブシステム群が相互作
用を行いながら協調し，全体として目的の仕事を行う
CSP は並行システムを記述・論証するための理論であり，
並行システム開発のための基盤を提供する
CSP に基づいて並行システムの検証を行うツールがある
–
詳細化検査（モデル検査）
–
詳細化関係の証明
©2016 PRINCIPIA Limited
45
参考文献とツール
●
参考文献
–
磯部祥尚，並行システムの検証と実装
●
–
A. W. Roscoe, The Theory and Practice of Concurrency
●
–
http://www.computing.surrey.ac.uk/personal/st/S.Schneider/books/CRTS.pdf
田辺誠，中島玲二，長谷川真人，コンピュータサイエンス入門 <2> 論理とプログラム意味論
●
●
http://www.cs.ox.ac.uk/ucs/
Steve Schneider, Concurrent and Real Time Systems: the CSP approach
●
–
http://www.usingcsp.com/
A. W. Roscoe, Understanding Concurrent Systems
●
–
http://www.cs.ox.ac.uk/people/bill.roscoe/publications/68b.pdf
C. A. R. Hoare, Communicating Sequential Processes (CSP)
●
–
https://staff.aist.go.jp/y-isobe/topse/vic/
https://www.iwanami.co.jp/.BOOKS/00/9/0061900.html
ツール
–
SyncStitch
●
–
CSP-Prover
●
–
http://www.principia-m.com/jp/syncstitch/
https://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html
Isabelle
●
https://isabelle.in.tum.de/
©2016 PRINCIPIA Limited
46

iWallet | 組合員証

平成28年熊本地震における被災者・被災地の支援について

PDF:217KB

Ⅱ 学校設定科目 Principia(プリンキピア)Ⅰ・Ⅱ・Ⅲの設置