|
形式言語のうち、モデル検査の機能を持つシステム。 時間制約付きモデルを図として記述し、検査・検証を行う。時相論理式で検査したい項目を指定する。 学術向けは無償利用できるが、商用は有償。日本ではキャッツが販売代理店をしている。 JAXAなど、研究開発〔 JAXAにおける形式手法に対する取組み | http://cfv.jp/cvs/event/workshop/2012/09/pdf/jaxa.pdf〕機関での利用が進んでいる。 == 開発元 == 2つの大学の共同事業 * Uppsala University, Sweden * Aalborg University in Denmark. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Uppaal」の詳細全文を読む スポンサード リンク
|