形式手法に基づく CONPASU 並行処理可視化ツールの紹介 ~CSP モデルベース開発のすすめ ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部 ET2012 展示会場内 IPA 出展ブースプレゼンテーション 2012 年 11 月 15 日 この資料の一部またはすべての内容について 作成者の許可なき使用 複製 配布を固くお断りします 1
目次 はじめに 背景 目標 pp.5-11 CONPASUツールの特徴 並行システムの解析例 協調動作の可視化 モデル検査との違い pp.12-16 CONPASUの適用 既存ツールとの連携 CSPモデルベース設計工程 おわりに まとめ 今後の課題 2
背景 並行システム : 協調する複数の処理 ( プロセス ) から構成されるシステム 並行システムの例 ( 昇降舵のフライバイワイヤ ) 操縦桿 x2 角度 x3x2 ジャイロ x3 重量計 x4 フラップ LVDT IRU WOW FSACE PB 優先ボタン x2 MON モニタ COM コマンド 協調 フライト制御 x4 アクチュエータ x4 ACE, PCU センサプロセッサアクチュエータ ( エンブラエル社レガシー ) なぜ並行システム? センサに対する応答性 故障時に対する冗長性 制御情報の通信 ( 共有 ) 背景 : ネットワークやマルチコアの普及によって 並行処理が身近になっている 課題 : 全体で正しく並行処理するように 個々のプロセスを設計するのは難しい 3
目標 目標 : 設計モデルの協調動作を理論的に解析するツール CONPASU の開発 効果 : 信頼性の向上 手戻りコストの削減 解析結果 設計レビュー支援 解析 フィードバック 並行システムのモデル 要求分析 設計 手戻りコスト削減 受入テスト 結合テスト CONPASU-tool SQ REM SUM 実装 単体テスト 4
CONPASU ツールの特徴 並行システムの解析例 協調動作の可視化 モデル検査との違い 5
並行システムの解析例 並行システム全体の動作を把握するのは難しいので? upload cancel complete UI input ok ng quit0 succ Sender start net term quit1 ack Receiver output 構造 UI Sender 振舞い Receiver 通信 通信 6
並行システムの解析例 並行システム全体の動作の可視化するツール CONPASU [1] を開発中! CONPASU-tool upload cancel complete 入力 : 並行システムの構造 各プロセスの振舞い UI UI input ok ng quit0 succ Sender Sender start net term quit1 Receiver τ[#ds0>0] /ds0:=tail(ds0), ack ds1:=ds1^<head(ds0)> @(0(11)) Receiver output 構造 振舞い 出力 : 全体の振舞い 処理 : 並行合成 状態数削減 CONPASU( 産総研知財管理番号 :H24PRO-1409) 並行システム通信全体の振舞い 通信デッドロック 7
協調動作 ( 並行処理 ) の可視化 既存のツール ( 例 :PAT [10], LTSA [11] ) でも状態遷移図を表示できる 入力値は具体化されるため状態数が多くなる CONPASU パイプライン並列計算の例 in.1 in.0 PAT in?x1 SQ REM SUM LTSA 状態数 : 8 遷移数 : 12 状態数 : 105 遷移数 : 160 入力値 : 無制限入力回数 : 任意 状態数 : 42 遷移数 : 67 入力値 :{0,1} 入力回数 :3 8
状態遷移図の抽象化 CONPASU では興味のあるイベントに着目した状態数の削減が可能 状態数 : 3 遷移数 : 3 CONPASU CONPASU-tool 途中結果の表示を隠蔽 状態数 : 8 遷移数 : 12 in?x1 [n>0] / y:=y+(x1*x1)%10,n:=n-1 @ ((11)1) SQ REM SUM ( 計算式が見える!) 9
計算過程の可視化 CONPASU では任意の入力値に対する計算過程 ( 計算式 ) を確認できる in?x1 状態数 : 3 遷移数 : 3 状態数 : 105 遷移数 : 160 in.1 in.0 比較 in.1 式 CONAPSU 入力値 : 無制限入力回数 : 任意 入力値 :{0,1} 入力回数 :3 prts.2 10 PAT 値
モデル検査との違い CONPASU では検証用の性質 ( 時相論理式など ) を記述する必要がない 性質 ( 逐次動作 ) は CONPASU が抽出する 両ツールを併用すると効果的 in の後にいつか ack が起きる? この性質を記述 in ack 並行システムの設計モデル Snd c1 Rcv out Ack c2 性質 ( 時相論理 ) (in ack) 逐次動作 in in in in c1 c2 ack c1 out ack ack ack c2 in と ack の関係は? in と ack を選択 11
CONPASU の適用 既存ツールとの連携 CSP モデルベース設計工程 12
既存のモデル / ツールとの連携 CONPASU は形式手法 CSP* 1[2,3] に基づく解析ツール CONPASU の入力言語には形式言語 CSP M * 2 を採用 ( 例 : モデル検査器 FDR と連携して UML モデルを解析可能 ) FDR モデル検査器 [8] ( オクスフォード大学 ) UML Activity UML State M. 変換器 UML CSP M ( サリー大学 [7] ) 変換器 SimuLink CSP M 状態遷移図 意味論 Snd = in -> c1 -> Snd Rcs = c1 -> out -> c2 -> Rcv Ack = Sys = ((Snd Ack) [ ]Rcv) \{ } ProB モデル検査器 [9] デュッセルドルフ大学 サウサンプトン大学 MATLAB/Simulink ペルナンブコ連邦大学 エンブラエル社 [6] CSP M 言語 CONPASU * 1 CSP : 並行システムを記述し 解析するための理論 ( プロセス代数 ) * 2 CSP M : CSP の代表的なモデル検査器 FDR の入力言語 ( 関連研究が多い ) モデル解析器 [1] ( 産総研 ) 13
形式手法 CSP CSP モデルは同期型メッセージパッシング通信を採用 協調部 ( 並行処理 ) とデータ部を分割して設計しやすい プロセス チャネル in?x f x, y, z = x + y z C UI in x z CNTL back out y back?z y:=f(x,y,z) out!y 協調部 ( 振舞い ) データ部 ( 関数 ) 協調部 ( 構造 ) 共有メモリ通信よりも並行処理がわかりやすい 設計ミスの削減 CSP の解析ツールによって効果的に解析できる 設計ミスの検出 設計工程を階層的に分割しやすい 役割分担の明確化 14
CSP による組込みシステム開発事例 農水産物加工向け全周 3 次元形状計測システム ( 株式会社ニッコー, 産業技術総合研究所 ) ステレオカメラを用いて 農水産物の全周 3 次元形状を高速 高精度に計測するシステム http://www.aist.go.jp/aist_j/press_release/pr2011/pr20110606/pr20110606.html 開発初期 並列処理を共有メモリ通信で設計して試作 計測結果が正しくない誤動作が低い確率で発生 ( 再現性がないため 誤動作の原因究明は困難 ) この問題を解消するため 並列処理を CSP で設計し直し モデル検査器で検証してから実装 高信頼 高速な並列処理を実現 マルチスレッドによる高速処理 UI 画像入力 制御 画像処理画像処理画像処理 設計検証実装 並列 SW の CSP モデル CSP モデル検査器 プログラム (CSP ライブラリ ) 修正 CSP モデルを用いた並列ソフトウェアの開発 全周 3 次元形状計測システム概観 15
CSP モデルベースの設計工程 CSP では協調部 ( 並行処理 ) とデータ部を分割して設計 解析しやすい 概念モデル 間違えやすい協調部は網羅的解析 (CONPASU に実装中 ) 設計工程 網羅的解析 解析工程 協調部 データ部 構造図 ( コンポーネント図 ) 振舞い図 ( ステートマシン図 ) 協調部 データ部 ( 関数定義等 ) int fact(n){... } 解析済の CSP モデル シミュレーション 状態数の多いデータ部はシミュレーション解析 (CONAPSU に実装予定 ) 16
おわりに まとめ 今後の課題 17
まとめ CONPASU 研究のポイント ネットワークやマルチコアの普及によって 並行処理が身近になっている 複雑な並行処理の全体像を解析して 簡潔に可視化するツールを開発 並行処理も解析可能で 既存の開発工程への導入が容易 信頼性の向上 手戻りコストの削減 モデルベース開発工程への導入 CSP モデルベース開発工程の採用 解析モデル 要求分析 設計モデル 手戻りコスト削減 受入テスト 結合テスト 解析 CSP/UML 要求分析 設計 CSP/UML 解析 CSP (CONPASU) 実装 単体テスト (CONPASU) 並行処理の明確化 検証効率の向上 実装 18
今後の課題 解析結果のフィードバック方法 見やすい解析結果の表示方法 解析結果ともとのモデルとの対応表示方法 他 設計モデル 解析結果 解析 フィードバック 解析能力の向上 さらなる状態数削減方法の研究 19
補足 :CONPASU の仕組み 記号処理 20
CONPASU の機能 CONPASU は並行処理の全体像を解析して可視化するツール 逐次化機能 : 並行処理を記号的意味論によって逐次処理に展開する機能 状態数削減機能 : 振舞いの等しさを保ったまま状態数を減らす機能 状態数 : 8 状態数削減 (CONPASU) CONPASU 並行システムの設計モデル 状態数 : 4 in c1 c2 out B0 B1 B2 in c1 c1 c2 c2 out 逐次化 (CONPASU) 容量 3 のバッファ 21
記号的意味論 プロセス代数の記号的意味論 [4,5] は 1995 年頃から研究が行われている CSP モデル Proc = in?x out!(x 2) ack Proc ( 普通の ) 意味論記号的意味論 入力値 x {0,, 9} 値 変数 in.0 in.1 in.2 in.9 out.0 out.2 out.4 out.18 ack in?x out!(x 2) ack 状態数の増加を抑えられる 解析 ( 等価性判定など ) は難しい 振舞いを変えずに 変数を含む状態遷移図の状態数を削減する方法を考案 22
並行システムの解析例 並行システム全体の動作の可視化するツール CONPASU を開発中! upload cancel 普通の意味論で状態遷移図 UI を作成した場合 complete (FDR 使用 ) 状態数 : 約 12 万 CONPASU-tool UI データ種類 :4 種類入力 : 転送回数 :4 回 並行システムの構造 各プロセスの振舞い input ok ng quit0 succ Sender Sender start net term 状態数 Receiver : 8 quit1 ack Receiver output 構造 振舞い 出力 : 全体の振舞い 処理 : 並行合成 状態数削減 通信 通信 23
参考文献 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/ 24