そろそろ始めませんか？「モデル検査」

• いまや、「リアルタイムシステムの安全性」は開発者だけでなく、高度に電子化されつつある現代社会のもっとも高い関心事のひとつです。しかし、リアルタイムでかつ複数のプロセスが同時に動作するようなシステムの安全性を確保するのは難しく、通常の方法（テスト）では非常にコストがかかります。

システムの非機能要求の一つとして重要な「時間に関する要件」を確認・検証するためには、以下のような課題があります。

• 検証の実現可能性
  リアルタイムシステムには、ユーザビリティを確保するための応答性から人命に関わる緊急時の振舞いの安全性に至るまで、多くの機能・動作が要求されます。しかし、その殆どが実機をつくるまで性能を評価できません。
• 時間制約※を伴うモデル検査
  形式手法の１分野である、モデル検査技術が注目されています。しかし、多くのモデル検査ツールは、リアルタイムシステムにおいて重要な概念である「時間制約」が自然な形で記述できず、また、ユーザビリティの面でも整備されていません。
  - ※時間オートマトン理論に基づく、時間制約を利用した遷移のガード条件、状態の不変条件
• 協調・分散システムの複雑性
  複数の並列に動作するプログラムが共通のリソースに対して書き込みを行うような状況で動作する場合、 タイミングにまつわる様々な問題（ 「デッドロック」など）が増えています。これらの問題を設計図からレビューや限られたテストだけで検出、解決することは困難です。

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

• 検証の実現可能性
  リアルタイムシステムには、ユーザビリティを確保するための応答性から人命に関わる緊急時の振舞いの安全性に至るまで、多くの機能・動作が要求されます。しかし、その殆どが実機をつくるまで性能を評価できません。
• 時間制約を伴うモデル検査
  時間制約の要求仕様を時間オートマトンとして、検証式を時間CTLとして記述することで、タイミングの問題を表現し、解法します。
• 協調・分散システムの複雑性
  各オートマトン間にブロードキャスト・メッセージ通信の機能を実装させることで、複雑な並列・分散システムの検証を実現します。

概要

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

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

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

  - モデル検証技術を利用するには、検証対象の挙動を表す状態遷移モデルを作成する必要があります。この作成のために、プログラミング言語のようなモデル記述 言語（だけ）を利用してモデルを作成しなければならない検証ツールもあります。この作業はプログラミング言語によるプログラミングと同様特殊なスキルと手 間が必要です。

  - UPPAALは、使いやすいビジュアルなモデリング環境（システム・エディタ）を提供しているため、状態遷移モデルの構築を短時間 で作成できます。また、詳細の記述のためのスクリプトに関しても、わかり易いエラーメッセージの表示が充実しているため、直ぐに間違いが見つけられます。

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

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

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

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

• わかりやすい反例出力
  

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

• 安全性の保証
  

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

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

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

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

例） 設計モデルの検査

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

例） 上位設計への利用

• 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/

UPPAALは次の環境で動作します。

↑ページTOPへ