いまや、「リアルタイムシステムの安全性」は開発者だけでなく、高度に電子化されつつある現代社会のもっとも高い関心事のひとつです。しかし、リアルタイムでかつ複数のプロセスが同時に動作するようなシステムの安全性を確保するのは難しく、通常の方法（テスト）では非常にコストがかかります。
このツールは、「モデル検査」という新しい技術によって、そのその様な安心・安全なリアルタイム・システムの開発を支援するビジュアルな統合モデル検証ツールです。

UPPAALは、「時間制約を考慮できるモデル検査ツール」です。このツールは、複数の並列で動作するプロセス群が時間的な制約の中で適切な動作をするか、といった複雑でテストではとてもカバーしきれない検証を可能とします。

外部要因が起こってから、実際に機能が動作するまでの時間に制限があるようなシステムがあります。これらは、そのシステムの安全性に対しての基準だったり、ユーザビリティを確保するための応答性だったりします。
特に、人命に関わる様な緊急時のシステムの振る舞いがこの様な時間性能を充たさない可能性を少しでも持っている場合、それが起こってしまったとき（間に合わなかったとき）のユーザへ及ぼす被害は多大なものとなりえます。
UPPAALの様なツールによって、システムがこの様な時間性能を満たす事を検査することではじめて、「その状況が起こらない」事が証明でき、安全を保障する事ができます。

複数の並行に動作するプログラムが共通のリソースに対して書き込みを行うような状況で動作する場合、タイミングにまつわる様々な問題が起こりえます。例えば、「デッドロック」などの問題です。
UPPAALを利用したモデル検証によって、システム内に定義されている複数のプロセス（またはタスク、スレッド）がどの様なタイミングで動作すればその様な問題が起こるのかを見つける事ができます。

多くのモデル検査ツールで採用している状態遷移モデルではこれらの時間制約を自然な形で記述できないため、時間制約のかかったモデル検査を行うにはモデル作成のために特殊なテクニックを駆使する必要があります。また、それには形式検証に関しての高度な知識を要求されます。
UPPAALでは、モデルとして時間制約を直接表現できるため、タイミングに関する要求仕様があれば検証モデルを作成可能です。したがって、安心、安全なシステム開発を行なう必要のあるエンジニアの多大な工数を節約できます。

現在注目されているモデル検査という技術は、開発者の意図するようにシステムが動作することを数学的な意味で証明する、といったことを研究する「形式検証」という分野の成果です。

モデル検査するためには、まず、動作を形式的に定義された状態遷移モデルで表現します。また、システム要件として、そのシステムがどの様に動作して欲しいか、そしてどの様な状況にはなって欲しくないか、といった性質を記述します。

そして、モデル検査のアルゴリズムによってそのモデルから得られるそのシステムのありうる挙動を網羅的に探索します。その探索によって記述したシステムの性質が満たされているかどうかを「証明」します。

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

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

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

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

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

現在のバージョンのUPPAALの対応OSは、Windows2000/XP/Vista, 一部のLinuxとなっています。GUIを含むクライアント側のソフトウェアの動作にはJRE(Ver5以上)がインストールされている必要があります。

※UPPAALの開発元について
UPPAALという名前は、このツールの開発を行なった２つの大学の名前に由来しています。この２つの大学とは、スエーデンのUpsala大学とデンマークAalborg大学です。この２つの大学の先頭３文字ずつをとって

というわけです。この２つの大学のそれぞれの研究者がこのUPPAALの開発陣ですが、現在は開発・販売のための会社UP4ALLが設立されています。

キャッツ株式会社　営業本部
TEL 045-473-2816  FAX 045-473-2673
E-mail：info@zipc.com