基于時(shí)間自動(dòng)機(jī)模型驗(yàn)證方法優(yōu)化研究.pdf

1、實(shí)時(shí)系統(tǒng)是一種帶有時(shí)間約束的計(jì)算系統(tǒng)，這些系統(tǒng)的許多動(dòng)作的完成是與時(shí)間相關(guān)的，即要滿足一定的時(shí)間限制。為了確保實(shí)時(shí)系統(tǒng)的正確性和可靠性，需要對(duì)其進(jìn)行嚴(yán)格的分析和驗(yàn)證。實(shí)時(shí)系統(tǒng)的驗(yàn)證不僅要求邏輯上是正確的，而且要求時(shí)間上也是正確的?，F(xiàn)在網(wǎng)絡(luò)協(xié)議的復(fù)雜性日益增加。協(xié)議中的每一處錯(cuò)誤和缺陷都將給網(wǎng)絡(luò)系統(tǒng)的穩(wěn)定性、可靠性等帶來(lái)巨大的危害。協(xié)議的驗(yàn)證中往往也需要驗(yàn)證一些時(shí)間性質(zhì)。 對(duì)實(shí)時(shí)系統(tǒng)和協(xié)議通常采用形式化的方法來(lái)進(jìn)行驗(yàn)證。有限自動(dòng)機(jī)

2、是最為重要的一種形式描述與驗(yàn)證技術(shù)，它是很多形式化方法的基礎(chǔ)。它直觀性強(qiáng)，可實(shí)現(xiàn)與其它形式化方法的組合和轉(zhuǎn)換。但是由于其沒(méi)有清楚的時(shí)間的概念，只能處理事件的序列，而不能準(zhǔn)確地描述事件發(fā)生的時(shí)間，因此在模型驗(yàn)證上的應(yīng)用受到很大的限制。為解決這個(gè)問(wèn)題，R.Alur等人提出了時(shí)間自動(dòng)機(jī)模型。時(shí)間自動(dòng)機(jī)在有窮自動(dòng)機(jī)的基礎(chǔ)上加入了時(shí)鐘變量，通過(guò)時(shí)鐘變量和時(shí)鐘值的比較來(lái)約束狀態(tài)的轉(zhuǎn)移，因此時(shí)間自動(dòng)機(jī)可以準(zhǔn)確地描述帶有時(shí)間的系統(tǒng)。 時(shí)間自動(dòng)機(jī)

3、的狀態(tài)空間的大小隨著問(wèn)題規(guī)模的增大呈指數(shù)級(jí)遞增。當(dāng)系統(tǒng)規(guī)模較大時(shí)，基于時(shí)間自動(dòng)機(jī)的驗(yàn)證就會(huì)變得非常復(fù)雜。所以需要對(duì)時(shí)間自動(dòng)機(jī)的模型驗(yàn)證方法進(jìn)行優(yōu)化。 本文主要研究了域自動(dòng)機(jī)方法、帶自動(dòng)機(jī)方法以及基于歷史等價(jià)和轉(zhuǎn)換互模擬的最小化方法。文中對(duì)時(shí)鐘域及其上的操作給出了一種符號(hào)化的表示方法，從而便于域自動(dòng)機(jī)在實(shí)際操作中的實(shí)現(xiàn)。本文還提出了基于狀態(tài)轉(zhuǎn)移時(shí)間關(guān)系的優(yōu)化方法。該方法通過(guò)計(jì)算狀態(tài)轉(zhuǎn)移的最早可能發(fā)生時(shí)間和最晚可能發(fā)生時(shí)間來(lái)判斷轉(zhuǎn)移