CSP記述によるモデル設計と ツールによる検証 数理情報科学専攻　福永研究室 坂本 達哉

目次 研究背景と意義 今回の研究で触れたツールの紹介 ツールによる論理的設計と検証 CSP記述 FDR2 UPPAAL 割り込みルータシステム

システムとは 個々の要素が有機的に組み合わされた、まとまりをもつ全体、体系 ここではある入力を元に演算を行い、 結果を出力する主体とする ex. プログラム

並列処理システムとは 複数のシステムが互いに連携しながら、 全体として一つのシステムを 成立させているもの システム1 システム2 　　初期値を入力 　　演算 　　システム2に演算結果を出力 　　システム1から初期値を入力 　　演算 　　演算 　　システム2から演算結果を入力 　　システム1に演算結果を出力 　　演算 　　演算結果を出力

deadlockとは 並列処理システム全体が連携の不具合 によって停止してしまった状態 設計の段階で排除されなければならない × システム1 システム2 　　初期値を入力 　　演算 　　システム2に演算結果を出力 　　システム1から初期値を入力 　　演算 　　演算 　　システム2に演算結果を出力 　　システム1に演算結果を出力 　　演算 　　演算結果を出力 × deadlock

リアルタイムシステムとは 各プロセスごとに時間的制約があるもの システムの連携関係だけでなく、時間経過も念頭に置いて設計しなければならない

TPCOREとは 当研究室では並列処理に対応したCPUプロセッサ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. 同期通信

UPPAAL検証画面 実際に描画したシステム この直後可能な選択を列挙したもの この時点での時間を含む各変数の値 検証成功例の経路とそれを図示したもの

割り込みルータシステムの設計 CSP記述、FDR2、UPPAALを総合的に応用する方法として、実際に与えられた要件を満たすTPCOREに実装可能な並列処理 リアルタイムシステムを開発、検証した 実装をする前に設計の段階でシステム全体の並列処理の正当性や、 時間的制約の成立性を証明しようとしたことが新しい試み

割り込みルータシステム 60本のシグナルがそれぞれ 数百～数千μs周期で発生する ルータはこのシグナルを統合管理して 上位モジュールへと伝達する 一つのCPUプロセッサに60本全てを処理させるのは負担が大きいので、少ない本数ずつ複数のプロセッサに並列で処理させる

ROUTER1イメージ図 結局最上位モジュールに過度の負担がかかる 60本の端子からシグナルが入力される これら一つ一つのモジュールに 一つのTPCOREを対応させる 要求される処理速度：5.1μs TPCOREの処理速度：22μs　　（シグナル1本あたり）

ROUTER2イメージ図 出力端子も複数にすることで 上位モジュールの負担減 与えられた要件を満たす範囲内で適当にグルーピング 要求される処理速度：95μs TPCOREの処理速度：22μs　　（シグナル1本あたり）

CSP記述による設計

FDR2による検証結果

研究結果 CSP記述によるモデル設計、その正当性を支えるFDR2、UPPAALといったツールを使ってのシステム構築に成功 設計段階でシステムの正当性が 保証される一例を示せた CSP記述に時間的制約を加えた Timed CSPによって、 さらに精度の高い検証が期待される