基于時(shí)間自動機(jī)的風(fēng)洞試驗(yàn)自動控制研究

用多個時(shí)間自動機(jī)來規(guī)范模擬風(fēng)洞試驗(yàn)自動控制系統(tǒng)，給出了一種自動化的風(fēng)洞
試驗(yàn)控制模型（CRW），并采用實(shí)時(shí)系統(tǒng)驗(yàn)證工具Uppaal 對CRW 進(jìn)行了驗(yàn)證，證明了該模型具有安全性、有效性和可控性。所采用的方法避免了積的等價(jià)類狀態(tài)空間的爆炸，減少了驗(yàn)證的搜索空間，為風(fēng)洞試驗(yàn)系統(tǒng)提供了一種可行的、安全的、智能的控制機(jī)制。
關(guān)鍵詞： 時(shí)間自動機(jī)；風(fēng)洞試驗(yàn)；Uppaal；實(shí)時(shí)系統(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