UPPAAL是使用較多的基于時間自動機的驗證工具。它是由丹麥Aalborg大學(xué)和瑞士Uppsala大學(xué)聯(lián)合開發(fā)的對實時系統(tǒng)模擬和驗證的工具。時間自動機是對自動機理論的擴展，提供了形式化的方法來建立和分析實時系統(tǒng)的行為，在模型檢測方面有著重要的應(yīng)用。時間自動機為實時系統(tǒng)的自動化分析和驗證提供了一種形式化的理論模型。

在http://www.uppaal.org/網(wǎng)站下載UPPAAl安裝包，安裝UPPAAL要求有java 運行環(huán)境，并且UPPAAL4.1版本需要比較高的JDK 版本，如1.7，1.8版本。

下載好UPPAAL壓縮文件之后，解壓，會有一個uppaal.jar文件，安裝該文件就可以安裝好UPPAAL。

uppaal.jar是一個可執(zhí)行的jar包，可執(zhí)行的jar包包含了：

Main-Class: com.uppaal.gui.Main
SplashScreen-Image: com/uppaal/resource/images/splash40.png
Class-Path: lib/jh.jar lib/jlfgr-1_0.jar lib/jsr173_1.0_api.jar lib/js
r173_1.0_ri.jar lib/swixml.jar lib/jdom.jar lib/editor.jar lib/model.

在控制臺運行命令：

java -jar uppaal.jar所在目錄
就可以成功安裝UPPAAL。
---------------------
作者：yuedaowenIT
來源：CSDN
原文：https://blog.csdn.net/yuedaowenIT/article/details/45558203
版權(quán)聲明：本文為博主原創(chuàng)文章，轉(zhuǎn)載請附上博文鏈接！

總結(jié)

以上是生活随笔為你收集整理的【转】ModelChecking工具UPPAAL安装与简介的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。