「Uppaal」の版間の差分
提供: miniwiki
(2016年09月06日20時01分付け英語版en:Uppaal Model CheckerにならってカテゴリーCategory:モデルチェッカに追加。) |
細 (1版 をインポートしました) |
(相違点なし)
|
2018/8/19/ (日) 20:03時点における最新版
形式言語のうち、モデル検査の機能を持つシステム。 時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。 学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。 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
脚注
- ↑ JAXAにおける形式手法に対する取組み | http://cfv.jp/cvs/event/workshop/2012/09/pdf/jaxa.pdf