UPPAALの適用事例
Uppaalは多くの（産業での）ケーススタディーに応用されてきました。このページでは、それらのいくつかをご紹介したいと思います(参照：Uppaalのカタログ/Uppaal開発元)。→日本語訳のダウンロード
- オーディオ/ビデオプロトコル
これはリアルタイムに非常に依存するオーディオ制御プロトコルです。このプロトコルはBnagとOlufsenが開発したもので、オーディオ/ビデオコンポーネント間のメッセージ転送のためのものです。それは不完全である事が知られていましたが、誤りは従来のテスト方法の利用によっては見つけられていませんでした。[5]では、Uppaalは見つけた誤りのエラートレースを自動的に生成するのに適用されています。さらに、修正はUppaalを使用することによって示され立証されました。 - 境界付きの再送プロトコル
このプロトコルはCOST247(International Workshop on Applied Formal Methods in System Design)にて提案され、研究されています。これは損失性の通信チャネルの上での交番ビットプロトコル(Alternating bit protocol)に基づいていますが、境界のある再送の回数を考慮するというものです。[4]では、プロトコルの多くの特性がUppaalによってに自動的に確かめられたと報告されます。特に、プロトコルの正当性が、正しく選ばれたタイムアウト値に依存していることが示されます。 - 衝突回避プロトコル
このプロトコルはCSMA/CDプロトコルの様なイーサネットに似ている媒体上に実装されます。それはネットワーク・ノード間の通信遅延の上限を確実にします。 [6]では、Uppaalを利用する事で設計され、正しさが証明されます。2つの主な確立した性質が、このプロトコルが衝突無しである事を示します。そして、それはユーザからユーザへの通信遅延の上限を確実にします（完全な媒体を仮定）。 - ギアボックスコントローラ
[12]では、UppaalはMecel AB(自動車生産の制御システムを開発しているスエーデンの会社）での自動車のギアボックスコントローラプロトタイプの設計と解析、といった工業的なケーススタディに適用されています。ギアボックスコントローラは現代的な自動車のリアルタイムシステムの中のコンポーネントです。コントローラの設計では、システムの挙動の検証のためにUppaalのシミュレーションツールが適用されました。ギアボックスコントローラの設計の正当性はMecelABによって指定されたインフォーマルな要件から導出された46の性質の自動検証によって確立されました。 - フィリップスオーディオ制御プロトコル
このプロトコルはManchesterエンコーディングを使っているオーディオ装置コンポーネント間の制御情報を交換するためにフィリップスが開発、実装したものです。このエンコードの正確さは信号間のタイミングの遅延に依存しています。[8]では、このプロトコルはUppaalを使ってモデル化され、検証されています。[3]では、バスの衝突検出に拡張されたプロトコルのバージョンはUppaalによって解析されました。このケーススタディのモデルは、いくつかの新しいコンポーネント（と変数）を導入するため、オリジナルバージョンよりもかなり大きく、既存のコンポーネントは、バス衝突に対応するように変更されています。 - TDMAプロトコルの起動メカニズム
[13]では、TDMA(Time Division Multiple Access)プロトコルの起動の形式検証が報告されます。３つの通信ステーションの全体が同期して任意の初期状態から与えられたクロックドリフトが+-10^-3の範囲で操作できることがUppaalを使うことでチェックされています。さらに、完全な起動のための時間の条件が導出されました。 - 【UPPAAL事例・関連論文】
[1] Tobias Amnell, Gerd Behrmann, Johan Bengtsson, Pedro R.D’Argenio,Alexandre David, Ansgar Fehnker, Thomas Hune, Bertrand Jeannet, Kim G.Larsen, M. Oliver M¨oller, Paul Pettersson, Carsten Weise, and Wang Yi.Uppaal - Now, Next, and Future. In F. Cassez, C. Jard, B. Rozoy, and M. Ryan, editors, Modelling and Verification of Parallel Processes, number2067 in Lecture Notes in Computer Science, pages 100-125. Springer-Verlag, 2001.
[2] Gerd Behrmann, Alexandre David, , and Kim G. Larsen. A tutorial on uppaal.In Proc. of 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, number 3185 in Lecture Notes in Computer Science, 2004.
[3] Johan Bengtsson, W.O. David Griffioen, K°are J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Verification of an Audio Protocol with Bus Collision Using Uppaal. In Rajeev Alur and Thomas A. Henzinger, editors, Proc. of the 8th Int. Conf. on Computer Aided Verifica- tion, number 1102 in Lecture Notes in Computer Science, pages 244-256.Springer-Verlag, July 1996.
[4] P.R. D’Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In Proc. of the 3rd Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1217 in Lecture Notes in Computer Science, pages 416-431. Springer-Verlag, April 1997.
[5] Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund. Formal Modeling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using Uppaal. In Proc. of the 18th IEEE Real-Time Systems Symposium. IEEE Computer Society Press, December 1997.
[6] Henrik E. Jensen, Kim G. Larsen, and Arne Skou. Modelling and Analysis of a Collision Avoidance Protocol Using SPIN and Uppaal. In Proc. of 2nd Int. Workshop on the SPIN Verification System, pages 1-20, August 1996.
[7] Kim G. Larsen, Paul Pettersson, and Wang Yi. Compositional and Symbolic Model-Checking of Real-Time Systems. In Proc. of the 16th IEEE Real-Time Systems Symposium, pages 76-87. IEEE Computer Society Press, December 1995.
[8] Kim G. Larsen, Paul Pettersson, and Wang Yi. Diagnostic Model-Checking for Real-Time Systems. In Proc. of Workshop on Verification and Control of Hybrid Systems III, number 1066 in Lecture Notes in Computer Science, pages 575-586. Springer-Verlag, October 1995.
[9] Kim G. Larsen, Paul Pettersson, and Wang Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1-2):134-152, October 1997.
[10] Kim G. Larsen, Carsten Weise, Wang Yi, and Justin Pearson. Clock difference diagrams. Nordic Journal of Computing, 6(3):271-298, 1999.
[11] Fredrik Larsson, Kim G. Larsen, Paul Pettersson, and Wang Yi. Efficient Verification of Real-Time Systems: Compact Data Structures and State-Space Reduction. In Proc. of the 18th IEEE Real-Time Systems Symposium, pages 14-24. IEEE Computer Society Press, December 1997.
[12] Magnus Lindahl, Paul Pettersson, and Wang Yi. Formal Design and Analysis of a Gear-Box Controller. In Proc. of the 4th Workshop on Tools and Algorithms for the Construction and Analysis of Systems, number 1384 in Lecture Notes in Computer Science, pages 281-297. Springer-Verlag, March 1998.
[13] Henrik L¨onn and Paul Pettersson. Formal Verification of a TDMA Protocol Startup Mechanism. In Proc. of the Pacific Rim Int. Symp. on Fault- Tolerant Systems, pages 235-242, December 1997.
[14] Wang Yi, Paul Pettersson, and Mats Daniels. Automatic Verification of Real-Time Communicating Systems By Constraint-Solving. In Dieter Hogrefe and Stefan Leue, editors, Proc. of the 7th Int. Conf. on Formal Description Techniques, pages 223-238. North-Holland, 1994.