Uppaal

ウィキペディア

Uppaal

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/12/09 04:30 UTC 版)

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