時(shí)間自動(dòng)機(jī)可達(dá)性研究.pdf

1、實(shí)時(shí)系統(tǒng)的模型檢驗(yàn)方法是一種保證計(jì)算機(jī)實(shí)時(shí)系統(tǒng)安全性和可靠性的嚴(yán)格的形式化方法,隨著計(jì)算機(jī)科學(xué)的發(fā)展,這種方法已經(jīng)被廣泛地接受和使用.由于模型檢驗(yàn)方法在對(duì)系統(tǒng)建模時(shí)存在狀態(tài)空間爆炸問題,因此模型驗(yàn)證核心問題是狀態(tài)空間最小化問題.使用時(shí)間自動(dòng)機(jī)對(duì)實(shí)時(shí)系統(tǒng)規(guī)范和驗(yàn)證,主要包括對(duì)實(shí)時(shí)系統(tǒng)建模即構(gòu)造系統(tǒng)的時(shí)間自動(dòng)機(jī)和安全可靠性驗(yàn)證.這兩方面的核心問題是狀態(tài)空間的簡(jiǎn)化和狀態(tài)可達(dá)性分析.而這一核心問題是本文研究的重點(diǎn).在實(shí)時(shí)系統(tǒng)規(guī)范驗(yàn)證中.考慮到系

2、統(tǒng)中多數(shù)待檢驗(yàn)問題僅僅是一些簡(jiǎn)單的性質(zhì).因此我們不必構(gòu)造系統(tǒng)的所有狀態(tài)集合,而僅僅考慮對(duì)可達(dá)性問題的判斷.論文對(duì)時(shí)間自動(dòng)機(jī)的可達(dá)性問題進(jìn)行了深入研究,對(duì)不同的可達(dá)性分析方法進(jìn)行了比較,并著重對(duì)基于時(shí)間約束的可達(dá)性分析方法進(jìn)行分析.在此基礎(chǔ)上,針對(duì)基于時(shí)間約束的可達(dá)性分析方法,本文給出了該方法的機(jī)器表示,并提出了一種新的后繼計(jì)算方法,通過該方法能夠較好地減少后繼狀態(tài)空間的個(gè)數(shù),從而使問題規(guī)模減小;另外給出了可達(dá)性算法的預(yù)處理方法,通過預(yù)處