形式手法に基づく CONPASU 並行処理可視化ツールの紹介 ~CSP モデルベース開発のすすめ ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部 ET2012 展示会場内 IPA 出

Size: px

Start display at page:

Download "形式手法に基づく CONPASU 並行処理可視化ツールの紹介 ~CSP モデルベース開発のすすめ ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部 ET2012 展示会場内 IPA 出"

みりあやすこ
4 years ago
Views:

1 形式手法に基づく CONPASU 並行処理可視化ツールの紹介 ~CSP モデルベース開発のすすめ ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部 ET2012 展示会場内 IPA 出展ブースプレゼンテーション 2012 年 11 月 15 日この資料の一部またはすべての内容について作成者の許可なき使用複製配布を固くお断りします 1

2 目次はじめに背景目標 pp.5-11 CONPASUツールの特徴並行システムの解析例協調動作の可視化モデル検査との違い pp CONPASUの適用既存ツールとの連携 CSPモデルベース設計工程おわりにまとめ今後の課題 2

3 背景並行システム : 協調する複数の処理 ( プロセス ) から構成されるシステム並行システムの例 ( 昇降舵のフライバイワイヤ ) 操縦桿 x2 角度 x3x2 ジャイロ x3 重量計 x4 フラップ LVDT IRU WOW FSACE PB 優先ボタン x2 MON モニタ COM コマンド協調フライト制御 x4 アクチュエータ x4 ACE, PCU センサプロセッサアクチュエータ ( エンブラエル社レガシー ) なぜ並行システム? センサに対する応答性故障時に対する冗長性制御情報の通信 ( 共有 ) 背景 : ネットワークやマルチコアの普及によって並行処理が身近になっている課題 : 全体で正しく並行処理するように個々のプロセスを設計するのは難しい 3

4 目標目標 : 設計モデルの協調動作を理論的に解析するツール CONPASU の開発効果 : 信頼性の向上手戻りコストの削減解析結果設計レビュー支援解析フィードバック並行システムのモデル要求分析設計手戻りコスト削減受入テスト結合テスト CONPASU-tool SQ REM SUM 実装単体テスト 4

5 CONPASU ツールの特徴並行システムの解析例協調動作の可視化モデル検査との違い 5

6 並行システムの解析例並行システム全体の動作を把握するのは難しいので? upload cancel complete UI input ok ng quit0 succ Sender start net term quit1 ack Receiver output 構造 UI Sender 振舞い Receiver 通信通信 6

並行システムの解析例並行システム全体の動作の可視化するツール CONPASU [1] を開発中!

各プロセスの振舞い UI UI input ok ng quit0 succ Sender Sender start

ds1:=ds1^<head(ds0)> @(0(11)) Receiver output 構造振舞い出力 :

7 並行システムの解析例並行システム全体の動作の可視化するツール 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 Receiver output 構造振舞い出力 : 全体の振舞い処理 : 並行合成状態数削減 CONPASU( 産総研知財管理番号 :H24PRO-1409) 並行システム通信全体の振舞い通信デッドロック 7

8 協調動作 ( 並行処理 ) の可視化既存のツール ( 例 :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

9 状態遷移図の抽象化 CONPASU では興味のあるイベントに着目した状態数の削減が可能状態数 : 3 遷移数 : 3 CONPASU CONPASU-tool 途中結果の表示を隠蔽状態数 : 8 遷移数 : 12 in?x1 [n>0] / ((11)1) SQ REM SUM ( 計算式が見える!) 9

10 計算過程の可視化 CONPASU では任意の入力値に対する計算過程 ( 計算式 ) を確認できる in?x1 状態数 : 3 遷移数 : 3 状態数 : 105 遷移数 : 160 in.1 in.0 比較 in.1 式 CONAPSU 入力値 : 無制限入力回数 : 任意入力値 :{0,1} 入力回数 :3 prts.2 10 PAT 値

この性質を記述 in ack 並行システムの設計モデル Snd c1 Rcv out Ack c2 性質 ( 時相論理 ) (in

11 モデル検査との違い 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

12 CONPASU の適用既存ツールとの連携 CSP モデルベース設計工程 12

$((Snd Ack) [ ]Rcv) \{ }$ ProB モデル検査器 [9]

13 既存のモデル / ツールとの連携 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 モデルは同期型メッセージパッシング通信を採用協調部 ( 並行処理

14 形式手法 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 次元形状計測システム (

15 CSP による組込みシステム開発事例農水産物加工向け全周 3 次元形状計測システム ( 株式会社ニッコー, 産業技術総合研究所 ) ステレオカメラを用いて農水産物の全周 3 次元形状を高速高精度に計測するシステム開発初期並列処理を共有メモリ通信で設計して試作計測結果が正しくない誤動作が低い確率で発生 ( 再現性がないため誤動作の原因究明は困難 ) この問題を解消するため並列処理を CSP で設計し直しモデル検査器で検証してから実装高信頼高速な並列処理を実現マルチスレッドによる高速処理 UI 画像入力制御画像処理画像処理画像処理設計検証実装並列 SW の CSP モデル CSP モデル検査器プログラム (CSP ライブラリ ) 修正 CSP モデルを用いた並列ソフトウェアの開発全周 3 次元形状計測システム概観 15

16 CSP モデルベースの設計工程 CSP では協調部 ( 並行処理 ) とデータ部を分割して設計解析しやすい概念モデル間違えやすい協調部は網羅的解析 (CONPASU に実装中 ) 設計工程網羅的解析解析工程協調部データ部構造図 ( コンポーネント図 ) 振舞い図 ( ステートマシン図 ) 協調部データ部 ( 関数定義等 ) int fact(n){... } 解析済の CSP モデルシミュレーション状態数の多いデータ部はシミュレーション解析 (CONAPSU に実装予定 ) 16

17 おわりにまとめ今後の課題 17

18 まとめ CONPASU 研究のポイントネットワークやマルチコアの普及によって並行処理が身近になっている複雑な並行処理の全体像を解析して簡潔に可視化するツールを開発並行処理も解析可能で既存の開発工程への導入が容易信頼性の向上手戻りコストの削減モデルベース開発工程への導入 CSP モデルベース開発工程の採用解析モデル要求分析設計モデル手戻りコスト削減受入テスト結合テスト解析 CSP/UML 要求分析設計 CSP/UML 解析 CSP (CONPASU) 実装単体テスト (CONPASU) 並行処理の明確化検証効率の向上実装 18

19 今後の課題解析結果のフィードバック方法見やすい解析結果の表示方法解析結果ともとのモデルとの対応表示方法他設計モデル解析結果解析フィードバック解析能力の向上さらなる状態数削減方法の研究 19

20 補足 :CONPASU の仕組み記号処理 20

21 CONPASU の機能 CONPASU は並行処理の全体像を解析して可視化するツール逐次化機能 : 並行処理を記号的意味論によって逐次処理に展開する機能状態数削減機能 : 振舞いの等しさを保ったまま状態数を減らす機能状態数 : 8 状態数削減 (CONPASU) CONPASU 並行システムの設計モデル状態数 : 4 in c1 c2 out B0 B1 B2 in c1 c1 c2 c2 out 逐次化 (CONPASU) 容量 3 のバッファ 21

22 記号的意味論プロセス代数の記号的意味論 [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

23 並行システムの解析例並行システム全体の動作の可視化するツール 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.

24 参考文献 1. (CONPASU)Y. Isobe, CONPASU-tool: A Concurrent Process Analysis Support Tool based on Symbolic Computation, CPA2011, WoTUG-33, IOS Press, pp , (CSP)C. A. R. Hoare, Communicating Sequential Processes, Prentice Hall, (CSP)A. W. Roscoe, The Theory and Practice of Concurrency, Prentice Hall, ( 記号的意味論 )Z. Li and H. Chen, Computing strong/weak bisimulation equivalences and observation congruence for value-passing processes, TACAS '99, LNCS 1579, Springer, pages , ( 記号的意味論 )M. Hennessy and H. Lin, Symbolic bisimulations, Theoretical Computer Science, Volume 138, Issue 2, pp , (Simulink-CSP)J. Jesus, A. Mota, A. Sampaio, and L. Grijo, Architectural Verification of Control Systems Using CSP, ICFEM 2011, LNCS 6991, Springer, pp , (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, (FDR)Formal Systems (Europe) Limited, Failures-divergence refinement: FDR2, 9. (ProB)Universität Düsseldorf and University of Southampton, The ProB Animator and Model Checker National University of Singapore, PAT: Process analysis toolkit Imperial College London, LTSA - labelled transition system analyser. 24

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

背景並行システム : 協調する複数の処理 ( プロセス ) から構成されるシステム並行システムの例 ( 昇降舵のフライバイワイヤ ) 操縦桿 x2 角度 x3x2 ジャイロ x3 重量計 x4 フラップ LVDT IRU WOW FSACE PB 優先ボタン x2 MON モニタ COM コマン並行システム解析支援ツール ~ 協調動作の可視化 ~ 磯部祥尚 * 1, 大岩寛 * 1, 高橋孝一 * 1, 田中純 * 2 産業技術総合研究所 * 1 セキュアシステム研究部門, * 2 イノベーション推進本部第 10 回クリティカルソフトウェアワークショップ 10 th WOCS 2 2012 年 9 月 28 日この資料の一部またはすべての内容について作成者の許可なき使用複製配布を固くお断りします