實(shí)時(shí)系統(tǒng)的運(yùn)行時(shí)驗(yàn)證研究.pdf

1、在國民經(jīng)濟(jì)與國防現(xiàn)代化建設(shè)中，計(jì)算機(jī)軟件在日常生活中的應(yīng)用越來越普及，軟件可靠性問題日趨受到人們的重視，尤其對于一些安全關(guān)鍵領(lǐng)域，如載人航天、高速軌道交通等。應(yīng)用于這些領(lǐng)域的系統(tǒng)通常是實(shí)時(shí)控制系統(tǒng)，這類系統(tǒng)不僅要求系統(tǒng)做出正確的響應(yīng)，且要求系統(tǒng)的響應(yīng)滿足相應(yīng)的時(shí)間約束。系統(tǒng)一旦發(fā)生失效，將會給國家安全乃至人員生命帶來極大損失，因此如何提高這類系統(tǒng)的可靠性成為目前計(jì)算機(jī)領(lǐng)域的一個(gè)非常重要的研究內(nèi)容。傳統(tǒng)的測試方法由于存在測試用例不完備等問

2、題無法滿足系統(tǒng)的可靠性需求，模型檢測能給出系統(tǒng)完備的正確性證明，但是對于復(fù)雜系統(tǒng)來說，這一技術(shù)面臨著狀態(tài)空間爆炸等問題。運(yùn)行時(shí)驗(yàn)證作為測試和模型檢測的有效補(bǔ)充，在系統(tǒng)運(yùn)行過程中實(shí)施有效地監(jiān)控與驗(yàn)證，盡早地發(fā)現(xiàn)軟件失效，有助于提高實(shí)時(shí)系統(tǒng)的安全性和可靠性。
　　為了提高實(shí)時(shí)系統(tǒng)的安全性和可靠性，本文提出一種基于度量區(qū)間時(shí)序邏輯(Metric Interval Temporal Logic，MITL)三值語義的運(yùn)行時(shí)驗(yàn)證方法，主要工作

3、如下:
　　1、介紹了pointwise語義模型下MITL在有窮軌跡上的語法及語義，采用pointwise語義模型是因?yàn)镸ITL在該語義模型下是可判定的，定義了MITL在有窮軌跡上的三值語義，與LTL三值語義不同的是，它是在有窮時(shí)間字上進(jìn)行解釋的。
　　2、本文定義了基于MITL三值語義的監(jiān)控器的形式化描述，即基于遷移的擴(kuò)展時(shí)間Buchi自動機(jī)(transition-based generalized timed Buchi

4、 automaton，TGTBA)，它是在基于遷移的擴(kuò)展Buchi自動機(jī)的基礎(chǔ)上，通過增加時(shí)鐘約束得到的。在此基礎(chǔ)上，研究了一種構(gòu)造預(yù)測監(jiān)控器的方法，即采用邏輯重寫的方法，根據(jù)給出的重寫算法將公式重寫為要求的形式，基于重寫后的公式來構(gòu)造TGTBA，將此TGTBA作為MITL公式的預(yù)測監(jiān)控器，用于運(yùn)行時(shí)驗(yàn)證過程中。
　　3、在上述驗(yàn)證方法和MaC驗(yàn)證框架的基礎(chǔ)上，將基于MITL的預(yù)測監(jiān)控器應(yīng)用于MaC框架中，實(shí)現(xiàn)了基于MITL三值語