用多個時間自動機來規(guī)范模擬風洞試驗自動控制系統(tǒng)，給出了一種自動化的風洞
試驗控制模型（CRW），并采用實時系統(tǒng)驗證工具Uppaal 對CRW 進行了驗證，證明了該模型具有安全性、有效性和可控性。所采用的方法避免了積的等價類狀態(tài)空間的爆炸，減少了驗證的搜索空間，為風洞試驗系統(tǒng)提供了一種可行的、安全的、智能的控制機制。
關鍵詞： 時間自動機；風洞試驗；Uppaal；實時系統(tǒng)
Abstract： Several timed automata are used to model an automatic wind tunnel test control
system and an automatic control model of a wind tunnel test (CRW) is presented. Uppaal is
adopted to carry out the on-the-flying testing and it is proved that CRW has such characteristics as safety, efficiency and control. The method mentioned avoids the equivalent state explosion of the product, reduces the verification search space and provides a feasible, safe and intelligent control mechanism.
Key words： timed automata；wind tunnel test；Uppaal；real-time system