並行システム設計支援ツール 『PAT Pro』

PAT Pro 並行システム設計支援ツール 時代はマルチコアへ。 今後、ハードウェアを有効利用するためには並列処理をソフトウェ アを適切に設計し、実装する必要があります。しかし、並行処理システム(マルチタスク、マル チスレッドを含む）の安全な設計方法が確立されたとはまだ言えないのが現状です。そのよ うなマルチタスク・マルチスレッドのソフトウェアを設計段階で検査し、妥当性や安全性を確 保する必要があります。PAT Proを利用することで そのような設計環境を確保できます。 ■並行処理記述に適したモデル言語 PAT Pro のモデル記述言語は安全な並列処理設計のための モデル言語であるCSP（※）をベースにしています。 ■ヴィジュアルな統合環境 モデルエディタ、シミュレータ、モデル検査の機能がGUIによって 連携・統合された使いやすいモデル検査環境を提供します。 ※ CSP(Communicating Sequential Process)はHoareが提唱した「プロセス代数」モデルです。 こんな方にオススメ 期待される効果 ・振る舞い設計を検証し実装時の不具合を減らしたい。 ・設計時のミスを減らすことで品質が向上します。 ・使いやすいモデル検査ツールが欲しい。 ・習得時間が短いため、作業コストを削減します。 ・用途に合ったモデル言語を選択したい。 ・PAT Proでは複数の検査モデル言語が用意されています。 作業の流れ 1 モデル作成 2 妥当性検証 3 形式検証 4 高品質設計書 既存または新規のモデルを シミュレーション実行する事で モデル検査機能によって網羅 元の設計書が「形式検証」さ CSPによって記述する事で動 モデルの妥当性を確認します。 的な検査を行います。 れたので、高品質な設計書と 作を明確に定義します。 問題があれば修正します。 なります。 関連サービス ・お手持ちの設計書から検査モデルを作成支援作業をお手伝いします。 ・本ツールを利用するような研究を支援します（コンサル、モデル作成、プロトタイプ開発）。 ・すでに使用中の設計ツールの保存形式をPAT Proのデータへ変換するツールを受託開発します。 キャッツ株式会社

PAT Pro PAT Pro の機能紹介 PAT Proのベースとするモデル言語であるCSP は、並列処理設計手法として の長い歴史を持ちます。複雑になりがちな並行プロセスの設計をPAT Pro を利用 して検討することで、安全で見通しの良い並列設計を実現可能になります。 使いやすい検査モデルエディタ PAT Pro のモデルエディタは入力ワードの補完機能をは じめとして使い勝手が配慮されています。また、言語要素 が色付で表示されるため、モデルの構造が把握しやすく なっています。 高機能なシミュレーション機能 PAT Pro のシミュレーション機能は、作成したモデルの妥当性をチェックしま す。また、モデル検査結果としてエラーが検出された場合に、そのエラーへ至 るまでのトレース情報が分析可能です。 ・システム全体のトレース情報の可視化 CSPモデルとして定義された複数の並行プロセスモデルを合成した状態の 遷移トレースを動的に生成し、可視化します。 ・動的なシーケンス図によるトレース シミュレーションの進行とともにシーケンス図が動的に生成されます。 ・ステップ毎の変数内容確認 ちょうどビジュアルなデバッガのように、適当に選ばれたトレースの途中ス テップでの変数内容を確認できます。 モデル検査機能 ・反例解析はシミュレーションと連動 モデル検査の結果がエラーだった場合、初期状態からエラーに至る までのトレースを分析（いわゆる「反例解析」）するために、結果がシミュ レーション画面と連動しています。 ・便利な検査用キーワードの提供 典型的な検査式が書きやすいように、「デッドロックしない」、「到達 性」、「発散しない」,「決定的である」など表現するキーワードが用意さ れています。 ・「CSP流儀」の検査式の利用 伝統的なCSPを利用した検証項目である、「詳細化関係」を検査で きます。これにより、抽象度の異なる２つのプロセスの関係を評価する ことができます。 〒222-0033 神奈川県横浜市港北区新横浜3-1-9 アリーナタワー TEL：045-473-2816 詳細はinfo@zipc.comまでお問い合わせください。http://www.zipc.com/ キャッツ株式会社 ・本資料の内容は、予告なしに変更する場合があります。 ・本資料に掲載された社名、製品名は各社の商標または登録商標です。 201902 ▼