リアルタイムシステム検査ツール『ＵＰＰＡＡＬ』

リアルタイムシステム検査ツール タイミングが原因の動作の不具合は、設計レベルではなかなか検査が困難です。 UPPAAL を利用したモデル検査を行うことによって、そのような時間的な制約を含むシス テムの挙動をモデル化し、検査することが可能です。 ■グラフィカルなエディタによるモデル作成 軽快に動作するグラフィカルエディタは使い勝手が良い。 ■時間制約付きモデル検査 「時間オートマトン」モデルによる時間制約の検査が可能。 ■ヴィジュアルなシミュレータ 動的に生成されるシーケンス図によるわかりやすい表示。 こんな方にオススメ 期待される効果 ・振る舞い設計を検証し実装時の不具合を減らしたい。 ・設計時のミスを減らすことで品質が向上します。 ・使いやすいモデル検査ツールが欲しい。 ・習得時間が短いため、作業コストを削減します。 ・時間制約を記述したモデルを定義し、検証したい。 ・タイミング制約が検査できます。 作業の流れ 1 モデル作成 2 妥当性検証 3 形式検証 4 高品質設計書 設計書からグラフィカルなモ シミュレーション実行すること モデル検査機能によって網羅 元の設計書が「形式検証」さ デルを作成することで設計を でモデルの妥当性を確認しま 的な検査を行います。 れたので、高品質な設計書と 視覚的に確認できます。 す。 問題があれば修正します。 なります。 関連サービス ・お手持ちの設計書から検査モデルを作成支援作業をお手伝いします。 ・本ツールを利用するような研究を支援します（コンサル、モデル作成、プロトタイプ開発）。 ・すでに使用中の設計ツールの保存形式をUPPAAL へ変換するツールを受託開発します。 キャッツ株式会社

UPPAAL の機能紹介 「形式手法」は機能安全規格などでその利用を推奨されるなど、ソフトウェアの品 質の確保のための技術として注目されています。UPPAAL によるモデル検査を 実施することで、通常は実装後でないと確認が難しいリアルタイムシステムの不具 合を設計の段階で可能な限り排除できます。 使いやすい検査モデルエディタ UPPAAL のモデルエディタの使い勝手は洗練されており、非常に 軽く動作します。ビジュアルなモデル表現を利用することにより高度 な数学的理論（時間オートマトン）を背景に持つにもかかわらず、簡 単にモデリング作業が進められます。 高機能なシミュレーション機能 UPPAAL のシミュレーション機能は、作成したモデルの妥当性をチェックしま す。また、モデル検査結果としてエラーが検出された場合に、そのエラーへ至 るまでのトレース情報が分析可能です。 ・モデルインスタンスのアニメーション モデルエディタで定義したテンプレートのインスタンス表示として、シミュ レーション中にアクティブな状態を赤色で表示します。 ・動的なシーケンス図によるトレース シミュレーションの進行とともにシーケンス図が動的に生成されます。 ・ステップ毎の変数内容確認 ちょうどビジュアルなデバッガのように、適当に選ばれたトレースの途中ス テップでの変数内容を確認できます。 モデル検査機能 ・検証式管理画面 リストから検証式を選択して検証できます。長時間かかる処理のた めに、処理中は状況が表示されています。 ・反例解析はシミュレーションと連動 モデル検査の結果がエラーだった場合、初期状態からエラーに至る までのトレースを分析（いわゆる「反例解析」）するために、結果がシ ミュレーション画面と連動しえいます。 ・高度なオプション 現在検査しようとしているモデルに最適なモデル検査アルゴリズム の方式やデータ構造を選択することができます（要専門知識）。 〒222-0033 神奈川県横浜市港北区新横浜3-1-9 アリーナタワー TEL：045-473-2816 詳細はinfo@zipc.comまでお問い合わせください。http://www.zipc.com/ キャッツ株式会社 ・本資料の内容は、予告なしに変更する場合があります。 ・本資料に掲載された社名、製品名は各社の商標または登録商標です。 201902 ▼