この記事は検証可能な参考文献や出典が全く示されていないか、不十分です。 出典を追加して記事の信頼性向上にご協力ください。（このテンプレートの使い方） 出典検索?: "Uppaal" – ニュース · 書籍 · スカラー · CiNii · J-STAGE · NDL · dlib.jp · ジャパンサーチ · TWL (2015年10月)

Uppaal（ウパール）は、形式言語のうち、モデル検査の機能を持つシステム。時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。JAXAなど、研究開発^[1]機関での利用が進んでいる。

開発元

2つの大学の共同事業

• Uppsala University, Sweden
• Aalborg University in Denmark.

脚注

参考文献

• UPPAALを用いたLEGO mindstorms EV3制御プログラムの合成 ,荒川 洸. 結縁 祥治,ソフトウェアサイエンス, 電子情報通信学会技術研究報告,電子情報通信学会, 114(271):2014.10.23・24,ページ41-46,ISSN 0913-5685
• UPPAALによる性能モデル検証 = Performance Model Verification by UPPAAL : リアルタイムシステムのモデル化とその検証 , 大須賀昭彦 監修 ; 長谷川哲夫, 田原康之, 磯部祥尚 著., 近代科学社, 2012.9. ISBN 978-4-7649-0431-6

外部リンク

• Home | UPPAAL - 学術用
• UP4ALL Inc - uppaal.com - 商用