PPT

CSP記述によるモデル設計と
ツールによる検証
数理情報科学専攻福永研究室
坂本達哉
目次


研究背景と意義
今回の研究で触れたツールの紹介




CSP記述
FDR2
UPPAAL
ツールによる論理的設計と検証

割り込みルータシステム
システムとは



個々の要素が有機的に組み合わされた、
まとまりをもつ全体、体系
ここではある入力を元に演算を行い、
結果を出力する主体とする
ex. プログラム
並列処理システムとは

複数のシステムが互いに連携しながら、
全体として一つのシステムを
成立させているもの
システム1
初期値を入力
演算
システム2に演算結果を出力
演算
システム2から演算結果を入力
演算
演算結果を出力
システム2
システム1から初期値を入力
演算
システム1に演算結果を出力
deadlockとは


並列処理システム全体が連携の不具合
によって停止してしまった状態
設計の段階で排除されなければならない
システム1
初期値を入力
演算
システム2に演算結果を出力
演算
システム2に演算結果を出力
演算
演算結果を出力
システム2
×
システム1から初期値を入力
演算
システム1に演算結果を出力
deadlock
リアルタイムシステムとは


各プロセスごとに時間的制約があるもの
システムの連携関係だけでなく、時間経過
も念頭に置いて設計しなければならない
TPCOREとは



当研究室では並列処理に対応したCPU
プロセッサTPCOREを研究開発した
開発した並列処理システムは
TPCOREでの実装をねらっている
つまりTPCOREで実装可能な
（並列処理リアルタイム）システムを
設計しなければならない
研究の意義



並列処理システムは
複数のシステムが結びついているため、
全体としてのデバッグが困難である
そのためあらかじめシステムが正当性を
もつように設計することが重要になる
そのためにはシステムのモデリングを導入
して形式設計をする必要がある
CSP記述(Communicating
Sequential Process)


A.Hoare(1978)らによって
理論展開されたシステム論
理で、並列処理システムを
独特の文法で記述すること
ができる
連続運転されるシステムを、
イベントによるプロセスの
状態遷移としてとらえる
状態
イベント
CSP記述における文法の例
内部選択
プロセスの選
択権はプロセ
ス自身にある
外部選択
発生したイベント
によって選択が
決定する
並列処理
イベントで同期通信処理をとる
CSP記述における演算


状態遷移の可能性について
数学的演算による推論が可能
ex.全ての状態遷移の可能性が
否定された状態がdeadlockに相当する
FDR2(Failures Divergences
Refinement checker)




B.Roscoe(94)によって開発された
CSP記述に準拠した検証ソフトウェア
deadlock、livelock、determinismの有無、
refinementの関係にあるかどうかを
PC上でソフトウェア的に検証できる
入力： CSP記述に準拠したソースコード
出力： deadlockの可能性の有無など
FDR2検証画面
検証項目
今はdeadlockが選択
されている
検証結果
TEAMはdeadlock
の可能性があり、
TEAM’はdeadlock
の可能性がないこ
とが分かる
UPPAAL



Uppsala University groupと
Aalborg University group(95)により
協同開発された、システムの検証に
時間の概念を導入可能にしたソフトウェア
一つのイベントで経過する時間などを
入力設定する
ある状態への到達可能性や
到達までの経路、時間を網羅的に調査
UPPAALでの描画



CSP記述の概念図
をそのまま
描画する
他の多くのCSP記
述の概念もそのま
ま描画することが
できる
ex. 同期通信
CSP記述
の概念図
UPPAAL
での描画
UPPAAL検証画面
実際に描画したシステム
この直後可能
な選択を列挙
したもの
この時点での時
間を含む各変数
の値
検証成功例の経路と
それを図示したもの
割り込みルータシステムの設計


CSP記述、FDR2、UPPAALを総合的に応用
する方法として、実際に与えられた要件を
満たすTPCOREに実装可能な並列処理
リアルタイムシステムを開発、検証した
実装をする前に設計の段階でシステム全
体の並列処理の正当性や、
時間的制約の成立性を証明しようとしたこ
とが新しい試み
割り込みルータシステム



60本のシグナルがそれぞれ
数百～数千μs周期で発生する
ルータはこのシグナルを統合管理して
上位モジュールへと伝達する
一つのCPUプロセッサに60本全てを処理さ
せるのは負担が大きいので、少ない本数
ずつ複数のプロセッサに並列で処理させる
ROUTER1イメージ図
結局最上位モジュール
に過度の負担がかかる
60本の端子からシ
グナルが入力される
これら一つ一つの
モジュールに
一つのTPCOREを
対応させる
要求される処理速度：5.1μs
TPCOREの処理速度：22μs
（シグナル1本あたり）
ROUTER2イメージ図
出力端子も複数
にすることで
上位モジュール
の負担減
与えられた要件を満
たす範囲内で適当に
グルーピング
ROUTER2の方が
より実現性が高い
要求される処理速度：95μs
TPCOREの処理速度：22μs
（シグナル1本あたり）
CSP記述による設計
FDR2による検証結果
研究結果



CSP記述によるモデル設計、その正当性を
支えるFDR2、UPPAALといったツールを
使ってのシステム構築に成功
設計段階でシステムの正当性が
保証される一例を示せた
CSP記述に時間的制約を加えた
Timed CSPによって、
さらに精度の高い検証が期待される

Download Report