株式会社NTTデータ オートモビリジェンス研究所
NTTデータグループ

取扱代理店製品

TOOLS

UPPAAL Product

UPPAAL

リアルタイムシステムの妥当性確認と検証の統合環境
~タイミング制約~

背景・課題

いまや、「リアルタイムシステムの安全性」は開発者だけでなく、高度に電子化されつつある現代社会のもっとも高い関心事のひとつです。しかし、リアルタイムでかつ複数のプロセスが同時に動作するようなシステムの安全性を確保するのは難しく、通常の方法(テスト)では非常にコストがかかります。
システムの非機能要求の一つとして重要な「時間に関する要件」を確認・検証するためには、以下のような課題があります。

検証の実現可能性

リアルタイムシステムには、ユーザビリティを確保するための応答性から人命に関わる緊急時の振舞いの安全性に至るまで、多くの機能・動作が要求されます。しかし、その殆どが実機をつくるまで性能を評価できません。

時間制約を伴うモデル検査

形式手法の1分野である、モデル検査技術が注目されています。しかし、多くのモデル検査ツールは、リアルタイムシステムにおいて重要な概念である「時間制約」が自然な形で記述できず、また、ユーザビリティの面でも整備されていません。
- ※時間オートマトン理論に基づく、時間制約を利用した遷移のガード条件、状態の不変条件

協調・分散システムの複雑性

複数の並列に動作するプログラムが共通のリソースに対して書き込みを行うような状況で動作する場合、タイミングにまつわる様々な問題( 「デッドロック」など)が増えています。これらの問題を設計図からレビューや限られたテストだけで検出、解決することは困難です。

解決策

時間制約を表現可能なモデルを通して検査・検証を行います。

検証の実現可能性

リアルタイムシステムには、ユーザビリティを確保するための応答性から人命に関わる緊急時の振舞いの安全性に至るまで、多くの機能・動作が要求されます。しかし、その殆どが実機をつくるまで性能を評価できません。

時間制約を伴うモデル検査

時間制約の要求仕様を時間オートマトンとして、検証式を時間CTLとして記述することで、タイミングの問題を表現し、解法します。

協調・分散システムの複雑性

各オートマトン間にブロードキャスト・メッセージ通信の機能を実装させることで、複雑な並列・分散システムの検証を実現します。

UPPAALの特長

時間拡張された状態遷移モデル

- UPPAALは時間拡張された状態遷移モデルを使っています。したがって、複数の並列で動作するプログラムたちが時間的な制約の中で適切な動作をするか、といった複雑なモデルを作成できます。これによって、テストではとてもカバーしきれないタイミングを含む網羅的な検証を可能とします。

ビジュアルなモデル作成

- モデル検証技術を利用するには、検証対象の挙動を表す状態遷移モデルを作成する必要があります。この作成のために、プログラミング言語のようなモデル記述 言語(だけ)を利用してモデルを作成しなければならない検証ツールもあります。この作業はプログラミング言語によるプログラミングと同様特殊なスキルと手間が必要です。
- UPPAALは、使いやすいビジュアルなモデリング環境(システム・エディタ)を提供しているため、状態遷移モデルの構築を短時間で作成できます。また、詳細の記述のためのスクリプトに関しても、わかり易いエラーメッセージの表示が充実しているため、直ぐに間違いが見つけられます。

UPPAAL ビジュアルなモデル作成

シーケンス図による動作シミュレーション

- シミュレーション機能によって、UPPAALの検証モデルとして作成した状態遷移モデルを直接実行し、動作の妥当性を確認する事が可能です。シミュレーションの進行は、UMLなどでおなじみの「メッセージ・シーケンス図」によってリアルタイムに表示されます。この図によって、定義された平行に動作する複数のプロセスの状態の変化と、そのプロセス同士の通信の発生も理解しやすい形で表示されます。シミュレーション中は、状態やシステムで定義された変数の内容の変化を確認できるため、シミュレーション中に起こった不具合などの原因を確かめることができます。

UPPAAL シーケンス図による動作シミュレーション

時間を考慮した検証性質の記述

- モデル検査では、作成したモデルの性質を検査するために記述する検証式という論理式を記述します。UPPAALでは時相論理という時間制約を表現できる論理式を採用しておりこれによってモデルが充たすべき時間制約を適切に表現することができます。

UPPAAL 時間を考慮した検証性質の記述

わかりやすい反例出力

- ある性質の検査の実行結果として、その性質が充たされなかった場合、UPPAALでは検査の失敗という情報だけでなくそのモデルが初期状態からどの様な動作経路を経て性質を充たさない状況にいたったのか、ということを「反例」として確認する事ができます。反例は、シミュレーションの画面のシーケンス図として表示されているため、そのシーケンス図の動作を再生して問題がある箇所を確認するといった作業が格段に楽に行なえます。

UPPAALの効果

安全性の保証

- システムが問題のある状況へ陥らないことをモデルと検証式(性質)から網羅的に検査し、安全性を保証できます。

並列・分散システムの構築支援

- マルチスレッド、マルチタスク、及びマルチコアに配置される並列動作するソフトウェアからなるシステムが問題なく動作可能な設計になっているかどうかを確認できます。

UPPAALのツール構成・オプション

UPPAALツール群は、Java/Swingで書かれたGUI部分(プラットフォーム非依存)と、C++によって書かれたモデル検査エンジン部分(プラットフォーム依存)が別々な実行単位として構成されています

UPPAAL ツール構成・オプション

モデル検査ツール適用の流れ

例) 設計モデルの検査

STEP1 要件定義⇒UPPAAL性質記述を抽出
STEP2 設計⇒UPPAAL検査モデルの抽出
STEP3 UPPAALによる検査
STEP4 検査内容の設計へのフィードバック

UPPAAL 設計モデルの検査

例) 上位設計への利用

STEP1 要件定義
⇒UPPAAL性質記述を抽出
STEP2 上位設計としてUPPAALモデルを検証しながら作成
STEP3 設計モデルを作成

UPPAAL 上位設計への利用

UPPAALの機能

モデル作成機能

Uppaalのモデルである時間オートマトンの遷移構造をグラフィカルなエディタによって記述できます。
(モデル要素)

  • グラフィカルなモデル要素(図形エディタによる)
  • ロケーション、エッジの図形的な接続関係
  • 非グラフィカルなモデル要素(テキストボックスへの入力)
  • ロケーション:名前、不変式(invariant)、ロケーション属性(初期、Comitted, Urgent)
  • エッジ:ガード条件、同期指定、変数更新
  • プロセス
  • 時間オートマトン定義(template)のインスタンスがプロセス
  • プロセス(インスタンス)生成時にパラメーターが渡せる。
  • 同期チャネルによるプロセス間通信

シミュレーション機能

Uppaalモデルを直接シミュレーションします。シミュレーションの表現は、状態遷移図、シーケンス図の動的な変化でグラフィカルに表示されて、見やすいものになっています。また、シミュレーションの各ステップでの変数の内容が表示されます。

モデル検査機能

記述したモデルが表現するシステムが満たすべき性質を時相論理式(TCTL)で表現したものを登録し、それぞれ、もしくは一括でモデル検査を実行できます。検査性質を満たさなれない場合、そこまでの実行パスを反例として出力し、シミュレーション画面で視覚的に不具合解析することができます。
<時相論理オペレータ(TCTL)による性質記述>

  • A[] p - 全ての実行パスで常にpが成り立つ
  • A<>p - 全ての実行パスでいずれpが成り立つ
  • E[] p - pが常に成り立つパスがある
  • E<>p - いずれpが成り立つパスがある
  • p → q - pが成り立てばそのうちqが成り立つ

対応モデル

UPPAAL時間オートマトン

開発元情報

http://www.uppaal.com/

取扱代理店製品

Agency Tools

Tableau

Tableau

Tableau

Business Intelligence ツール

手元に存在する大量のデータを、専門知識やプログラミングスキルを要さず簡単に視覚化し、分析できるツールです。高速で簡単、そして美しさを備えた役立つデータ分析が可能な、誰もが使えるソフトウェアです。

UPPAAL

UPPAAL

UPPAAL

Timed Automaton
モデル検査ツール

複数の並列で動作するプログラムが時間的な制約の中で適切な動作をするか、といった複雑なモデルを作成できます。これによって、テストではカバーしきれないタイミングを含む網羅的な検証を可能とします。

PAT Pro

PAT Pro

National University of Singapore

Multi Domain
モデル検査ツール

並列システムの形式仕様記法 CSP(Communicating Sequential Process)を用いて並列システムが満たすべき性質のモデル検査を実行できます。検査性質を満たさない場合、実行パスを反例として出力し、シミュレーション画面で視覚的に不具合を解析できます。

テクマトリックス株式会社

C++test

PARASOFT社

静的解析・単体テストツール

C/C++ 言語対応の静的解析・単体テストツールです。静的解析はパターンマッチングによる解析と実行フローのシミュレーションによる解析の両方をサポートしています。開発工程に C++test による静的解析、単体テストを組み込むことにより、効率的なテストとソースコードの品質向上が期待できます。

Altia

組込みシステム向け
モデルベース HMI 設計ツール、コードジェネレータ

組込み向け HMI/スクリーン設計およびソースコード生成ツールです。小さなメモリのローエンドシステムからハイエンドまで、幅広いデバイスと多くの RTOS に対応しています。理想の GUI 画像設計を実現出来ます。

株式会社SRA

組込みシステム向け
モデルベース HMI 設計ツール、コードジェネレータ

組込み向け HMI/スクリーン設計およびソースコード生成ツールです。小さなメモリのローエンドシステムからハイエンドまで、幅広いデバイスと多くの RTOS に対応しています。理想の GUI 画像設計を実現出来ます。

MicroFocus

StarTeam

MicroFocus社

構成・変更管理ツール

構成管理機能の他に変更管理、欠陥追跡、要件管理、プロジェクト・タスク管理、スレッド形式のディスカッションなどを含む包括的なソリューションを提供するツール

CONTACT

導入に関する質問やご相談、サポートに関することなど、まずはお気軽にご相談ください。