基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)建模及驗(yàn)證

摘要：實(shí)時(shí)系統(tǒng)必須在一個(gè)事先定義好的時(shí)間限制內(nèi)對(duì)來(lái)自外部或內(nèi)部的事件進(jìn)行響應(yīng)，如何有效驗(yàn)證實(shí)時(shí)模型的正確性和安全性是一個(gè)難點(diǎn)。文章通過(guò)多個(gè)時(shí)間自動(dòng)機(jī)來(lái)模擬實(shí)時(shí)系統(tǒng)中的各個(gè)對(duì)象，并用uPPAAL對(duì)模型進(jìn)行驗(yàn)證，減少了模型驗(yàn)證的狀態(tài)搜索空間，為實(shí)時(shí)嵌入式系統(tǒng)開(kāi)發(fā)和驗(yàn)證提供了一種可行、安全的控制機(jī)制。實(shí)驗(yàn)結(jié)果顯示了系統(tǒng)的有效性。

關(guān)鍵詞：時(shí)間自動(dòng)機(jī)；實(shí)時(shí)系統(tǒng)；UPPAAL；模型驗(yàn)證